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 (except in the antecedent of implication), 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.

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 (sometimes three) recursive sets of formulae. In one formulation:

G-formulae are defined as follows:

...
Wikipedia