Theory decision by decomposition
type: Item
instance of: scholarly article
title: Theory decision by decomposition
zbMATH Open document ID: 1192.68626
author: Maria Paola Bonacina
author: Mnacho Echenim
published in: Journal of Symbolic Computation
publication date: 2009-12-03T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5641699
zbMATH Keywords: satisfiability modulo theories: decision procedures
zbMATH Keywords: combination of theories
zbMATH Keywords: automated theorem proving: rewriting
zbMATH Keywords: superposition
describes a project that uses: Jahob
describes a project that uses: z3
describes a project that uses: SIMPLIFY
MaRDI profile type: Publication
full work available at URL: j.jsc.2008.10.008
OpenAlex ID: W1980250820
cites work: New results on rewrite-based satisfiability procedures
cites work: Theory and Applications of Satisfiability Testing
cites work: A rewriting approach to satisfiability procedures.
cites work: Splitting on Demand in SAT Modulo Theories
cites work: Q4804899
cites work: Q4941840
cites work: Rewrite-based decision procedures
cites work: Rewrite-based satisfiability procedures for recursive data structures
cites work: ${\mathcal{T}}$ -Decision by Decomposition
cites work: On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
cites work: Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
cites work: Using First-Order Theorem Provers in the Jahob Data Structure Verification System
cites work: Efficient theory combination via Boolean search
cites work: M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
cites work: Q5310200
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Proving Theorems with the Modification Method
cites work: Q4804887
cites work: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
cites work: Automated model building
cites work: A machine program for theorem-proving
cites work: A Computing Procedure for Quantification Theory
cites work: Efficient E-Matching for SMT Solvers
cites work: Engineering DPLL(T) + Saturation
cites work: Model-based theory combination
cites work: Q4809077
cites work: Rewriting
cites work: Simplify: a theorem prover for program checking
cites work: Modular proof systems for partial functions with Evans equality
cites work: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
cites work: Decision procedures for extensions of the theory of arrays
cites work: Frontiers of Combining Systems
cites work: Lazy abstraction
cites work: Automatic Combinability of Rewriting-Based Satisfiability Procedures
cites work: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
cites work: Automatic Decidability and Combinability Revisited
cites work: SMELS: Satisfiability Modulo Equality with Lazy Superposition
cites work: Computer Aided Verification
cites work: Simplification by Cooperating Decision Procedures
cites work: Solving SAT and SAT Modulo Theories
cites work: Paramodulation-based theorem proving
cites work: Q4345253
cites work: Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
cites work: Q3506045
cites work: Automated Deduction – CADE-20
cites work: Q4809068
DOI: 10.1016/J.JSC.2008.10.008
description: scientific article; zbMATH DE number 5641699