Otter is a powerful implementation of Predicate Calculus. It reasons using a number of different resolution methods. Proofs are done by contradiction. Otter implements unification to handle variables.
Otter supports two ways of representing predicate calculus statements. You can use the standard form, with ^, |, -, -->, and <-->. (AND, inclusive OR, NOT, IF, IF & ONLY IF (equivalence)) But you can also use clausal form which just uses | and -. All the clauses are implicitly ANDed.
Clausal form is easier to use but it does require some translation. All examples given here use clausal form. Most users of Otter prefer to use the clausal form because clausal form involves only two connectives. If you use the full FOL in Otter, the first thing Otter does is translate your code into clausal form. This is because the resolution-refutation proof method requires that all implications (-->) be removed.
This is the hard part! There are two categories of difficulty.
In English, knowledge if often expressed in the form of if-then rules which translate easily into FOL's -->.
Some examples.
Now, if you assume that these statements are universal (= "all") as opposed to existential (= "some") the translation to FOL is easy. You might have,
where the English words are predicate (= verbs, usually), hence the name predicate calculus. x is a universally quantified variable ("for all").
These statements are not in clausal form. So for Otter you would translate it from if-then to not-or, the latter being the clausal form. In propositional calculus, the translation formula is easy to remember.
p -> q is equivalent to -p | q.
Applying this formal to the predicate calculus statements above we get,
These clauses are correct Otter statements.
Of course, sometimes, it is more natural to translate directly form English to the OR form.
"Roberta is either a nurse or a teacher", naturally becomes in Otter,
(Note: This is inclusive OR. This statement leaves open the possibility that Roberta holds both jobs. Note also that all Otter clauses are terminated with a period.)
English can hide the IF-THEN (not to mention NOT-OR). Consider,
How would you translate this into FOL in normal form or clausal form? None of the words, IF, THEN, OR, or NOT appear in the sentence.
For me it sounds unnatural to translate the sentence as
If you did state it this way you could get an Otter clause directly,
-is_mammal(x) | is_mortal(x).
More natural is the two step approach. First change the English to,
Then use the equivalence of p --> q and -p | q to get the same result,
-is_mammal(x) | is_mortal(x).
Note that you have a lot of freedom (too much?) in English.
You could rephrase "All mammals are mortal." into "If
x is a mammal then x will die sometime." and get an Otter
clause like,
-mammal(x) | must_die_sometime(x).
Usually you translating a collection of English statements, so
the watchword is consistency in
your translation.
Note that two nots cancel in Otter, as in English. (When you hear someone say "I don't know nothing about it." , you usually interpret it as " I know nothing about it.", but the sentence actually says "I know everything about it." because the two negatives cancel out. The computer would have difficulty doing this -- it likely does not have the contextual knowledge humans have. We humans automatically assume we are talking to an uneducated person when we hear double negatives like this.)
Consider,
Translating form IF-THEN to NOT-OR we get
- -nurse(Roberta) | teacher(Roberta)
which becomes,
nurse(Roberta) | teacher(Roberta).
Note that the translation of n English sentence with a negative in the condition part results in a OR clause with no negatives whereas, an English sentence with no negative in the condition part results in an OR clause with a negation in it. This is a bit confusing and can easily lead to Otter bugs. In short,
Many English sentences have a form like the FOL statement,
p^ q ^ r --> s.
This translates into clausal form as,
-p | -q | -r | s.
For example,
This can be translated as,
-do_assignments(x) | -study_notes(x) | get_cps721_A(x).
English sentences can also have a form like,
p --> q ^ r ^ s.
This is equivalent two three separated clauses (which are implicitly ANDed by Otter).
For example,
This might be translated as,
p <--> q.
This can be put in clausal form as two clauses,
For example,
(You could rephrase this as "x wins if and only if x scores more goals.")
There are actually two, but this one is most useful here.
-(p ^ q) is equivalent to -p | -q.
This can usually be represented as,
-p ^ -q
In clausal form represent this a two separate statements:
Which are implicitly ANDed by Otter.
He is neither tall nor handsome.
- -tall(x).
- -handsome(x).
You may have felt a bit uneasy with some of the above translations from English into clausal FOL. The problems of translation lies in the facts that English is often ambiguous and contextual knowledge is needed to resolve the ambiguity (which is sometimes impossible to do). FOL on the other hand is precise and context free. We have a mismatch.
There are some cases which are fairly easily solved. Two examples are,
The OR in logic is inclusive. p | q is true not only if one of p or q is true, but also if both are true. In everyday English we tend to use OR exclusively. We mean one or the other of p and q, but not both.
You can put this in propositional calculus terms thus:
The second statement eliminates the case where both p and q are true. The second statement is not clausal form but with deMorgan's law we can change it to -p | -q. So for Otter we can translate XOR as
When you are translating English for Otter, you have to decide from the context, whether the English "or" is to be translated by OR or XOR. If you choose to interpret the English "or" as XOR, don't forget you need BOTH the above clauses in Otter.
Above we have discussed a famous example of ambiguity in English, the meaning of the word "or". The other main problem in translating into a machine usable form sentences in a human language such as English is the amount of information not explicitly put in the text. Logic puzzles illustrate this problem nicely.
A certain logic puzzle has 5 pilots flying planes form 5 UK airports to airports in 5 other countries. Now humans know that a pilot only flies one plane at a time. We also know from the way the puzzle is written, although it is not necessarily true in general, that each flight goes to only one of the destination airports.
None of this knowledge is explicitly stated in the puzzle description. And Otter, the machine, knows nothing about these facts. You have to tell Otter. How? That's part of your assignment!
Here in propositional notation is the basis of the answer. Suppose you have 4 choices, p, ,q, r, or s. And these choices are exclusive. Only one can be true. You can write,
p | q | r | s.
Alone that is not enough because | means inclusive OR and you want to express the fact that exactly one of the 4 can be true. You can do the following to exclude the unwanted alternatives. Add,
This is an extended version of XOR. Note that, for example, -r | -s means "If r is true, then s is not true".
Variables in Otter are universally quantified. You can represent existentially quantified variable as functions in Otter, but you will not need to do this in cps721.
All variables in Otter must begin with the lowercase letters u, v, w, x, y, z. or _. Any other beginning letter creates a constant symbol. Beware!