# Clausal-Form Logic (1)

Clausal form is a subset of first order logic. It is a normal form in which a sentence is defined by an universal prefix (a string of universal quantifiers) and a matrix (a quantifier-free conjunction of a clause). Here are a couple of examples of clauses:

### a b c (U)( healthy(U) ¬eat(U, porridge) )

The basic evaluation step of Prolog replaces a query call by the body of a program clause whose head it can match. This is the same as the application of an inference rule in logic, called resolution. A resolution inference step chooses two clauses having the property that one contains a disjunct X (a positive literal) and the other contains a disjunct ¬X (a negative literal), these disjuncts are known as complementary. A new clause (the resolvent) is constructed from the two initial clauses, using all the literals except the complementary ones. Here are a couple of examples:

1. a ¬b c
2. d b
these "resolve" to produce
3. a c d
1. (U)(healthy(U) ¬eat(U, porridge))
2. ¬healthy(sim)
these "resolve" to produce
3. ¬eat(sim, porridge)

Clauses can be classified by the number of positive and negative literals they contain.

 Clause Classification Definition Example Definite Exactly one positive literal, any number of negative literals happy(sim) or ¬eating(sim, pie) Positive unit No negative literals happy(sim) Negative unit Exactly one negative literal ¬desirable(pop_music) Unit A positive or negative unit clause Negative No positive literals, and any number of negative literals ¬happy(sim) ¬eating(sim, snails) Empty No literals (denoted by ) Indefinite At least two positive literals happy(sim) unhappy(sim)