A decision procedure for equality logic with uninterpreted functions

DOI10.1007/978-3-540-30210-0_7MaRDI QIDQ5464719zbMATH OpenOpenAlexFDO

Authors Olga Tveretina

Publication date 19 August 2005

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

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

zbMATH Keywords

DPLL procedureequality logic with uninterpreted functionssatisfiability

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• LATIN 2004: Theoretical Informatics
• EufDPLL -- a tool to check satisfiability of equality logic formulas
• BDD based procedures for a theory of equality with uninterpreted functions
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• DPLL(T): Fast decision procedures

Cited in

(14)

• BDD based procedures for a theory of equality with uninterpreted functions
• EUFORIA: complete software model checking with uninterpreted functions
• Generalizing DPLL and satisfiability for equalities
• Reduced functional consistency of uninterpreted functions
• Finite instantiations in equivalence logic with uninterpreted functions
• EVC: A validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality, and conservative transformations
• Transforming equality logic to propositional logic
• EufDPLL -- a tool to check satisfiability of equality logic formulas
• Tools and Algorithms for the Construction and Analysis of Systems
• DPLL(T): Fast decision procedures
• Mathematical Foundations of Computer Science 2005
• Computer Aided Verification
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• LATIN 2004: Theoretical Informatics

Describes a project that uses

Uses Software

• ATERM

This page was built for publication: A decision procedure for equality logic with uninterpreted functions

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