Transforming equality logic to propositional logic

DOI10.1016/S1571-0661(04)80661-3MaRDI QIDQ4916229zbMATH OpenOpenAlexFDO

Authors Jan Friso Groote, Hans Zantema

Publication date 19 April 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)80661-3

Mathematics Subject Classification ID

Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35)

Recommendations

• LATIN 2004: Theoretical Informatics
• scientific article; zbMATH DE number 1885175
• Computer Aided Verification
• Artificial Intelligence and Symbolic Computation
• Equality propositional logic and its extensions

Cites work

• BDD based procedures for a theory of equality with uninterpreted functions
• Boolean satisfiability with transitivity constraints
• scientific article; zbMATH DE number 1670770 (Why is no real title available?)
• scientific article; zbMATH DE number 1696764 (Why is no real title available?)
• scientific article; zbMATH DE number 1796130 (Why is no real title available?)
• scientific article; zbMATH DE number 2102726 (Why is no real title available?)
• LATIN 2004: Theoretical Informatics
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Solvable cases of the decision problem
• The propositional formula checker HeerHugo

Cited in

(3)

• Transforming Boolean equalities into constraints
• Generalizing DPLL and satisfiability for equalities
• scientific article; zbMATH DE number 67458 (Why is no real title available?)

Describes a project that uses

Uses Software

• HeerHugo

This page was built for publication: Transforming equality logic to propositional logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4916229)