Dissertation, Universitaet Dortmund, 1988
This thesis presents a Horn clause logic with equality where functions and predicates are declared with polymorphic types. Types are parameterized with type variables. This leads to an ML-like polymorphic type system. A type declaration of a function or predicate restricts the possible use of this function or predicate so that only certain terms are allowed to be arguments for this function or predicate. The semantic models of polymorphic Horn clause specifications are defined and several proof methods (deduction, resolution, paramodulation, rewriting and narrowing) for this kind of specifications are given. Moreover, it is shown that higher-order programming techniques can be applied in our framework.
Available: DVI BibTeX-Entry