ausblenden:
Schlagwörter:
-
Zusammenfassung:
This paper presents a Horn clause logic where functions and predicates are \u000Adeclared with polymorphic types. Types are parameterized with type variables. \u000AThis leads to an ML‐like polymorphic type system. A type declaration of a \u000Afunction or predicate restricts the possible use of this function or predicate \u000Aso that only certain terms are allowed to be arguments for this function or \u000Apredicate. The semantic models for polymorphic Horn clause programs are defined \u000Aand a resolution method for this kind of logic programs is given. It will be \u000Ashown that several optimizations in the resolution method are possible for \u000Aspecific kinds of programs. Moreover, it is shown that higher‐order programming \u000Atechniques can be applied in our framework.
