Theory decision by decomposition (Q1041591): Difference between revisions

@@ Property / DOI @@
-.1016/j.jsc.2008.10.008
@@ Property / DOI: 10.1016/j.jsc.2008.10.008 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+SIMPLIFY
@@ Property / describes a project that uses: SIMPLIFY / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.jsc.2008.10.008
+Normal rank
@@ Property / OpenAlex ID @@
+W1980250820
@@ Property / OpenAlex ID: W1980250820 / rank @@
+Normal rank
@@ Property / cites work @@
+New results on rewrite-based satisfiability procedures
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+A rewriting approach to satisfiability procedures.
+Normal rank
@@ Property / cites work @@
+Splitting on Demand in SAT Modulo Theories
@@ Property / cites work: Splitting on Demand in SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804899
@@ Property / cites work: Q4804899 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4941840
@@ Property / cites work: Q4941840 / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-Based Decision Procedures
@@ Property / cites work: Rewrite-Based Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-Based Satisfiability Procedures for Recursive Data Structures
+Normal rank
@@ Property / cites work @@
+${\mathcal{T}}$ -Decision by Decomposition
@@ Property / cites work: ${\mathcal{T}}$ -Decision by Decomposition / rank @@
+Normal rank
@@ Property / cites work @@
+On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
+Normal rank
@@ Property / cites work @@
+Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
+Normal rank
@@ Property / cites work @@
+Using First-Order Theorem Provers in the Jahob Data Structure Verification System
+Normal rank
@@ Property / cites work @@
+Efficient theory combination via Boolean search
@@ Property / cites work: Efficient theory combination via Boolean search / rank @@
+Normal rank
@@ Property / cites work @@
+M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
+Normal rank
@@ Property / cites work @@
+Q5310200
@@ Property / cites work: Q5310200 / rank @@
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Proving Theorems with the Modification Method
@@ Property / cites work: Proving Theorems with the Modification Method / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804887
@@ Property / cites work: Q4804887 / rank @@
+Normal rank
@@ Property / cites work @@
+Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
+Normal rank
@@ Property / cites work @@
+Automated model building
@@ Property / cites work: Automated model building / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering DPLL(T) + Saturation
@@ Property / cites work: Engineering DPLL(T) + Saturation / rank @@
+Normal rank
@@ Property / cites work @@
+Model-based Theory Combination
@@ Property / cites work: Model-based Theory Combination / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809077
@@ Property / cites work: Q4809077 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751361
@@ Property / cites work: Q2751361 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Modular proof systems for partial functions with Evans equality
+Normal rank
@@ Property / cites work @@
+Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Decision procedures for extensions of the theory of arrays
+Normal rank
@@ Property / cites work @@
+Frontiers of Combining Systems
@@ Property / cites work: Frontiers of Combining Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy abstraction
@@ Property / cites work: Lazy abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Combinability of Rewriting-Based Satisfiability Procedures
+Normal rank
@@ Property / cites work @@
+Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
+Normal rank
@@ Property / cites work @@
+Frontiers of Combining Systems
@@ Property / cites work: Frontiers of Combining Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Decidability and Combinability Revisited
+Normal rank
@@ Property / cites work @@
+SMELS: Satisfiability Modulo Equality with Lazy Superposition
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4345253
@@ Property / cites work: Q4345253 / rank @@
+Normal rank
@@ Property / cites work @@
+Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
+Normal rank
@@ Property / cites work @@
+Q3506045
@@ Property / cites work: Q3506045 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809068
@@ Property / cites work: Q4809068 / rank @@
+Normal rank
@@ Property / DOI @@
+.1016/J.JSC.2008.10.008
@@ Property / DOI: 10.1016/J.JSC.2008.10.008 / rank @@
+Normal rank