Horn clause programs with polymorphic types: Semantics and resolution (Q1177936)

A Horn clause logic where functions and predicates are declared with polymorphic types is presented. The semantics models for polymorphic Horn clause programs are defined. Deduction and resolution methods for typed logic programs are presented. For several classes of programs, optimizations of the resolution procedure are given. It is shown that higher-order programming techniques can be applied in the framework.