Harrop formula


In intuitionistic logic, the Harrop formulae, named after Ronald Harrop, are the class of formulae inductively defined as follows:
By excluding disjunction and existential quantification, non-constructive predicates are avoided, which has benefits for computer implementation. From a constructivist point of view, Harrop formulae are "well-behaved." For example, in Heyting arithmetic, Harrop formulae satisfy a classical equivalence not usually satisfied in constructive logic:
Harrop formulae were introduced around 1956 by Ronald Harrop and independently by Helena Rasiowa. Variations of the fundamental concept are used in different branches of constructive mathematics and logic programming.

Hereditary Harrop formulae and logic programming

A more complex definition of hereditary Harrop formulae is used in logic programming as a generalisation of Horn clauses, and forms the basis for the language λProlog. Hereditary Harrop formulae are defined in terms of two recursive sets of formulae. In one formulation:
G-formulae are defined as follows: