Refutational theorem proving using term-rewriting systems
The paper proposes a new approach to theorem proving in first-order logic based on term-rewriting systems. First, for propositional calculus a canonical term-rewriting system for Boolean algebra is introduced. The key point enabling successful construction of the canonical term- rewriting system (in contrast with all the previous attempts that failed due to the fact that the prime implicant representation of Boolean terms is not unique) consists in choosing exclusive or instead of or. The canonical system for Boolean algebra enables transformation of the first- order calculus into a form of equational logic and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix completion algorithm. These strategies deal with predicate logic and built-in (equational) theories in a uniform and quite efficient way. Comparison of implementation of a theorem prover based on term-rewriting with other theorem provers based on locking reduction or natural deduction shows that the method proposed is in general much more efficient then the methods based on resolution. Great efficiency and easy modifiability of a theorem prover based on the term-rewriting method makes the method a serious counterpart to resolution and it will probably have significant impact on theorem proving.
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A Machine-Oriented Logic Based on the Resolution Principle
- A simplified problem reduction format
- A Unification Algorithm for Associative-Commutative Functions
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Complete Sets of Reductions for Some Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Computer-Implemented Set Theory
- Experiment with an automatic theorem-prover having partial ordering inference rules
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 3871334 (Why is no real title available?)
- scientific article; zbMATH DE number 3810909 (Why is no real title available?)
- scientific article; zbMATH DE number 3936507 (Why is no real title available?)
- scientific article; zbMATH DE number 3981150 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3550181 (Why is no real title available?)
- scientific article; zbMATH DE number 3566230 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3310921 (Why is no real title available?)
- scientific article; zbMATH DE number 3346109 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- New decision algorithms for finitely presented commutative semigroups
- Non-resolution theorem proving
- Orderings for term-rewriting systems
- Proving Theorems with the Modification Method
- Theorem-Proving on the Computer
- Termination orderings for associative-commutative rewriting systems
- Rewrite method for theorem proving in first order theory with equality
- Embedding Boolean expressions into logic programming
- Automatic inductive theorem proving using Prolog
- Critical pair criteria for completion
- Unification in Boolean rings
- Modular algebraic specification of some basic geometrical constructions
- A refutational approach to geometry theorem proving
- Fuzzy term-rewriting system
- Discriminator varieties and symbolic computation
- Subsumption computed algebraically
- Completion for rewriting modulo a congruence
- Theorem proving by chain resolution
- Refutational theorem proving for hierarchic first-order theories
- Gordon's computer: A hardware verification case study in OBJ3
- Buchberger's algorithm: The term rewriter's point of view
- Linear strategy for Boolean ring based theorem proving
- Partial completion of equational theories
- An expert system for managing medical appropriateness criteria based on computer algebra techniques
- A prototype of a RBES for personalized menus generation
- Use of logical models for proving infeasibility in term rewriting
- Boolean unification - the story so far
- A Gröbner bases-based rule based expert system for fibromyalgia diagnosis
- The Multi-SAT algorithm
- A logic-algebraic tool for reasoning with knowledge-based systems
- An algebraic model for implementing expert systems based on the knowledge of different experts
- A natural language for implementing algebraically expert systems
- An algebraic approach for detecting nearly dangerous situations in expert systems
- Revisiting four-valued logics from \textit{Maple} using the \textit{Logics Explorer} package
- On conversions from CNF to ANF
- A Groebner bases-based approach to backward reasoning in rule based expert systems
- A polynomial model for logics with a prime power number of truth values
- Structures for abstract rewriting
- Rewriting-based verification of authentication protocols
- A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules
- Polynomial ring calculus for modal logics: a new semantics and proof method for modalities
- scientific article; zbMATH DE number 4203770 (Why is no real title available?)
- CWA extensions to multi-valued logics
- scientific article; zbMATH DE number 3930371 (Why is no real title available?)
- scientific article; zbMATH DE number 4074536 (Why is no real title available?)
- A new algebraic model for implementing expert systems represented under the `concept-attribute-value' paradigm
- An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- scientific article; zbMATH DE number 2016837 (Why is no real title available?)
- On Theorem Proving in Annotated Logics
- Canonical ground Horn theories
- Conditional rewrite rule systems with built-in arithmetic and induction
- Boolean algebra admits no convergent term rewriting system
- Incremental techniques for efficient normalization of nonlinear rewrite systems
- Open problems in rewriting
- Proving and rewriting
- Ordered binary decision diagrams and the Davis-Putnam procedure
- Buchberger's algorithm: a constraint-based completion procedure
- Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple
- Could orders be captured by term rewriting systems?
- Completion procedures as semidecision procedures
- Towards automated deduction in cP systems
- An inference engine for propositional two-valued logic based on the radical membership problem
- A portable knowledge-based system for car breakdown evaluation
- Towards a foundation of completion procedures as semidecision procedures
- The problem of demodulator adjunction
- The Logics' Explorer: a Maple package for exploring finite many-valued propositional logics
- A logic-algebraic approach to decision taking in a railway interlocking system
- On the relation between resolution based and completion based theorem proving
- Multi-valued logic and Gröbner bases with applications to modal logic
- An algebraic approach to rule based expert systems
This page was built for publication: Refutational theorem proving using term-rewriting systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q802317)
