Canonical Ground Horn Theories

DOI10.1007/978-3-642-37651-1_3zbMath1383.03042OpenAlexW64666703MaRDI 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

zbMATH Keywords

canonical systemsnormal formsHorn theoriesredundancysaturationMoore familiesdecision proceduresconditional theories

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (5)

Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Canonicity! ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ SGGS decision procedures ⋮ Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• OEIS

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

This page was built for publication: Canonical Ground Horn Theories