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

Goguen, Joseph A.; Meseguer, José

J. Logic Program. 1, 179-210 (1984).

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.

Reviewer: G. E. Mints (Leningrad)

MSC:

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

Keywords:

extension of PROLOG; Eqlog; equality; sorts; modules; pre-programmed sets of Horn clauses; completeness theorem