<p>You should have a look at <a href="http://www.lix.polytechnique.fr/~dale/papers/apal91.pdf">Uniform Proofs as a Foudation for Logic Programming</a> by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has seen spawn from these ideas is to understand the execution of a logic program as proof search in simple and expressive logics, such as intuitionistic logic or linear logic. A particular class of formulas with good proof search properties are the Hereditary Harrop Formulas, which nicely generalize Horn Clauses.</p>

CC BY-SA 4.0
2020-12-06T22:50:05.537Z
I'm curious: Does implementing the Hereditary Harrop formulas require a type system in a language? The only system I know of that implements them is λProlog, which is typed.
MWB
CC BY-SA 4.0
2020-12-12T08:07:45.390Z
No, I don't think a type system is necessary -- just like for Horn Clauses.
gasche
CC BY-SA 4.0
2020-12-12T12:02:11.973Z
I should have said "Higher-order Hereditary Harrop formulas"
MWB
CC BY-SA 4.0
2020-12-13T13:11:55.960Z
The higher-order aspect basically embeds a lambda-calculus whose base type is a formula of the logic. You can have a lambda-calculus in an untyped programming language.
gasche
CC BY-SA 3.0
2016-02-07T18:43:10.600Z
2016-02-07T18:43:10.600Z
gasche
<p>There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there formal methods that can help specify and verify Horn clauses. Is there semantics of Horn clauses. One can perceive Horn clauses as something similar to programming code of traditional programming languages and therefore one can expect the denotation, operational and similar semantics as well for Horn clauses.</p>

<lo.logic><pl.programming-languages><semantics><logic-programming>
How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses
TomR
# How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses

(Asked by: username_0 on 2016-02-07)

There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there formal methods that can help specify and verify Horn clauses. Is there semantics of Horn clauses. One can perceive Horn clauses as something similar to programming code of traditional programming languages and therefore one can expect the denotation, operational and similar semantics as well for Horn clauses.

**Tags:** lo.logic, pl.programming-languages, semantics, logic-programming

---

## 1 answers

### Answer by username_1 on 2016-02-07. Score: 6 | Accepted answer

You should have a look at [Uniform Proofs as a Foudation for Logic Programming](http://www.lix.polytechnique.fr/~dale/papers/apal91.pdf) by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has seen spawn from these ideas is to understand the execution of a logic program as proof search in simple and expressive logics, such as intuitionistic logic or linear logic. A particular class of formulas with good proof search properties are the Hereditary Harrop Formulas, which nicely generalize Horn Clauses.

> **Comments:**
> **username_2**: I'm curious: Does implementing the Hereditary Harrop formulas require a type system in a language? The only system I know of that implements them is λProlog, which is typed.  
> **username_1**: No, I don't think a type system is necessary -- just like for Horn Clauses.  
> **username_2**: I should have said "Higher-order Hereditary Harrop formulas"  
> **username_1**: The higher-order aspect basically embeds a lambda-calculus whose base type is a formula of the logic. You can have a lambda-calculus in an untyped programming language.  

---

