Theory decision by decomposition

DOI10.1016/J.JSC.2008.10.008zbMath1192.68626OpenAlexW1980250820MaRDI QIDQ1041591

Maria Paola Bonacina, Mnacho Echenim

Publication date: 3 December 2009

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2008.10.008

zbMATH Keywords

superpositioncombination of theoriesautomated theorem proving: rewritingsatisfiability modulo theories: decision procedures

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)

Related Items (9)

Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ On First-Order Model-Based Reasoning ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Canonical Ground Horn Theories ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ SMELS: satisfiability modulo equality with lazy superposition

Uses Software

• z3
• SIMPLIFY
• Jahob

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• A rewriting approach to satisfiability procedures.
• Modular proof systems for partial functions with Evans equality
• Efficient theory combination via Boolean search
• Decision procedures for extensions of the theory of arrays
• Automated model building
• Rewrite-Based Decision Procedures
• Model-based Theory Combination
• Rewrite-Based Satisfiability Procedures for Recursive Data Structures
• Solving SAT and SAT Modulo Theories
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Engineering DPLL(T) + Saturation
• Simplify: a theorem prover for program checking
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• ${\mathcal{T}}$ -Decision by Decomposition
• Automatic Decidability and Combinability Revisited
• Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
• Simplification by Cooperating Decision Procedures
• Proving Theorems with the Modification Method
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Lazy abstraction
• New results on rewrite-based satisfiability procedures
• Splitting on Demand in SAT Modulo Theories
• Automatic Combinability of Rewriting-Based Satisfiability Procedures
• Automated Deduction – CADE-20
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Frontiers of Combining Systems
• Frontiers of Combining Systems
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Theory decision by decomposition