Refutational theorem proving using term-rewriting systems

DOI10.1016/0004-3702(85)90074-8zbMath0558.68072OpenAlexW2019751493WikidataQ56039144 ScholiaQ56039144MaRDI QIDQ802317

Publication date: 1985

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: http://ntur.lib.ntu.edu.tw/bitstream/246246/118462/-1/20.pdf

zbMATH Keywords

Boolean algebra first-order logic equational logic

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Foundations of classical theories (including reverse mathematics) (03B30) Ring-theoretic properties of Boolean algebras (06E20) Word problems (aspects of algebraic structures) (08A50)

Related Items

Could orders be captured by term rewriting systems? ⋮ Completion procedures as semidecision procedures ⋮ Gordon's computer: A hardware verification case study in OBJ3 ⋮ 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 ⋮ A Groebner bases-based approach to backward reasoning in rule based expert systems ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Rewrite method for theorem proving in first order theory with equality ⋮ Embedding Boolean expressions into logic programming ⋮ Automatic inductive theorem proving using Prolog ⋮ Structures for abstract rewriting ⋮ Critical pair criteria for completion ⋮ Unification in Boolean rings ⋮ Modular algebraic specification of some basic geometrical constructions ⋮ A refutational approach to geometry theorem proving ⋮ Ordered Binary Decision Diagrams and the Davis-Putnam procedure ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ A Gröbner bases-based rule based expert system for fibromyalgia diagnosis ⋮ A new algebraic model for implementing expert systems represented under the `concept-attribute-value' paradigm ⋮ Towards automated deduction in cP systems ⋮ A polynomial model for logics with a prime power number of truth values ⋮ The \(Multi\)-SAT algorithm ⋮ 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 ⋮ Fuzzy term-rewriting system ⋮ A portable knowledge-based system for car breakdown evaluation ⋮ A prototype of a RBES for personalized menus generation ⋮ POLYNOMIAL RING CALCULUS FOR MODAL LOGICS: A NEW SEMANTICS AND PROOF METHOD FOR MODALITIES ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications ⋮ Discriminator varieties and symbolic computation ⋮ A logic-algebraic tool for reasoning with knowledge-based systems ⋮ The problem of demodulator adjunction ⋮ Canonical Ground Horn Theories ⋮ Subsumption computed algebraically ⋮ 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 ⋮ Unnamed Item ⋮ An algebraic approach to rule based expert systems ⋮ On Theorem Proving in Annotated Logics ⋮ Completion for rewriting modulo a congruence ⋮ On conversions from CNF to ANF ⋮ On the relation between resolution based and completion based theorem proving ⋮ Theorem proving by chain resolution ⋮ CWA Extensions to Multi-Valued Logics ⋮ Boolean unification - the story so far ⋮ Linear strategy for Boolean ring based theorem proving ⋮ A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple ⋮ Partial completion of equational theories ⋮ Multi-valued logic and Gröbner bases with applications to modal logic ⋮ An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics ⋮ Termination orderings for associative-commutative rewriting systems ⋮ An expert system for managing medical appropriateness criteria based on computer algebra techniques

Uses Software

REVE

Cites Work