Propositional Theorem Proving

a different approach to using logic to solve problems is to use logical rules of inference to generate logical implications

in some cases, this can be less work than model-checking (i.e. generating a truth table) or even SAT solving

plus, logical rules of inference are at the level of logical reasoning that humans consciously strive to do

theorem-proving is interested in entailment, e.g. given a logical sentence A and a logical sentence B, we can ask if A entails B

the general idea is that sentence A is what the agent knows, and sentence B is something that the agent can infer from what it knows

sentence A might be very big, i.e. the entire “brain” of an agent encoded in logic

an important basic result in logic is the deduction theorem, which says:

A entails B if, and only if, A => B (A implies B) is a tautology (i.e. valid for all assignments of values to its variables)

so we can answer the question “Does A entail B?” by showing that the sentence A => B is a tautology

recall that a sentence is unsatisfiable if no assignment of values to its variables makes it true

so A => B is a tautology, then !(A=>B) is unsatisfiable, and !(A=>B) == !(!(A & !B)) == A & !B

so we can re-write the deduction theorem like this:

A entails B if, and only if, A & !B is unsatisfiable

this means you can use a SAT solver to figure out entailment!

Rules of Inference

recall that there are various rules of inference that can be used to create proofs, i.e. chains of correct inferences

e.g. modus ponens is this rule of inference:

A, A => B
---------   modus ponens
    B

this rule says that if you are given a sentence A, and a sentence A => B, you may infer B

e.g. and-elimination is this pair of rules:

A & B
-----       and-elimination
  A

A & B
-----
  B

these two rules encode the (obvious!) fact that if the sentence A & B is true, then A is true, and also B is true

logical equivalences can also be stated as inference rules, e.g.:

A <==> B
---------------
(A=>B) & (B=>A)

there are many inference rules, and choosing a reasonable set of rules for a theorem-prover turns out to be important

  • we can think of the application of one rule of inference as an action performed to the state of the world, i.e. the rule of inference adds more facts to the knowledge base
  • if there are multiple inference rules to choose from, then we need knowledge (i.e. heuristics) to help decide which rule to use
    • or we could rely on backtracking, i.e. just pick a rule at random, apply it, and keep going until it “seems” like a proof is not being reached
  • plus, how do we know that the rules of inference we are using are complete, i.e. if a proof exists, how do we know our set of inference rules will find it?
    • e.g. suppose the two and-elimination rules were our only rules of inference; is this enough to prove any entailment in propositional logic?
      • no!
      • for example, (P | P) -> P is clearly true, but and-elimination doesn’t apply to this sentence

Proof by Resolution

it turns out that only one particular inference rule is needed to prove any logical entailment (that can be proved): the resolution rule

in a 2-variable form, the resolution inference rule is this (| here means “or”):

A | B,  !B
----------
    A
              resolution

A | !B,  B
----------
    A

in English, the first rules says that if A or B is true, and B is not true, then A must be true; the second rule says the same thing, but B and !B are swapped

note that A | !B is logically equivalent to B -> A, and so the resolution rules can be translated to this:

!B -> A, !B
-----------   variation of modus ponens
   A


B -> A, B
---------    modus ponens
   A

in other words, resolution inference could be viewed as a variation of inference with modus ponens

we can generalize resolution as follows:

A_1 | A_2 | ... | A_i | ... | A_n    !A_i
-----------------------------------------     resolution generalized
A_1 | A_2 | ... | A_i-1 | A_i+1... | A_n

we’ve written A_i and !A_i, but those could be swapped: the key is that they are complementary literals

notice that both sentence above and below the inference line are CNF clauses

  • recall that a CNF clause consists of literals (a variable, or the negation of a variable), or-ed together

so resolution can be stated conveniently in terms of clauses, e.g.:

Clause_1   L_i     opposite of literal L_i is in Clause_1
--------------
Clause_2           Clause_2 is Clause_1 with opposite of literal L_i removed

here, L_i is a literal that has the opposite sign of a literal in Clause_1

  • i.e. L_i is the complement of a literal in Clause_1

Clause_2 is the same as Clause_1, but with the literal that is the opposite of L_i removed

e.g.:

(A | !B | !C)  !A     A and !A are complementary literals
-----------------
    !B | !C

(A | !B | !C)  C      C and !C are complementary literals
-----------------
    A | !B

full resolution generalizes this even further to two clauses:

Clause_1  Clause_2
------------------   full resolution
     Clause_3

here, we assume that some literal L appears in Clause_1, and the complement of L appears in Clause_2

Clause_3 contains all the literals (or-ed together) from both Clause_1 and Clause_2, except for L and its opposite — those are not in Clause_3

e.g.:

(A | !B | !C)  (!A | !C | D)    A and !A are complementary literals
----------------------------
        !B | !C | D

what is surprising is that full resolution is complete: it can be used to proved any entailment (assuming the entailment can be proven)

to do this, resolution requires that all sentences be converted to CNF

  • this can always be done … see the textbook for a sketch of the basic idea
  • the same requirement for most SAT solvers!

next, recall from above that if A entails B, then A & !B is unsatisfiable

  • this is a consequence of the deduction theorem

resolution theorem proving proves that A entails B by proving that A & !B is unsatisfiable

it follows these steps:

  • A & !B is converted to CNF
  • clauses with complementary literals are chosen and resolved (i.e. the resolution rule is applied to them to remove the literal and its complement) and added as a new clause in the knowledge base
  • this continues until one of two things happens:
    1. no new clause can be added, which means that A does not entail B
      • in other words, A & !B is satisfiable
    2. two clauses resolve to yield the empty clause, which means that A entails B
      • the empty clause means there is a contradiction, i.e. if P and !P are clauses then we can apply resolution to them to get the “empty clause”
      • clearly, if both P and !P are in the same knowledge base, then it is inconsistent since P & !P is false for all values of P

Example. KB = {P->Q, Q->R}

  • does KB entail P->R?

  • yes it does, and lets use resolution to prove this

  • to prove KB entails P->R, we will prove that KB & !(P->R) is unsatisfiable

  • first we convert KB & !(P->R) to CNF:

    !P | Q
!Q | R
P
!R

  • next we pick pairs of clauses and resolve them (i.e. apply the resolution inference rule) if we can; we add any clauses produced by this to the collection of clauses:

    !P | Q
!Q | R
P
!R

!P | R     // from resolving (!P | Q) with (!Q | R)
Q          // from resolving (!P | Q) with (P)
!Q         // from resolving (!Q | R) with (!R)

  • we have Q and !Q, meaning we’ve reach a contradiction

  • this means KB & !(P->R) is unsatisfiable

  • which means KB entails P->R

this is a proof of entailment, and the various resolutions are the steps of the proof

the exact order in which clauses are resolved could result in shorter or longer proofs, and in practice you usually want short proofs, and so heuristic would be needed to help make decisions

Horn Clauses and Definite Clauses

a fundamental difficulty with SAT solvers and algorithms like resolution is that, for propositional logic, they have exponential running time

  • SAT solvers are fast, but in the worst case they can still take an exponential amount of time to finish
  • plus, many problems require thousands or more variables when encoded in propositional logic, and that alone makes some problems simply too big to be handled by SAT solvers

so, some AI researchers have explored the possibility of using a logic that is less expressive than propositional logic, but for which entilaments can be computed more efficiently

for example, a definite clause is a clause in which exactly 1 literal is positive, e.g.:

A | !B | !C        definite clause

!A | !W | E | !S   definite clause

P                  definite clause


A | B | !C         not a definite clause

!T                 not a definite clause

a horn clause is a clause with 0 or 1 positive literals (i.e. at most one positive literal), e.g.:

A | !B | !C        horn clause

!A | !B | !C       horn clause (but not a definite clause)

!A                 horn clause (but not a definite clause)

A                  horn clause

note that every definite clause is a horn clause, but some horn clauses are not definite clauses

these restricted forms of clauses are interesting for a few reasons:

  • entailment of horn clauses can be decided in time linear with respect to the size of the knowledge base – much more efficient than full resolution

  • reasoning with horn clauses can be done in a straightforward way that humans find easier to follow than resolution

  • definite clauses can be written in an appealing form using implication, i.e. the definite clause A | !B | !C can be written (B & C) -> A

    • more generally, the definite clause A | !B1 | !B2 | … | !Bn can be written as (B1 & B2 & … & Bn) -> A

      • the implication is sometimes written in reverse:

        A <- B1 & B2 & ... & Bn

    • for some real-world problems, this is can be a natural way to encode knowledge, i.e. A is true if B1, B2, …, and Bn are all true

    • horn clauses are used extensively in the logic programming language Prolog

however, the problem with Horn clauses is that not all problems can be represented with them: they’re less expressive than propositional logic

this seems to be a fundamental trade-off: the more expressive the logic, the less efficient entailment algorithms are

  • but research continues!