To prove things in predicate calculus we need two things. First we need to know what inference rules are valid - we can't keep going back to the formal semantics when trying to draw a simple inference! Second we need to know a good proof procedure that will allow us to prove things with the inference rules in an efficient manner.
When discussing propositional logic we noted that a much used inference rule was modus ponens:
A, A B
---
B
This rule is a sound rule of inference for predicate logic. Given the
semantics of the logic, if the premises are true then the
conclusions are guaranteed true. Other sound inference rules
include modus tollens (if A B is true and B is false then
conclude
A), and-elimination (if A
B is true then
conclude both A is true and B is true), and lots more.
In predicate logic we need to consider how to apply these
rules if the expressions involved have variables. For
example we would like to be able to use the facts X (man(X)
mortal(X)) and man(socrates) and conclude mortal(socrates). To do this
we can use modus ponens, but allow universally quantified sentences to
be matched with other sentences (like in Prolog). So, if we
have a sentence
X A
B and a sentence
C then if A and C can be matched or unified then we can apply modus
ponens.
The most well known general proof procedure for predicate
calculus is resolution. Resolution is a sound proof
procedure for proving things by refutation - if you can derive
a contradiction from P then P must be true. In
resolution theorem proving, all statements in the logic are transformed into
a normal form involving disjunctions of atomic expressions
or negated atomic expressions
(e.g.,
dog(X)
animal(X)). This allows new expressions
to be deduced using a single inference rule. Basically, if we
have an expression A1 v A2 ...v An v
C and an expression
B1 v B2 ...v Bm v C then we can deduce a new expression
A1 v A2 ...v An v B1 v B2 ...v Bm. This single inference rule
can be applied in a systematic proof procedure. This is all
described in tedious detail in [Rich &Knight, pgs 143-160].
Resolution is a sound proof procedure. If we prove something using it we can be sure it is a valid conclusion. However, there are many other things to worry about when looking at a proof procedure. It may not be complete (ie, we may not be able to always prove something is true even if it is true) or decidable (the procedure may never halt when trying to prove something that is false). Variants of resolution may be complete, but no proof procedure based on predicate logic is decidable. And of course, it may just not be computationally efficient. It may eventually prove something, but take such a long time that it is just not usable. The efficiency of a proof will often depend as much on how you formulate your problem as on the general proof procedure used, but it is still an important issue to bear in mind.