University of Hertfordshire

By the same authors

A Decision Procedure for Equality Logic with Uninterpreted Functions

Research output: Chapter in Book/Report/Conference proceedingConference contribution

View graph of relations
Original languageEnglish
Title of host publicationArtificial Intelligence and Symbolic Computation
PublisherSpringer
Pages66-79
ISBN (Electronic)978-3-540-30210-0
ISBN (Print)978-3-540-23212-4
DOIs
Publication statusPublished - 2004
EventAISC 2004, 7th Int Conf - Linz, Austria
Duration: 22 Sep 200424 Sep 2004

Publication series

NameLecture Notes in Computer Science
Volume3249

Conference

ConferenceAISC 2004, 7th Int Conf
CountryAustria
CityLinz
Period22/09/0424/09/04

Abstract

The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced. Since it is based on the DPLL method, the procedure can adopt its heuristics. Therefore the procedure can be used as a basis for efficient implementations of satisfiability checkers for EUF. A part of the introduced method is a technique for reducing the size of formulas, which can also be used as a preprocessing step in other approaches for checking satisfiability of EUF formulas

ID: 1302920