New results on rewrite-based satisfiability procedures
From MaRDI portal
Publication:5277822
DOI10.1145/1459010.1459014zbMath1367.68243arXivcs/0604054OpenAlexW2084417024WikidataQ118123555 ScholiaQ118123555MaRDI QIDQ5277822
Silvio Ranise, Stephan Schulz, Alessandro Armando, Maria Paola Bonacina
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/cs/0604054
automated reasoningscalabilitysuperpositionrewritinginferenceterminationdecision procedurescombination of theoriessatisfiability modulo a theory
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)
Related Items
Interpolation systems for ground proofs in automated deduction: a survey ⋮ Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited ⋮ Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ Weakly Equivalent Arrays ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ Superposition as a decision procedure for timed automata ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ Engineering DPLL(T) + Saturation ⋮ Superposition for Bounded Domains ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Canonical Ground Horn Theories ⋮ A superposition calculus for abductive reasoning ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Combinable Extensions of Abelian Groups ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ Satisfiability Procedures for Combination of Theories Sharing Integer Offsets ⋮ Politeness and combination methods for theories with bridging functions ⋮ Unification modulo lists with reverse relation with certain word equations ⋮ Superposition Modulo Linear Arithmetic SUP(LA) ⋮ Data Structures with Arithmetic Constraints: A Non-disjoint Combination ⋮ Theory decision by decomposition ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ On interpolation in automated theorem proving
Uses Software
