FOPC - First Order Predicate Calculus

Propositional calculus: Fido_is_a_dog
Predicate calculus: Is_a_dog(Fido)

Definition of Propositional calculus sentences

Every propositional symbol and truth symbol is a sentence.
For example: true, P, Q and R are four sentences.
The negation of a sentence is a sentence.
For example not P and not false are sentences
The conjunction (and) of two sentences is a sentence.
For example: P and not P is a sentence.
The disjunction (or) of two sentences is a sentence.
For example: P or not P is a sentence.
The implication of one sentence for another is a sentence.
For example: P=>Q is a sentence.
The equivalence of two sentences is a sentence.
For example P or Q = R is a sentence.

Predicate Calculus Sentences

Every atomic sentence is a sentence.
If S is a sentence, then so is its negation, not S
If S1 and S2 are sentences, then so is their conjunction, S1 and S2.
If S1 and S2 are sentences, then so is their disjunction, S1 or S2.
If S1 and S2 are sentences, then so is their implication, S1 => S1.
If S1 and S2 are sentences, then so is their equivalence, S1 = S2.
If X is a variable and S is a sentence, then forall X S is a sentence.
If X is a variable and S a sentence, then thereexists X S is a sentence.

Some definitions: Logical inference: infer new correct expressions from a set of true assertions.

An interpretation that makes a sentence true is said to satisfy that sentence.

An expression X logically follows from a set of predicate calculus expressions S if every interpretation that satisfies S also satisfies X. (Normally the inference rules give us the logically follows.)

When every sentence X produced by an inference rule operating on a set S of logical expressions logically follows from S, the inference rule is said to be sound.

If the inference rule is able to produce every expression that logically follows from S, then it is said to be complete.

A proof procedure is a combination of an inference rule and an algorithm for applying it to a set of logical expression to generate new sentences.

A predicate calculus expression X logically follows from a set S of predicate calculus expressions if every interpretation and variable assignment that satisfies S also satisfies X.

An inference rule is sound if every predicate calculus expression produced by the rule from a set S of predicate calculus expressions also logically follows from S.

An inference rule is complete if, given a set S of predicate calculus expressions, it can infer every expression that logically follows form S.

Satisfy, Model, Valid, Inconsistent
If S has a value of T under I and a particular variable assignment, then S is assaid to be satisfied.

If I satisfies S for all variable assignments, then I is a model of S.

S is satisfiable if and only if there exist an interpretation and variable assignment that satisfy it; otherwise, it is unsatisfiable.

A set of expression is satisfiable if and only if there exist an interpretation and variable assignment that satisfy every element.

If a set of expression is not satisfiable, it is said to be inconsistent.

If S has a value T for all possible interpretations, is said to be valid.

Modus Ponens, Modus Tolens, and Elimination and Introduction, and Universal Instantiation

If the sentences P and P=>Q are known to be true then, modus ponens lets us infer Q.

Under the inference rule, modus tolens, if P=>Q is known to be true and Q is known to be false, we can infer not P.

And elimination allows us to infer the truth of either of the conjuncts from the truth of a conjunctive sentence. For example, P and Q lets us conclude both P and Q are true.

And introduction lets us infer the truth of a conjunction from the truth of its conjuncts. For example, if both P and Q are true, then P and Q are true.

Universal instantiation states that if any universally quantified variable in a true sentence is replace by any appropriate term from the domain, the result is a true sentence, Thus, if A is from the domain of X, then forall X P(x) lets us infer P(A).

A FOPC description of a world.

Could be described with FOPC notation as: on(c,a), on(b,d), ontable(a), ontable(d), clear(b), clear(c) hand_empty.

We could then try to describe a move by

  forall X forall Y (hand_empty and clear(X) and clear(Y)
                    and pick_up(X) and put_down(X,Y)
                    => stack(X,Y)

This is a reasonable description intuitively and we can write program using this. There is a serious problem with this, however. Everything is FOPC, if true is true for all time. There is NO way to change values within a definition of a world.

FOPC

FOPC includes Propositional calculus (things like john_loves_mary fido_is_a_dog)
FOPC also includes Predicates (things like love(john,mary) dog(fido)) the quantifiers there_exits and for_all and all WFF's based on Predicate Calculus the the additional rules for quantifiers and variables.

Unification

Unification allows us to build more complex (or simpler) formulas. The two rules are

            a           a             a is substitued for a
            a           X    {a/X}    a is substituted for X

So you might have a variable X in a WFF and substitute father(jack) or {father(jack)/X}