Herbrand Universe: It is a good exercise to determine for given formulae if they are satisfied/valid on specific L-structures, and to determine, if they exist, models for them. A good starting point in this task, and useful for a number of other reasons, is the Herbrand Universe for this set of formulae. Say that {F01 .. F0n} are the individual constants in the formulae [if there are no such constants, then introduce one, say, F0]. Say that {F1 .. Fm} are all the non 0-ary function symbols occurring in the formulae. Then the set of (constant) terms obtained starting from the individual constants using the non 0-ary functions, is called the Herbrand Universe for these formulae.
For example, given the formula (P x A) OR (Q y), its Herbrand Universe is just {A}. Given the formulae (P x (F y)) OR (Q A), its Herbrand Universe is {A (F A) (F (F A)) (F (F (F A))) ...}.
Reduction to Clausal Form: In the following we give an algorithm for deriving from a formula an equivalent clausal form through a series of truth preserving transformations. We can state an (unproven by us) theorem:
Theorem: Every formula is equivalent to a clausal form
We can thus, when we want, restrict our attention only to such forms.
Deduction
An Inference Rule is a rule for obtaining a new formula [the consequence] from a set of given formulae [the premises]. A most famous inference rule is Modus Ponens:
When we introduce inference rules we want them to be Sound, that is, we want the consequence of the rule to be a logical consequence of the premises of the rule. Modus Ponens is sound. But the following rule, called Abduction , is not:
is not. For example:
gives us a conclusion that is usually, but not always true [John takes a shower even when it is not raining].
A Logic or Deductive System is a language, plus a set of inference rules, plus a set of logical axioms [formulae that are valid].
A Deduction or Proof or Derivation in a deductive system D, given a set of formulae GAMMA, is a a sequence of formulae B1 B2 .. Bn such that:
In this case we say that Bn is Derived from GAMMA in D, and in the case that GAMMA is empty, we say that Bn is a Theorem of D.