Automatic decidability and combinability
From MaRDI portal
Publication:549666
DOI10.1016/j.ic.2011.03.005zbMath1216.68163OpenAlexW1998734164WikidataQ118190406 ScholiaQ118190406MaRDI QIDQ549666
Publication date: 18 July 2011
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2011.03.005
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Adding decision procedures to SMT solvers using axioms with triggers ⋮ Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ A superposition calculus for abductive reasoning ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols ⋮ SMELS: satisfiability modulo equality with lazy superposition
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Combining nonstably infinite theories
- Superposition theorem proving for abelian groups represented as integer modules
- A rewriting approach to satisfiability procedures.
- Superposition with completely built-in abelian groups
- Automated complexity analysis based on ordered resolution
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Automatic Decidability and Combinability Revisited
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Simplification by Cooperating Decision Procedures
- Reasoning About Recursively Defined Data Structures
- Renaming a Set of Clauses as a Horn Set
- Theorem proving in cancellative abelian monoids (extended abstract)
- Automatic recognition of tractability in inference relations
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- Theoretical Aspects of Computing – ICTAC 2005
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Frontiers of Combining Systems
- Frontiers of Combining Systems
- Theoretical Aspects of Computing - ICTAC 2004
- Polynomial-time computation via local inference relations
- Logic and structure.
This page was built for publication: Automatic decidability and combinability
