Yet another decision procedure for equality logic

DOI10.1007/11513988_32MaRDI QIDQ5716573zbMATH OpenOpenAlexFDO

Authors Orly Meir, Ofer Strichman

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b138445

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• LATIN 2004: Theoretical Informatics
• A decision procedure for equality logic with uninterpreted functions
• Equality propositional logic and its extensions
• Equality logic
• Equality in linear logic
• scientific article; zbMATH DE number 3945373
• Kleene's Logic with equality
• Equality reasoning in sequent-based calculi
• scientific article; zbMATH DE number 956469
• Equivalence in logic-based argumentation

Cited in

(7)

• Theory decision by decomposition
• A superposition calculus for abductive reasoning
• Generating minimum transitivity constraints in P-time for deciding equality logic
• scientific article; zbMATH DE number 3945373 (Why is no real title available?)
• Range allocation for equivalence logic
• Transforming equality logic to propositional logic
• EufDPLL -- a tool to check satisfiability of equality logic formulas

Describes a project that uses

Uses Software

• UCLID
• Siege
• Chaff

This page was built for publication: Yet another decision procedure for equality logic

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