CIS 554 Clause Syntax
 Fall 2012, David Matuszek

Literals Predicate Calculus Clojure
Propositions

CaesarIsEmperor

CaesarIsEmperor
Predicates Emperor(Caesar), loves(John, Mary) (emperor caesar), (loves john mary)
Functions EmperorOf(Rome) (emperor-of rome)
Skolem constants x', NextPresident'
We don't know who the next president will be, but there will be one. 		(skolem x), (skolem next-president)
Skolem functions Every person p has a mother m, but who that mother is, is a function of p: m'(p) (skolem m p)

A clause is a disjunction (or) of literals, some of which may be negated.

  Predicate Calculus Clojure (the "or" is implied)
Clauses

¬Roman(x) ∨ knows(x, Caesar)

animal(x) ∨ vegetable(x) ∨ mineral(x)

eats(x, broccoli) ∨ ¬(healthy, x)

( (not (roman x)) (knows x caesar) )

((animal x) (vegetable x) (mineral x) )

( (eats x broccoli) (not (healthy x)) )

When a fact consists of a conjunction (and) of predicate calculus expressions, it can be broken down into separate facts.

  Predicate Calculus Clojure
Expression loves(john, mary) ∧
loves(mary, john) ∧
(hates(bill, john) ∨ (not (loves john mary)))		 (and (loves john mary)
     (loves mary john)
     (or (hates bill john) (not (loves john mary)))  )
Clause form
("and" and "or" are both implied)
  1. loves(john, mary)
  2. loves(mary, john)
  3. hates(bill, john) ∨ (not (loves john mary)
 (  (loves john mary)
   (loves mary john)
   ((hates bill john) (not (loves john mary)))  )