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_passTo remove the if-then and other English words, connectives are used. The commonly used connectives of propositional logic are:
Denoting arbitary propositional formulae by uppercase variable letters, e.g., P, propositional formulae are defined recursively by:
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 |
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_clever | i_will_pass | i_am_clever => i_will_pass | i_will_pass => i_am_clever | i_am_clever | i_will_pass | A | i_am_clever & i_will_pass |
T | T | T | T | T | T | T |
T | F | F | T | T | F | F |
F | T | T | F | T | F | F |
F | F | T | T | F | F | F |
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 2^{N}, 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 | ||||||
p | q | p => q | q => p | p | q | A | p & q |
T | T | T | T | T | T | T |
T | F | F | T | T | F | F |
F | T | T | F | T | F | F |
F | F | T | T | F | F | F |
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 | ||||||
p | q | p => q | q => p | p | q | A | p & q |
T | T | T | T | T | T | T |
T | F | F | F | |||
F | T | T | F | F | ||
F | F | T | T | F | F |
Another example to illustrate logical consequence in propositional logic, using meaningless propositions:
Example | |||||||
---|---|---|---|---|---|---|---|
A = { q | r, q => ~p, ~(r & p) } C = ~p | |||||||
p | q | r | q | r | q => ~p | ~(r & p) | A | ~p |
T | T | T | T | F | F | ||
T | T | F | T | F | F | ||
T | F | T | T | T | F | F | |
T | F | F | F | F | |||
F | T | T | T | T | T | T | T |
F | T | F | T | T | T | T | T |
F | F | T | T | T | T | T | T |
F | F | F | F | 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 | |||||
p | q | p => q | p | q | A | p & q |
T | T | T | T | T | T |
T | F | F | F | ||
F | T | T | T | T | F |
F | F | T | F | F |
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 | ||||||||
p | q | r | p => q | q => p | p | q | p => ~q | A | ~r |
T | T | T | T | T | T | F | F | |
T | T | F | T | T | T | F | F | |
T | F | T | F | F | ||||
T | F | F | F | F | ||||
F | T | T | T | F | F | |||
F | T | F | T | F | F | |||
F | F | T | T | T | F | F | ||
F | F | F | T | T | F | 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 | |||||||
p | q | r | q | r | q => ~p | ~(r & p) | {~C} = p | A ∪ {~C} |
T | T | T | T | F | F | ||
T | T | F | T | F | F | ||
T | F | T | T | T | F | F | |
T | F | F | F | F | |||
F | T | T | T | T | T | F | F |
F | T | F | T | T | T | F | F |
F | F | T | T | T | T | F | F |
F | F | F | F | 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 2^{N} 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].
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 |