A Decision Procedure for Equality Logic with Uninterpreted Functions

Olga Tveretina

doi:10.1007/978-3-540-30210-0_7

A Decision Procedure for Equality Logic with Uninterpreted Functions

Olga Tveretina

School of Physics, Engineering & Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

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

Original language	English
Title of host publication	Artificial Intelligence and Symbolic Computation
Publisher	Springer Nature
Pages	66-79
ISBN (Electronic)	978-3-540-30210-0
ISBN (Print)	978-3-540-23212-4
DOIs	https://doi.org/10.1007/978-3-540-30210-0_7
Publication status	Published - 2004
Event	AISC 2004, 7th Int Conf - Linz, Austria Duration: 22 Sept 2004 → 24 Sept 2004

Publication series

Name	Lecture Notes in Computer Science
Volume	3249

Conference

Conference	AISC 2004, 7th Int Conf
Country/Territory	Austria
City	Linz
Period	22/09/04 → 24/09/04

Access to Document

10.1007/978-3-540-30210-0_7

Cite this

@inproceedings{2747463acf8e4e0ebebbf72da586f435,

title = "A Decision Procedure for Equality Logic with Uninterpreted Functions",

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",

author = "Olga Tveretina",

year = "2004",

doi = "10.1007/978-3-540-30210-0_7",

language = "English",

isbn = "978-3-540-23212-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "66--79",

booktitle = "Artificial Intelligence and Symbolic Computation",

note = "AISC 2004, 7th Int Conf ; Conference date: 22-09-2004 Through 24-09-2004",

}

TY - GEN

T1 - A Decision Procedure for Equality Logic with Uninterpreted Functions

AU - Tveretina, Olga

PY - 2004

Y1 - 2004

N2 - 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

AB - 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

U2 - 10.1007/978-3-540-30210-0_7

DO - 10.1007/978-3-540-30210-0_7

M3 - Conference contribution

SN - 978-3-540-23212-4

T3 - Lecture Notes in Computer Science

SP - 66

EP - 79

BT - Artificial Intelligence and Symbolic Computation

PB - Springer Nature

T2 - AISC 2004, 7th Int Conf

Y2 - 22 September 2004 through 24 September 2004

ER -