To be useful, the representation language must support methods of reasoning. (You also use inference or interpretation here.)
This works in predicate calculus as well, using the additional operation of unification.
Unify: x <- Socrates. (This is called 'instantiation'.)
Therefore,
Note that predicate calculus has more power that propositional calculus. In predicate calculus, one statement represents all men (still < 1/2 population :-)). In the proposition calculus one would have to write a statement for every man, about 3 billion of them. The propositional calculus had no universally qualified variables such as x above.
NOTE: The use of 'man' above follows the original use by Aristotle. H took 'man' to mean 'human', a practice continued up until the 1970s. Nowadays, the meaning of the word 'man' has been narrowed. Apart from issues of sexism, the changing use of 'man' is an example of the enormous problems in making intelligent machines which pass the Turing test. How much knowledge does a machine need? Is it possible for a machine to ever acquire sufficient human knowledge if it does not live humanly in the world?
You can get around the language problem by using just symbols. Modus ponens becomes,
Note the implicit AND here. The above says "If p --> q is true AND p is true THEN q is true">
This is also valid.
Similar sequences hold for predicate calculus.
There is a 'hole' in such arguments. However, nonetheless, we use abduction all the time. If you sit on a jury, you use abduction when you weigh the prosecution's evidence, and decide whether the defendant is guilty "beyond reasonable doubt". With abduction you can never be 100% sure. What we can say is that, q provides evidence of the existence of p. For example, you might have the premise, p = "If you commit a crime, you must be there." And, q = "A witness saw you in the vicinity of the crime.". This makes you a suspect but does not prove you guilty.
Abduction is very important in AI in spite of being fallacious. Many "Expert" Systems employ abduction, often with statistical methods to evaluate the probability of correct conclusions.
Systems such as Otter and Prolog follow correct logic but this limits their applicablility to the real world.
You can connect complex sentences out of simple ones in FOL. There are 5 connectives to do this for you: and ^, or |, not -, if --> and if and only if (equivalence) <-->
Predicate calculus variables come in two flavours.
Life is easier in situations with only universally quantified variables. In most analyses, existential variables are replaced by functions.
Truth tables can be handy for proving propositions in FOL You can combine the 5 basic ones to deal with more complex statements. ( You may also find this table useful when working with Otter.
| p | q | -p | p^q | p|q | p->q | p<->q |
| T | T | F | T | T | T | T |
| T | F | F | F | T | F | F |
| F | T | T | F | T | T | F |
| F | F | T | F | F | T | T |
With the rise of the computer it seemed natural to employ them to do logic. A difficulty was that while modus ponens and modus tolens were useful for humans they were not so good for machines. In the 1960s Robinson developed an new proof method which machines found more congenial.
This is shown most easily in the propositional calculus.
It looks like a kind of cancellation. q and -q cancel each other out. You can show this deduction is correct with a truth table.
| p | q | r | p|q | -q|r | p|q^-q|r | p|r | p|q^-q|r=>p|r |
|---|---|---|---|---|---|---|---|
| T | T | T | T | T | T | T | T |
| T | T | F | T | F | F | T | T |
| T | F | T | T | T | T | T | T |
| T | F | F | T | T | T | T | T |
| F | T | T | T | T | T | T | T |
| F | T | F | T | F | F | F | T |
| F | F | T | F | T | F | T | T |
| F | F | F | F | T | F | F | T |
So p | r is implied by p | q AND -q | r.
To do resolution with the predicate calculus, you must first unify the variables. See the section on Otter for an example.
On a computer, resolution must be combined with a contradiction of some sort to enable the machine to realize when it has succeeded. This proof by contradiction is also quite common in human generated proofs. Logic languages such as Prolog or Otter either require the user to create a potential contradiction or do so automatically in some circumstances. The role of contradiction is shown in the discussion of Otter.