In intuitionistic logic, the Harrop formulae, named after Ronald Harrop, are the class of formulae inductively defined as follows:[1][2][3] By excluding disjunction and existential quantification (except in the antecedent of implication), non-constructive predicates are avoided, which has benefits for computer implementation.
Harrop formulae are "well-behaved" also in a constructive context.
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.
In one formulation:[4] G-formulae are defined as follows:[4] Harrop formulae were introduced around 1956 by Ronald Harrop and independently by Helena Rasiowa.
[2] Variations of the fundamental concept are used in different branches of constructive mathematics and logic programming.