Automatic decidability and combinability
From MaRDI portal
Publication:549666
DOI10.1016/J.IC.2011.03.005zbMATH Open1216.68163OpenAlexW1998734164WikidataQ118190406 ScholiaQ118190406MaRDI QIDQ549666FDOQ549666
Authors: Yong-Cai Geng, Sumit K. Garg 
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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cites Work
- Simplify: a theorem prover for program checking
- Simplification by Cooperating Decision Procedures
- Renaming a Set of Clauses as a Horn Set
- A rewriting approach to satisfiability procedures.
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Automatic recognition of tractability in inference relations
- Combining nonstably infinite theories
- Title not available (Why is that?)
- Theorem proving in cancellative abelian monoids (extended abstract)
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Paramodulation-based theorem proving
- Automated complexity analysis based on ordered resolution
- Automatic Decidability and Combinability Revisited
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Title not available (Why is that?)
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- Frontiers of Combining Systems
- Superposition theorem proving for abelian groups represented as integer modules
- Superposition with completely built-in abelian groups
- Reasoning About Recursively Defined Data Structures
- Title not available (Why is that?)
- Theoretical Aspects of Computing – ICTAC 2005
- Frontiers of Combining Systems
- Theoretical Aspects of Computing - ICTAC 2004
- Polynomial-time computation via local inference relations
- Logic and structure.
Cited In (10)
- Self-assembly of decidable sets
- Modular termination and combinability for superposition modulo counter arithmetic
- A superposition calculus for abductive reasoning
- Automatic decidability: a schematic calculus for theories with counting operators
- Combined Satisfiability Modulo Parametric Theories
- Adding decision procedures to SMT solvers using axioms with triggers
- SMELS: satisfiability modulo equality with lazy superposition
- Modular instantiation schemes
- Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
- Automatic Decidability and Combinability Revisited
Uses Software
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)
