A semantics for λProlog
D. A. Wolfram · Theoretical Computer Science · 1994
We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the λProlog higher-order logic programming language. We define certain intensional general models and show that higher-order Horn clause logic is sound and complete with respect to them.