Automatic decidability and combinability
From MaRDI portal
Publication:549666
DOI10.1016/J.IC.2011.03.005zbMATH Open1216.68163OpenAlexW1998734164WikidataQ118190406 ScholiaQ118190406MaRDI QIDQ549666FDOQ549666
Recommendations
Cites work
- scientific article; zbMATH DE number 1303342 (Why is no real title available?)
- scientific article; zbMATH DE number 1140674 (Why is no real title available?)
- scientific article; zbMATH DE number 2090529 (Why is no real title available?)
- A rewriting approach to satisfiability procedures.
- Automated complexity analysis based on ordered resolution
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- Automatic Decidability and Combinability Revisited
- Automatic recognition of tractability in inference relations
- Combining nonstably infinite theories
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Frontiers of Combining Systems
- Frontiers of Combining Systems
- Logic and structure.
- Paramodulation-based theorem proving
- Polynomial-time computation via local inference relations
- Reasoning About Recursively Defined Data Structures
- Renaming a Set of Clauses as a Horn Set
- Simplification by Cooperating Decision Procedures
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Superposition theorem proving for abelian groups represented as integer modules
- Superposition with completely built-in abelian groups
- Theorem proving in cancellative abelian monoids (extended abstract)
- Theoretical Aspects of Computing - ICTAC 2004
- Theoretical Aspects of Computing – ICTAC 2005
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
Cited in
(10)- SMELS: satisfiability modulo equality with lazy superposition
- Automatic Decidability and Combinability Revisited
- Adding decision procedures to SMT solvers using axioms with triggers
- Modular termination and combinability for superposition modulo counter arithmetic
- Automatic decidability: a schematic calculus for theories with counting operators
- Combined Satisfiability Modulo Parametric Theories
- Modular instantiation schemes
- Self-assembly of decidable sets
- A superposition calculus for abductive reasoning
- Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
This page was built for publication: Automatic decidability and combinability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q549666)
