Canonical Ground Horn Theories
From MaRDI portal
Publication:4916071
DOI10.1007/978-3-642-37651-1_3zbMath1383.03042MaRDI QIDQ4916071
Maria Paola Bonacina, Nachum Dershowitz
Publication date: 19 April 2013
Published in: Programming Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_3
canonical systems; normal forms; Horn theories; redundancy; saturation; Moore families; decision procedures; conditional theories
03B70: Logic in computer science
03B35: Mechanization of proofs and logical operations
68Q42: Grammars and rewriting systems
Related Items
Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Conditional congruence closure over uninterpreted and interpreted symbols, SGGS decision procedures, Set of support, demodulation, paramodulation: a historical perspective, Canonicity!
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On deciding satisfiability by theorem proving with speculative inferences
- Towards a foundation of completion procedures as semidecision procedures
- On word problems in Horn theories
- A completion procedure for conditional equations
- Refutational theorem proving using term-rewriting systems
- Theory decision by decomposition
- Rewrite method for theorem proving in first order theory with equality
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
- A note on simplification orderings
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Complexity and related enhancements for automated theorem-proving programs
- Theory reasoning in connection calculi
- Deductive and inductive synthesis of equational programs
- A new method for the Boolean ring based theorem proving
- A rewriting approach to satisfiability procedures.
- Abstract congruence closure
- Automated deduction by theory resolution
- Proof lengths for equational completion
- Abstract canonical presentations
- Rewrite-Based Satisfiability Procedures for Recursive Data Structures
- Computing with rewrite systems
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Existence, Uniqueness, and Construction of Rewrite Systems
- Proving termination with multiset orderings
- On rewrite programs: Semantics and relationship with prolog
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- Equational inference, canonical proofs, and proof orderings
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- The integration of functions into logic programming: From theory to practice
- Abstract canonical inference
- New results on rewrite-based satisfiability procedures
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Completion Is an Instance of Abstract Canonical System Inference
- On sentences which are true of direct unions of algebras
- The decision problem for some classes of sentences without quantifiers
