@prefix foaf: .
@prefix dbpedia: .
@prefix ns2: .
dbpedia:Harrop_formula foaf:page ns2:Harrop_formula .
@prefix dbpprop: .
dbpedia:Harrop_formula dbpprop:reference ,
.
@prefix rdfs: .
dbpedia:Harrop_formula rdfs:label "Harrop formula"@en ;
dbpprop:abstract "In intuitionistic logic, the Harrop formulae, named after Ronald Harrop, are the class of formulae inductively defined as follows: Atomic formulae are Harrop, including falsity (\u22A5); <math>A \\wedge B</math> is Harrop provided <math>A</math> and <math>B</math> are; <math>\\neg A</math> is Harrop provided <math>A</math> is; <math>F \\rightarrow A</math> is Harrop provided <math>A</math> is, and <math>F</math> is any well-formed formula; <math>\\forall x. A</math> is Harrop provided <math>A</math> is. 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: <math>A \\leftrightarrow \\neg \\neg A</math> 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."@en ;
rdfs:comment ""@en .
@prefix skos: .
@prefix ns6: .
dbpedia:Harrop_formula skos:subject ns6:Logic ,
ns6:Mathematical_logic ,
ns6:Mathematical_constructivism .