1st order logic overcomes these two weaknesses of propositional logic by providing a richer language. The cost of this increased expressivity is the loss of decidability for logical consequence. 1st order logic is semi-decidable, which means that if a formula is a logical consequence of a set of axioms, it is possible to show that it is. However, if a formula is not a logical consequence of a set of axioms, it may not be possible to show that it is not. In addition, 1st order logic requires more complex mechanisms for checking for logical consequence.
| Example |
|---|
V = { V : V starts with uppercase }
F = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }
|
From the components of the language, two types of expressions are built. This is in contrast to propositional logic where only propositions exist. The first type of expression is terms. Terms are used to denote (possibly arbitrary) objects in the domain of interest. Terms thus correspond roughly to data in conventional programming. Terms are defined recursively by:
| Example |
|---|
geoff Person brother_of(jim) brother_of(brother_of(X)) |
Note that if there is a functor of arity greater than 0, then there is an infinite number of terms. As might be expected, ATP for 1st order logic is much easier if the number of terms is finite (in fact it reduces to ATP for propositional logic). For this reason, it is desirable to formulate ATP problems without any functors of arity greater than 0.
The second type of expression is atoms, which correspond to the propositions of propositional logic. Atoms decribe relationships between terms (objects in the domain). Atoms are defined by:
| Example |
|---|
wise(geoff) taller(Person,brother_of(jim)) wise(brother_of(brother_of(X))) |
If the number of terms is infinite (which occurs if there is a functor of arity greater than 0), and there is a predicate symbol of arity greater than 0, then there is an infinite number of atoms.
Connectives are used to combine atoms into the formulae of 1st order logic. The connectives include all those used in propositional logic, and two new quantifiers:
The precedence order of the above operators is ∀ ∃ ~ | & => <=>, i.e., ∀ and ∃ bind most tightly, down to <=>. This precedence ordering allows some brackets to be omitted, e.g., ∀X (clever(X) => pass(X) | lazy(X)) means ∀X (clever(X) => (pass(X) | lazy(X))). Note that the ()s round the (clever(X) => pass(X) | lazy(X)) are necessary, for otherwise the quantification would apply to only the clever(X).
| Example |
|---|
wise(geoff) ~taller(Person,brother_of(jim)) wise(geoff) & wise(brother_of(brother_of(Person))) ~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person))) wise(brother_of(brother_of(Person)) => wise(geoff) wise(geoff) <=> ~taller(Person,brother_of(jim)) (wise(geoff) & wise(brother_of(brother_of(Person)))) | wise(geoff) ∀Person ~taller(Person,brother_of(jim)) ∃Person wise(brother_of(brother_of(Person)) => wise(geoff) |
Atoms and the negations of atoms are called literals.
| Example |
|---|
wise(brother_of(X)) ~taller(geoff,jim) |
The scope of a quantification is the formula which follows the
quantification, e.g., the scope of ∃Person in
∃Person wise(brother_of(brother_of(Person)) =>
wise(geoff)
is
wise(brother_of(brother_of(Person)).
A variable is bound if it occurs in a quantification or it is
within the scope of a quantification of that variable.
Otherwise a variable is free.
A formulae that has no free variables is a closed formula;
otherwise a formula is open.
| Example |
|---|
|
Person is bound in in the closed formula: ∀Person ~taller(Person,brother_of(jim))
Person is free in the open formula:
Person is bound and free in the open formula:
Person is bound in the closed formula:
|
For ATP open formulae are not useful, because it is not possible to interpret (in the sense of giving meaning) open formulae. In English universal quantification is usually meant if no explicit quantification is given, e.g., "Sheep are stupid" usually means "All sheep are stupid", not "There exists a sheep that is stupid".
| Example |
|---|
There is a barbers' club that obeys the following three conditions:
|
V = { V : V starts with uppercase }
F = { guido/0, lorenzo/0, petrucio/0, cesare/0 }
P = { member/1, shaved/2, all_shaved/1 }
|
|
Osama Bin Laden is a terrorist. If someone is a terrorist and is dangerous, then his leader is a terrorist and is dangerous. There are some terrorists who are their own leader. Dangerous people care about themselves, or about no-one (not even themselves!).
Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also there are some grains, and grains are plants. Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars but not snails. Caterpillars and snails like to eat some plants. Prove that there is an animal that likes to eat a grain eating animal.
The basic notion of set theory is membership of a set. Using a member/2 predicate, define set equality, intersection, union, power set, empty set, and diifference. For example, intersection is defined as:
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,A)
& member(X,B) ) )
Now write conjectures for transitivity of subset, associativity of set
intersection, and distribution of intersection over union.
If, by repetitive use, the application of SPTs produces a set that is obviously unsatisfiable (e.g., containing FALSE) from a set of formulae, then, iteratively, this means that the very original set is also unsatisfiable. If the original set is of the form Ax U {~C}, this establishes that C is a logical consequence of Ax. The process of producing a set that is obviously unsatisfiable is called finding a refutation.
An inference rule is sound if it infers only logical consequences of its parents.
The operation of applying a sound inference rule to parents from a set, and then adding the inferred formula back into the set, is a SPT (think why!). (There are other SPTs, but this is an important one.) Thus sound inference rules form the basis of a a simple algorithm for establishing logical consequence.
The basic saturation procedure is :
While a refutation has not been found
Copy formulae from the set
Generate logical consequences
Put logical consequences into the set
Note the "Copy", indicating that a formula may be used multiple
times with a new set of variables each time.
An inference system is complete if, by repetitive use, it can infer every logical consequence of its input.
An inference system is refutation complete if, by repetitive use, it can infer FALSE (a contradiction) from every unsatisfiable set.
Note: A complete inference system can infer all logical consequences, while a refutation complete inference system can only check (via the unsatisfiability idea) for logical consequence.
Suming, Yi, and Yury are students, and are the only three students. If a student works hard then they get a good grade. At least one of the students works hard. Therefore at least one student will get a good grade.
There are some students who fail. If a student fails, then either there is a lecturer who has taught the student badly, or the student is stupid. No lecturer teaches any student badly. Therefore there is some student who is stupid.