Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Logic Programming Basics – Horn Logic

  • Syntactically a LP rule is a First Order Logic Horn Clause
  • The semantics of LP are different form the standard Tarski style FOL semantics (details later)
    • Herbrand semantics differ from FOL smeantics in the structures it considers to be models (details later)
      → Minimal model semantics
  • A FOL Horn clause is a disjunction of literals with one positive literal, with all variables universally quantified:
    • (∀) ¬C1 ∨ … ∨ ¬Cn ∨ H
  • This can be rewritten to closer correspond to a rule-like form:
    • (∀) C1 ∧ … ∧ Cn → H
  • In LP systems usually the following (non First Order Logic) syntax is used:
    • H :- C1,...,Cn
  • Such rules can be evaluated very efficiently , since the resolution of two Horn clauses is a again a Horn clause

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.