Hints for Solving Logic Problems
These guidelines will help in the translation of
``story problems'' into predicate calculus and solution of the problems
by resolution. Following these will help to avoid common errors.

Terms (constants, variables, and functions) are always
objects in the domain about which the formulas are written. Predicates
are true/false properties or relations of these objects.

It is a good idea to write down, at the side, type descriptions of
predicates, e.g.,
DRIVES(x,y) where x
is a person and y is a car.
A use of the predicate that involves objects of the wrong types is
likely either to be wrong or not part of a solution.

A statement ``for all'' or ``every'' in English usually translates to
a ∀ quantifier and uses a → connective.
``There exists'' or ``some'' usually translates to ∃
and uses a ∧ connective.

Use your knowledge of the realworld meaning of a statement to guide
the translation into predicate calculus. There may be multiple correct
ways of translating a statement, but they all result in the same clause
form. For example, the statement ``No cat likes any dog'' could be
written:
 ∀ x (CAT(x) →
∀ y (DOG(y) → ¬ LIKES(x,y)))
 ∀ x (CAT(x) →
¬ ∃ y (DOG(y) ∧ LIKES(x,y)))
 ¬ ∃ x (CAT(x) ∧ ∃ y (DOG(y) ∧ LIKES(x,y)))
 ¬ ∃ x ∃ y (CAT(x) ∧ DOG(y) ∧ LIKES(x,y))
All of these produce the clause form:
¬ CAT(x) ∨ ¬ DOG(y) ∨ ¬ LIKES(x,y)

After translating a sentence into clause form, read it back into English
and see whether it has the same meaning: ``Either x is not a cat or
y is not a dog or x does not like y .''

Any form P(x) or ¬ P(x) that appears as a clause by itself
is wrong, whether it appears as a clause resulting from translation of
an English statement, or as the result of a resolution step. (Note that
x is a universally quantified variable; P(a) , where a is
a constant, is okay.) The rationale for this rule is that if P(x)
is true, then P is true of everything and therefore cannot be useful
for reasoning.

More generally, the literals of a clause should be connected by the
variables they contain. Imagine that lines are drawn between occurrences
of each variable, i.e., all the occurrences of x are connected, etc.
The clause should be completely connected; if any literal is disconnected
from the rest of the clause, it probably indicates an error. Moreover,
each variable should appear at least twice.

Constants other than Skolem constants are generally numbers or things
that would be written as proper names in English: 3 John Austin .
A common noun written as a constant is probably incorrect. For example,
``Every boy loves some dog'' can be written:
∀ x (BOY(x) → ∃ y (DOG(y) ∧ LOVES(x,y)))
but not:
∀ x (BOY(x) → LOVES(x,dog)) . Note that in the latter
form there is nothing to say that the constant dog is a dog.

Every time a Skolem constant or Skolem function is created, it must be
a new one. By convention, Skolem constants are represented by letters
a b c and Skolem functions by f() g() h() .

Different Skolem constants and functions cannot be unified.
If you find yourself wanting to unify two different Skolems, don't do it!
Instead, use this information to find your bug: one of the Skolems
should be a universally quantified variable.

Certain common forms can be translated to clause form by inspection.
``Every P is Q'' will translate to: ¬ P(x) ∨ Q(x) .
More generally, ``Every P that is R and S and ... is Q'' will translate to:
¬ P(x) ∨ ¬ R(x) ∨ ¬ S(x) ∨ ... ∨ Q(x) .

Statements with an ``and'' in the conclusion will result in multiple clauses.
For example, ``Every cat is soft and furry'' results in clauses:
 ¬ CAT(x) ∨ SOFT(x)
 ¬ CAT(x) ∨ FURRY(x)
 Use brackets liberally to avoid making mistakes in algebraic
manipulations. For example, in writing the negated conclusion,
 Write the conclusion in positive form.
 Put large brackets around it.
 Put a negation sign in front of the bracket.
 An ``If [...] then [...]'' should be translated as:
[ [...] → [...] ] . Use brackets to make sure your
manipulations are correct.

If the conclusion is of the form ``If condition then result ''
you can often simplify the algebra by:
 Writing the condition as additional positive axioms.
 Negating the result.
Justification: ``If C then R'' is written [ C → R] , which is
negated:
¬ [ C → R] = ¬ [ ¬ C ∨ R ]
= [ C ∧ ¬ R ] .
C and R must have no variables in common to be separated in
this manner.

Use your knowledge of the realworld situation to guide the resolution
steps you make, so that the resulting search will be short. Use the
strategies set of support (use the negated conclusion, which will
often involve constants) and unit preference (resolve with shorter
clauses).
Gordon S. Novak Jr.