A decision procedure for equality logic with uninterpreted functions

O. Tveretina

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

A decision procedure for equality logic with uninterpreted functions

O. Tveretina

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004)
Editors	B. Buchberger, J.A. Campbell
Place of Publication	Berlin
Publisher	Springer
Pages	66-79
ISBN (Print)	3-540-23212-5
DOIs	https://doi.org/10.1007/978-3-540-30210-0_7
Publication status	Published - 2004

Publication series

Name	Lecture Notes in Computer Science
Volume	3249
ISSN (Print)	0302-9743

Access to Document

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

Cite this

Tveretina, O. (2004). A decision procedure for equality logic with uninterpreted functions. In B. Buchberger, & J. A. Campbell (Eds.), Artificial Intelligence and Symbolic Computation (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004) (pp. 66-79). (Lecture Notes in Computer Science; Vol. 3249). Springer. https://doi.org/10.1007/978-3-540-30210-0_7

@inproceedings{566504ef4aff4c4d983e366fed574c4d,

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 = "O. Tveretina",

year = "2004",

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

language = "English",

isbn = "3-540-23212-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "66--79",

editor = "B. Buchberger and J.A. Campbell",

booktitle = "Artificial Intelligence and Symbolic Computation (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004)",

address = "Germany",

}

Tveretina, O 2004, A decision procedure for equality logic with uninterpreted functions. in B Buchberger & JA Campbell (eds), Artificial Intelligence and Symbolic Computation (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004). Lecture Notes in Computer Science, vol. 3249, Springer, Berlin, pp. 66-79. https://doi.org/10.1007/978-3-540-30210-0_7

A decision procedure for equality logic with uninterpreted functions. / Tveretina, O.
Artificial Intelligence and Symbolic Computation (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004). ed. / B. Buchberger; J.A. Campbell. Berlin: Springer, 2004. p. 66-79 (Lecture Notes in Computer Science; Vol. 3249).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A decision procedure for equality logic with uninterpreted functions

AU - Tveretina, O.

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 - 3-540-23212-5

T3 - Lecture Notes in Computer Science

SP - 66

EP - 79

BT - Artificial Intelligence and Symbolic Computation (Proceedings 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004)

A2 - Buchberger, B.

A2 - Campbell, J.A.

PB - Springer

CY - Berlin

ER -

A decision procedure for equality logic with uninterpreted functions

Abstract

Publication series

Access to Document

Fingerprint

Cite this