scientific article

zbMath0585.68048MaRDI QIDQ3709891

Stéphane Kaplan

Publication date: 1985

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

finite terminationsimplification orderingKnuth-Bendix-like completion procedurerewriting procedureunification by narrowing

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Related Items

On solving the equality problem in theories defined by Horn clauses, Kernel-LEAF: A logic plus functional language, History and basic features of the critical-pair/completion procedure, Automatic inductive theorem proving using Prolog, Narrowing vs. SLD-resolution, Conditional rewrite rules: Confluence and termination, Incremental constraint satisfaction for equational logic programming, Conditional equational theories and complete sets of transformations, Order-sorted completion: The many-sorted way, Efficient deduction in equality Horn logic by Horn-completion, Dynamic detection of determinism in functional logic languages, Conditional narrowing modulo a set of equations, Complete sets of transformations for general E-unification, A completion procedure for conditional equations, A strong restriction of the inductive completion procedure, Basic narrowing revisited, Contextual rewriting as a sound and complete proof method for conditional LOG-specifications