Publication:3709891
From MaRDI portal
zbMath0585.68048MaRDI QIDQ3709891
Publication date: 1985
finite termination; simplification ordering; Knuth-Bendix-like completion procedure; rewriting procedure; unification by narrowing
68W30: Symbolic computation and algebraic computation
68Q65: Abstract data types; algebraic specification
Related Items
Dynamic detection of determinism in functional logic languages, A completion procedure for conditional equations, Conditional equational theories and complete sets of transformations, On solving the equality problem in theories defined by Horn clauses, 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, Order-sorted completion: The many-sorted way, Efficient deduction in equality Horn logic by Horn-completion, Conditional narrowing modulo a set of equations, Complete sets of transformations for general E-unification, Contextual rewriting as a sound and complete proof method for conditional LOG-specifications, Incremental constraint satisfaction for equational logic programming, A strong restriction of the inductive completion procedure, Basic narrowing revisited, Kernel-LEAF: A logic plus functional language
