On deciding satisfiability by theorem proving with speculative inferences
From MaRDI portal
(Redirected from Publication:438533)
Recommendations
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- An Abstract Framework for Satisfiability Modulo Theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- SMELS: satisfiability modulo equality with lazy superposition
- Foundations of satisfiability modulo theories
Cites work
- scientific article; zbMATH DE number 1418280 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- ${\mathcal{T}}$ -Decision by Decomposition
- A Computing Procedure for Quantification Theory
- A Decision Procedure for Monotone Functions over Bounded and Complete Lattices
- A Machine-Oriented Logic Based on the Resolution Principle
- A decidable class of nested iterated schemata
- A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
- A machine program for theorem-proving
- A rewriting approach to satisfiability procedures.
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- Automated Deduction – CADE-20
- Automated Inference of Finite Unsatisfiability
- Automated complexity analysis based on ordered resolution
- Automated model building
- Automated reasoning in some local exensions of ordered structures
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combining theories with shared set operations
- Computer Aided Verification
- Computer Science Logic
- Data structures with arithmetic constraints: A non-disjoint combination
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Efficient E-Matching for SMT Solvers
- Engineering DPLL(T) + Saturation
- Frontiers of Combining Systems
- Integrating Linear Arithmetic into Superposition Calculus
- Lazy satisfiability modulo theories
- Model-based theory combination
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- On Local Reasoning in Verification
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- On word problems in Horn theories
- Orderings for term-rewriting systems
- Paramodulation-based theorem proving
- Presburger arithmetic with unary predicates is Π11 complete
- Proving refutational completeness of theorem-proving strategies
- Proving termination with multiset orderings
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Rewrite-based decision procedures
- Rewrite-based satisfiability procedures for recursive data structures
- Simplification by Cooperating Decision Procedures
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Superposition modulo linear arithmetic SUP(LA)
- Theorem-proving with resolution and superposition
- Theory decision by decomposition
- Towards a foundation of completion procedures as semidecision procedures
- Verification, Model Checking, and Abstract Interpretation
Cited in
(23)- SGGS decision procedures
- Towards a Semantics of Unsatisfiability Proofs with Inprocessing
- On interpolation in decision procedures
- Quantifier simplification by unification in SMT
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Semantically-guided goal-sensitive reasoning: model representation
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Theorem proving in large formal mathematics as an emerging AI field
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Disproving using the inverse method by iterative refinement of finite approximations
- Rewriting modulo SMT and open system analysis
- Superposition decides the first-order logic fragment over ground theories
- On First-Order Model-Based Reasoning
- Superposition for bounded domains
- Canonical ground Horn theories
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Proving infinite satisfiability
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Blocking and other enhancements for bottom-up model generation methods
- On interpolation in automated theorem proving
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Making theory reasoning simpler
This page was built for publication: On deciding satisfiability by theorem proving with speculative inferences
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438533)
