Show simple item record

dc.contributor.authorTveretina, Olga
dc.contributor.authorZantema, Hans
dc.identifier.citationTveretina , O & Zantema , H 2004 , A Proof System and a Decision Procedure for Equality Logic . in LATIN 2004: Theoretical Informatics . Lecture Notes in Computer Science , vol. 2976 , Springer Nature , pp. 530-539 , 6th Latin American Symposium , Buenos Aires , Argentina , 5/04/04 .
dc.identifier.otherPURE: 1302860
dc.identifier.otherPURE UUID: bb3c00ac-140b-4581-87ad-821fd8da63ee
dc.identifier.otherScopus: 26844475009
dc.description.abstractEquality 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-SATen
dc.publisherSpringer Nature
dc.relation.ispartofLATIN 2004: Theoretical Informatics
dc.relation.ispartofseriesLecture Notes in Computer Science
dc.titleA Proof System and a Decision Procedure for Equality Logicen
dc.contributor.institutionSchool of Physics, Engineering & Computer Science

Files in this item


There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record