Logics

In ATP, problems are expressed in some formal language. Most commonly the problems are expressed in a logic, ranging from classical propositional logic to more exotic logics, such as modal and temporal logics. Current research in ATP is dominated by the use of classical logic, at the propositional and 1st order levels. These logics, and proof within these logics, are well understood and documented.

Propositional (0th order) Logic

Propositional logic is a simple and well known language for representing knowledge. It is very simple to test for logical consequence in propositional logic, as is shown below.

The Language of Propositional logic

The syntax of propositional logic is most easily introduced through an example.

Example 
A = { If I am clever then I will pass,
      If I will pass then I am clever,
      Either I am clever or I will pass }
C = I am clever and I will pass

The conclusion that I am clever and I will pass is a logical consequence of the axioms. The example is written in English, but it is easily translated into propositional logic. There are two propositions in the example: I am clever and I will pass. In propositional logic, these propositions can be represented by their text. Using the Prolog convention of starting propositions with lowercase alphabetic, the axiom set and conclusion become : 

A = { If i_am_clever then i_will_pass,
      If i_will_pass then i_am_clever,
      Either i_am_clever or i_will_pass }
C = i_am_clever and i_will_pass
To remove the if-then and other English words, connectives are used. The commonly used connectives of propositional logic are: There are other less common connectives, giving a total of four unary connectives and 16 binary ones. Any good introductory text on logic, e.g., [Chu56] will provide details. For ATP, the above are adequate. The truth tables for the connectives provide their meaning.

Denoting arbitary propositional formulae by uppercase variable letters, e.g., P, propositional formulae are defined recursively by:

The precedence order of the above operators is ~ & | => <=>, i.e., ~ binds most tightly, down to <=>. This precedence ordering allows some brackets to be omitted, e.g., ~a | b => c means (((~a) | b) => c).

Now the above example can be written in propositional logic as follows:

Example 
A = { i_am_clever => i_will_pass,
      i_will_pass => i_am_clever,
      i_am_clever | i_will_pass }
C = i_am_clever & i_will_pass

Logical Consequence in Propositional Logic

Logical consequence in propositional logic can be established using truth tables to check that "every model of the axiom set is a model of the formula".

Example 
A = { i_am_clever => i_will_pass,
      i_will_pass => i_am_clever,
      i_am_clever | i_will_pass }
C = i_am_clever & i_will_pass
i_am_cleveri_will_passi_am_clever => i_will_passi_will_pass => i_am_cleveri_am_clever | i_will_passAi_am_clever & i_will_pass
TTTTTTT
TFFTTFF
FTTFTFF
FFTTFFF

It is simply necessary to check that each row that is a model of the axiom set, i.e., in those rows where A is TRUE the conclusion is also TRUE. In this example only the first row needs to be checked. In general, the maximal number of rows to be checked is 2N, where N is the number of propositions in the language. Thus this constitutes a simple decision procedure for logical consequence in propositional logic.

To avoid accidental use of the intended meaning of the propositions, the propositions can be reduced to meaningless symbols. This indicates that the conclusion follows from the axioms, regardless of the meaning of the symbols, i.e., it is a logical consequence. The truth table is the same as before:

Example 
A = { p => q,
      q => p,
      p | q }
C = p & q
pqp => qq => pp | qAp & q
TTTTTTT
TFFTTFF
FTTFTFF
FFTTFFF

When building these truth tables, as soon as an axiom is found to be FALSE in a given interpretation, that interpretation can be ignored for the remaining axioms, because the check is only for interpretations that are models of all the axioms. (This is AI - solving an O(E) problem in O(P) time!) To make this observation most effective, the axioms that are most easily shown to be FALSE in many interpretations should be considered first.

Example 
A = { p => q,
      q => p,
      p | q }
C = p & q
pqp => qq => pp | qAp & q
TTTTTTT
TFF F
FTTF F
FFTTFF

Another example to illustrate logical consequence in propositional logic, using meaningless propositions:

Example 
A = { q | r,
      q => ~p,
      ~(r & p) }
C = ~p
pqrq | rq => ~p~(r & p)A~p
TTTTF F
TTFTF F
TFTTTFF
TFFF F
FTTTTTTT
FTFTTTTT
FFTTTTTT
FFFF F

Each of the three models of the axiom set is also a model of the conclusion, i.e., the conclusion is a logical consequence of the axiom set.

Here's an example where the formula is not a logical consequence of the axiom set:

Example (of non-logical consequence) 
A = { p => q,
      p | q }
C = p & q
pqp => qp | qAp & q
TTTTTT
TFF F
FTTTTF
FFTFF

The third interpretation is a model of the axiom set, but is not a model of the conclusion. The conclusion is thus not a logical consequence of the axiom set.

Here is an example to illustrate logical consequence by an unsatisfiable axiom set:

Example 
A = { p => q,
      q => p,
      p | q,
      p => ~q }
C = ~r
pqrp => qq => pp | qp => ~qA~r
TTTTTTFF
TTFTTTFF
TFTF F
TFFF F
FTTTF F
FTFTF F
FFTTTF F
FFFTTF F

There are no models of the axiom set, so every model of the axiom set is a model of the conclusion, i.e., the conclusion is a logical consequence of the axiom set. Intuitively, it seems unreasonable to conclude ~r from the axiom set, as r is not even mentioned in the axioms. Thus it is sensible to first check that the axioms are satisfiable, by ensuring that at least one row of the truth tables has all the axioms true.

Here is an example illustrating logical consequence in propositional logic by unsatisfiability:

Example 
A = { q | r,
      q => ~p,
      ~(r & p) }
C = ~p
pqrq | rq => ~p~(r & p){~C} = pA ∪ {~C}
TTTTF F
TTFTF F
TFTTTF F
TFFF F
FTTTTTFF
FTFTTTFF
FFTTTTFF
FFFF F

None of the interpretations are models of A ∪ {~C}, i.e. A ∪ {~C} is unsatisfiable and the conclusion is a logical consequence of the axiom set.

From the observation that the truth table for any propositional logic contains 2N rows for N propositions, it is clear that the complexity of determining whether or not a conclusion is a logical consequence of an axiom set is O(E). Note that it is always possible to decide whether or not a conclusion is a logical consequence of a set of axioms, i.e., the problem is decidable. In fact the problem can be shown to be NP-complete [REF].

Exercises

  1. Determine if each Conjecture is a logical consequence of the Axioms. Do some directly and some using unsatisfiability.

    Axioms Conjecture
    a
    a => b     		b
    p => q
    ~q | p
    p | q
    		p & q
    p => q
    p | q
    		p & q
    p | q | r
    r => (p | q)
    (q & r) => p
    ~p | q | r
    		q | r
    p | q | r
    r => (p | q)
    (q & r) => p
    ~p | q | r
    		q & (r => p)
    p => q
    ~q | p
    p | q
    ~(p & q)
    		(~q => p) => (q | ~p)
    q | p
    q => r
    (s & r) => t
    t => p
    		p
    q | p
    p => q
    q => (~r | p)
    r
    		p
    ~n | ~t
    m | q | n
    m => l
    q => l
    ~l | ~p
    r | p | n
    r => ~l
    		~t

  2. Convert the following to propositional logic, and use truth tables to determine whether or not the Conjecture is a logical consequence of the Axioms.

Exam Style Questions

  1. Use a truth table to show that (q => p) | ~(q => (p | r)) is a logical consequence of the set { p | q | r, r => (p | q), (q & r) => p, -p | q | r }
  2. Use a truth table to prove that ~p is a logical consequence of the set { q | r, q => ~p, ~(r & p) }.
  3. Use a truth table to show that p & q is not a logical consequence of the set { p => q, q }.
  4. Encode the following scenario in propositional logic, and prove the conclusion:
    If the races are fixed or the gambling houses are crooked, then the tourist trade will decline. If the tourist trade declines then the police force will be happy. The police force is never happy.
    Conclusion: The races are not fixed