February 13, 2014
The two prominent declarative paradigms, namely logic and functional programming differ radically in an important aspect: logic programming is traditionally first-order while functional programming encourages and promotes the use of higher-order functions and constructs.
We consider an extensional higher-order logic programming language where predicates can be passed as parameters. Every higher-order logic program has a unique minimum Herbrand model. In this semantics program predicates denote sets of ordered tuples and two predicates are equal iff they are equal as sets.
We propose an SLD-resolution proof procedure and we demonstrate that it is sound and complete with respect to this semantics. In this way, we extend the familiar proof theory of first-order logic programming to apply to the more general higher-order case.
We then enhance our source language with constructive negation and extend the aforementioned proof procedure
to support this new feature. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas.