1
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
4
  • 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$
    – bobcat
    Dec 6 '20 at 22:50
  • 1
    $\begingroup$ No, I don't think a type system is necessary -- just like for Horn Clauses. $\endgroup$
    – gasche
    Dec 12 '20 at 8:07
  • 1
    $\begingroup$ I should have said "Higher-order Hereditary Harrop formulas" $\endgroup$
    – bobcat
    Dec 12 '20 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$
    – gasche
    Dec 13 '20 at 13:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.