First-Order Hereditary Harrop Formulas
A logic programming language that is based on the logic of first-order Horn clauses or
fohc does not make very strong use of the structure afforded by logic in general even while providing significant computational capabilities. Part of this weakness arises from the fact that goal formulas and the bodies of program clauses in the setting of
fohc, are not permitted to contain implications and universal quantifiers. In the first section of this chapter, we introduce the logic of first-order hereditary Harrop formulas, or
fohh, that eases this restriction. The computational interpretation of these additional logical symbols then leads to a logic programming language in which programs and signatures can grow ...