# Harrop formula

In intuitionistic logic, the **Harrop formulae**, named after Ronald Harrop, are the class of formulae inductively defined as follows:^{[1]}^{[2]}^{[3]}

- Atomic formulae are Harrop, including falsity (⊥);

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:^{[1]}

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.

## 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 (sometimes three) recursive sets of formulae. In one formulation:^{[4]}

*G*-formulae are defined as follows:^{[4]}

- Atomic formulae are
*G*-formulae, including truth(⊤);

## References

- ↑
^{1.0}^{1.1}{{#invoke:citation/CS1|citation |CitationClass=book }} - ↑
^{2.0}^{2.1}{{#invoke:citation/CS1|citation |CitationClass=book }} - ↑ {{#invoke:Citation/CS1|citation |CitationClass=journal }}
- ↑
^{4.0}^{4.1}Dov M. Gabbay, Christopher John Hogger, John Alan Robinson,*Handbook of Logic in Artificial Intelligence and Logic Programming: Logic programming*, Oxford University Press, 1998, p 575, ISBN 0-19-853792-1