A Proof System and a Decision Procedure for Equality Logic

Olga Tveretina, Hans Zantema

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

1 Citation (Scopus)


Equality Logic with uninterpreted functions is used for proving the equivalense or refinement between systems (hardware verification, compiler translation, etc). Current approaches for deciding this type of formulas use a transformation of an equality formula to the propositional one of larger size, and then any standard SAT checker can be applied. We give an approach for deciding satisfiability of equality logic formulas (E-SAT) in conjunctive normal form. Central in our approach is a single proof rule called ER. For this single rule we prove soundness and completeness. Based on this rule we propose a complete procedure for E-SAT and prove its correctness. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT
Original languageEnglish
Title of host publicationLATIN 2004: Theoretical Informatics
PublisherSpringer Nature
ISBN (Electronic)978-3-540-24698-5
ISBN (Print)978-3-540-21258-4
Publication statusPublished - 2004
Event6th Latin American Symposium - Buenos Aires, Argentina
Duration: 5 Apr 20048 Apr 2004

Publication series

NameLecture Notes in Computer Science


Conference6th Latin American Symposium
CityBuenos Aires


Dive into the research topics of 'A Proof System and a Decision Procedure for Equality Logic'. Together they form a unique fingerprint.

Cite this