Equality, types, modules, and (why not?) generics for logic programming. (English) Zbl 0575.68091

The system Eqlog suggested in this paper extends Prolog by equality, sorts (with subsort relation) and modules, i.e. pre-programmed sets of Horn clauses (axioms for specific sorts like ”natural” or ”rational”) to be included into the program. Implementation is only planned, but the completeness theorem is stated for the case when clauses containing equality are pure equations and the equality relation determined by these equations read as rewrite rules is confluent and terminating (that is, strongly normalizable). Slightly more general completeness theorems are conjectured.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI