# 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:
• ~ for negation. This is "not" in English. Negation takes a single formula as its argument, e.g., ~i_am_clever, and is thus a unary connective.
• or & for conjunction This is "and" in English. Conjunction is an infix binary connective, taking two formulae as arguments, e.g., i_am_clever & i_will_pass.
• or | for disjunction This is also known as "inclusive or", and corresponds to some uses of "or" in English. Disjunction is also infix binary, e.g., i_am_clever | i_will_pass.
• => for implication. This corresponds to the English if-then construction. Implication is binary infix. The left hand operand is called the antecedent, and the right hand operand is called the consequent. E.g., i_am_clever => i_will_pass.
• <=> for equivalence. This is also known as double implication, and has the meaning of "if and only if" in English. Equivalence is binary infix, e.g., i_am_clever <=> i_will_pass.
• <~> for exclusive or. It has the meaning of "one or the other, but not both" in English. Exclusive or is binary infix, e.g., democrat <~> republican.
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:

• Propositions are formulae.
• If P and Q are formulae then ~P, P & Q, P | Q, P => Q, P <=> Q, and (P) are formulae.
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.
• Axioms: If you work hard then you get lucky. Either you get lucky or you work hard, or both. If you get lucky then, either you are not a rogue or you work hard (but not both). You are a rogue. Conjecture: You work hard.
• Axioms: If Mary loves Pat then Mary loves Quincy. If it is Monday then Mary loves Pat or Quincy (or both). Mary does not love both Pat and Quincy. Conjecture 1: If it is Monday then Mary loves Pat. Conjecture 2: If it is Monday then Mary loves Quincy.
• Axioms: If the car has no fuel or it has no spark, then it will not start. The car has a spark. The car will not start. Conjecture: The car has no fuel.

## 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