Transforming equality logic to propositional logic

DOI10.1016/S1571-0661(04)80661-3zbMath1261.03070OpenAlexW2002015997MaRDI QIDQ4916229

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

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

Related Items (1)

Generalizing DPLL and satisfiability for equalities

Uses Software

• HeerHugo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• BDD based procedures for a theory of equality with uninterpreted functions
• The propositional formula checker HeerHugo
• Solvable cases of the decision problem
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Boolean satisfiability with transitivity constraints
• LATIN 2004: Theoretical Informatics

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