An Efficient Unification Algorithm
Copyright policy )An Efficient Unification Algorithm
The unification problem in f'mst-order predicate calculus is described in general terms as the solution of a system of equations, and a nondeterministic algorithm is given. A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given. A comparison with other well-known unification algorithms shows that the algorithm described here performs well in all cases.
- University of Turin Italy
- University of Pisa Italy
Complexity of proofs, Mechanization of proofs and logical operations, nondeterministic algorithm, mechanical theorem proving, unification problem, resolution, Classical first-order logic, complexity of proof procedures, Theorem proving (deduction, resolution, etc.)
Complexity of proofs, Mechanization of proofs and logical operations, nondeterministic algorithm, mechanical theorem proving, unification problem, resolution, Classical first-order logic, complexity of proof procedures, Theorem proving (deduction, resolution, etc.)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).506 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 1% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 0.1% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!