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.
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
You should have a look at Uniform Proofs as a Foudation for Logic Programming 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.
-
1$\begingroup$ 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. $\endgroup$– MWBCommented Dec 6, 2020 at 22:50
-
1$\begingroup$ No, I don't think a type system is necessary -- just like for Horn Clauses. $\endgroup$– gascheCommented Dec 12, 2020 at 8:07
-
1$\begingroup$ I should have said "Higher-order Hereditary Harrop formulas" $\endgroup$– MWBCommented Dec 12, 2020 at 12:02
-
1$\begingroup$ 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. $\endgroup$– gascheCommented Dec 13, 2020 at 13:11