A rewriting approach to satisfiability procedures.
From MaRDI portal
Publication:1401930
DOI10.1016/S0890-5401(03)00020-8zbMath1054.68077OpenAlexW2156915267MaRDI QIDQ1401930
Alessandro Armando, Silvio Ranise, Michaël Rusinowitch
Publication date: 19 August 2003
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0890-5401(03)00020-8
Automated deductionEquational logicTerm rewritingEncryptionHomomorphismDecision proceduresSuperpositionArrays with extensionalityFinite sets with extensionalityLists
Related Items
Interpolation systems for ground proofs in automated deduction: a survey, Adding decision procedures to SMT solvers using axioms with triggers, Modular Termination and Combinability for Superposition Modulo Counter Arithmetic, Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005), Solving linear optimization over arithmetic constraint formula, Metalevel algorithms for variant satisfiability, Equational Theorem Proving for Clauses over Strings, A Rewriting Approach to the Combination of Data Structures with Bridging Theories, Modular proof systems for partial functions with Evans equality, Superposition decides the first-order logic fragment over ground theories, On deciding satisfiability by theorem proving with speculative inferences, An instantiation scheme for satisfiability modulo theories, SMELS: Satisfiability Modulo Equality with Lazy Superposition, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Decision procedures for extensions of the theory of arrays, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Canonical Ground Horn Theories, Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs, Automatic decidability and combinability, A superposition calculus for abductive reasoning, On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving, Combinable Extensions of Abelian Groups, Locality Results for Certain Extensions of Theories with Bridging Functions, Variant-Based Satisfiability in Initial Algebras, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Politeness and combination methods for theories with bridging functions, Metalevel Algorithms for Variant Satisfiability, Data Structures with Arithmetic Constraints: A Non-disjoint Combination, Theory decision by decomposition, Combination of convex theories: modularity, deduction completeness, and explanation, Rewrite-Based Decision Procedures, Rewrite-Based Satisfiability Procedures for Recursive Data Structures, SMELS: satisfiability modulo equality with lazy superposition, On interpolation in automated theorem proving
Uses Software
Cites Work
- Towards a foundation of completion procedures as semidecision procedures
- Theorem-proving with resolution and superposition
- On word problems in Horn theories
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Any ground associative-commutative theory has a finite canonical system
- Proof lengths for equational completion
- Automated complexity analysis based on ordered resolution
- Deciding Combinations of Theories
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Variations on the Common Subexpression Problem
- THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLE
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Shostak's congruence closure as completion
- Completion procedures as semidecision procedures
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
