scientific article
From MaRDI portal
Publication:4000281
zbMath0732.68094MaRDI QIDQ4000281
Publication date: 23 January 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
theorem provingproof normalizationcompletion methodconvergent rewrite techniquesreasoning about equations
Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items
A maximal-literal unit strategy for horn clauses, Deciding confluence of certain term rewriting systems in polynomial time, On how to move mountains ‘associatively and commutatively’, Open problems in rewriting, Improving transformation systems for general E-unification, Problems in rewriting applied to categorical concepts by the example of a computational comonad, Structures for abstract rewriting, Multi-completion with termination tools, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, Buchberger's algorithm: A constraint-based completion procedure, Rational rewriting, Unnamed Item, Towards automated deduction in cP systems, Dynamically-typed computations for order-sorted equational presentations, What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory, Redundancy criteria for constrained completion, Rewrite semantics for production rule systems: Theory and applications, On weakly confluent monadic string-rewriting systems, From Search to Computation: Redundancy Criteria and Simplification at Work, Citius altius fortius, How to decide the lark, Redundancy criteria for constrained completion, On interreduction of semi-complete term rewriting systems, Identification of proofs via syzygies, Completion for multiple reduction orderings, Mechanizable inductive proofs for a class of ∀ ∃ formulas, Unnamed Item, Termination of rewrite systems by elementary interpretations, Extending Maximal Completion (Invited Talk), Knuth-Bendix Completion for Non-Symmetric Transitive Relations, Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols, Induction = I-axiomatization + first-order consistency., Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, The equational part of proofs by structural induction, Automated modular termination proofs for real Prolog programs
