Tuesday, August 12, 2008

Automatic Theorem Proving



The system consists of 10 rules, an axiom schema, and rules of well formed sequents and formulas.

1. Variables :

The capital letters A, B, C, …, P, Q, R, … are used as statement variables. They are also used as statement formulas.

2. Connectives:

The connectives ù , Ù , Ú , ® , and appear in the formulas with the order of precedence as given; ù has the highest precedence, followed by Ù , and so on.

3. String of Formulas :
A string of formulas is defined as follows:

    1. Any formula is a string of formulas.

    2. If a and b are strings of formulas, then a , b and b , a are strings of formulas.

    3. Only those strings which are obtained by steps (a) and (b) are strings of formulas, with the exceptions of the empty string which is also a string of formulas.


Example, the strings A, B, C; B,C,A; A,C,B, etc are the same.

4. Sequents :

If a and b are string of formulas, then is called a sequent in which a is denoted the antecedent and b the consequent of the sequent.

Sequent is true iff either atleast one of the formulas of the antecedent is false or atleast one of the formulas of the consequent is true. Thus

A, B, C,, E, F is true iff AÙ BÙ C® DÚ EÚ F is true.

The symbol is a generalization of the connective ® to strings of formulas.

AÞ B means "A implies B" or "A® B is a tautology" while a b means that a b is true.

For example P, Q, RP, N.

The empty antecedent is interpreted as the logical constant "true" or T, and empty consequent is interpreted as the logical constant "false" or F.

5. Axiom Schema :
If a and b are strings of formulas such that every formula in both a and b is a variable only, then the sequent is an axiom iff a and b have atleast one variable in common. As an example, A,B,CP,B, R, where A, B, C, P and R are variables, is an axiom

If a b is an axiom, then a b .

6. Theorem :

    1. Every axiom is a theorem.

    2. If a sequent a is a theorem and a sequent b results from a through the use of one of the 10 rules of the system, which are given below, then b is a theorem.

    3. Sequents obtained by (a) and (b) are the only theorem.


7. Rules :

The following rules are used to combine formulas within strings by introducing connectives. Corresponding to each of the connectives there are two rules, one for the introduction of the connective in the antecedent and the other for its introduction in the consequent. In the description of these rules a,b,g,… are strings of formulas while X and Y are formulas to which the connectives are applied.



Antecedent Rules

Rule ù Þ : If a , b X, g , then a ,ù X, b g .
Rule Ù Þ : If X, Y, a , b g , then a , XÙ Y, b g .
Rule Ú Þ : If X, a , b g and Y, a , b g , then a , X Ú Y, b g .
Rule ® Þ : If Y, a , b g and a , b X, g then a , X® Y, b g .
Rule Þ : If X, Y, a , b g and a , b X, Y, g , then a , X Y, b g .

Consequent Rules

Rule Þ ù : If X, a b , g , then a b , ùX, g .
Rule Þ Ù : If a X, b , g and a Y, b , g , then a b , XÙ Y, g .
Rule Þ Ú : If a X, Y, b , g then a b , X Ú Y, g .
Rule Þ ® : If X, a Y, b , g then a b , X® Y, g .
Rule Þ : If X, a Y, b , g and Y, a X, b , g , then a b , X Y, g .

In order to show that C follows from H1,H2,…,Hm we establish that

H1® (H2® (H3.......(Hm® C)....)) ………… (1)

is a theorem we must show that

H1® (H2® (H3....(Hm® C).....)) ………… (2)

our procedure involves showing (1) to be a theorem.

We first assume (2) and then show that this assumption is or is not justified. This task is accomplished by working backward from (2), using the rules, and showing that (2) holds if some simpler sequent is a theorem. We continue working backward until we arrive at the simplest possible sequents i.e., those which do not have any connectives.

If these sequents are axioms, then we have justified our assumption of (2). If atleast one of the simplest sequent is not an axiom, then the assumption of (2) is not justified and C does not follows from H1,H2,…,Hm. In the case C follows from H1,H2,…,Hm the derivation of (2) is easily constructed by simply working through the same steps, starting from the axioms obtained.

Example 1:
Show that PÚQ follows from P.

Solution:
We need to show that

(1) P® (PÚ Q)
(1) if (2) PPÚ Q (Þ ® )
(2) if (3) PP, Q (Þ Ú )

We first eliminate the connective ® in (1). Using the rule Þ ® we have "if PPÚ Q then P® (PÚ Q)". Here we have named PPÚ Q by (2). Each line of derivation thus introduces the name as well as gives a rule "(1) if (2)" means "if (2) then (1)". The chain of arguments is then given by (1) holds if (2), and (2) holds if (3). Finally (3) is a theorem, because it is an axiom. (3) is an axiom that leads to P® (PÚ Q) as shown.

(a) PP, Q Axiom
(b) PPÚ Q Rule (Þ Ú ), (a)
(c) P® (PÚ Q) Rule (Þ ® ), (b).


Example 2:
Show that (ùQÙ (P® Q)) ® ùP.

Solution:

 (1) (ùQÙ (P® Q))® ùP
(1) if (2) ùQÙ (P® Q) ù P (Þ ® )
(2) if (3) ùQ, P® QùP (Ù Þ )
(3) if (4) P® QùP, Q (ù Þ )
(4) if (5) QùP, Q and (6) P, ùP, Q (® Þ )
(5) if (7) P, Q Q (Þ ù )
(6) if (8) PP, Q (Þ ù )

Now (7) and (8) are axioms, hence the theorem (1) follows.


Example 3:
Does P follows from P Ú Q?

Solution:
We investigate whether (PÚ Q) ® P is a theorem.
Assume (1) (PÚ Q)® P
(1) if (2) (P Ú Q) P (Þ ® )
(2) if (3) PP and (4) Q P (Ú Þ )
Here (3) is an axiom, but (4) is not. Hence P does not follow from P Ú Q.

Example 4:
Show that SÚ R is tautologically implied by (PÚ Q) Ù (P® R)Ù (Q® S).

Solution:
To show (1) ((PÚ Q)Ù (P® R)) Ù (Q® S))® (SÚ R).
(1) if (2) (PÚ Q)Ù (P® R)Ù (Q® S) (SÚ R) (Þ ® )
(2) if (3) (PÚ Q)Ù (P® R)Ù (Q® S) S, R (Þ Ú )
(3) if (4) (PÚ Q), (P® R), (Q® S) S, R (Ù Þ twice)
(4) if (5) P, P® R, Q® SS,R and (6) Q, P® R, Q® SS,R (Ú Þ )
(5) if (7) P, R, Q® SS,R and (8) P, Q® SP,S,R (® Þ )
(6) if (9) P, R, S, S, R and (10) P, R S,R,Q (® Þ )
(7) if (11) P, S P, S, R and (12) PP, S, R, Q (® Þ )
(8) if (13) Q, R, Q® SS, R and (14) Q, Q® SS, R, P (® Þ )
(9) if (15) Q, R, SS, R and (16) Q, R S, R, Q (® Þ )
(10) if (17) Q, S S, R, P and (18) Q S, R, P, Q (® Þ )

Now (9) to (12) and (15) to (18) are all axioms. Therefore, the result follows.

Back to top





Exercise:
1. Show the validity of the following arguments for which the premises are given on the left and the conclusion on the right.

  1. ù(PÙ ùQ), ùQÚ R, ùR ùP
  2. (A® B)Ù (A® C), ù(BÙ C), DÚ A D
  3. ùJ® (MÚ N), (HÚ G)® ùJ, HÚ G MÚ N
  4. P® Q, (ùQÚ R) Ù ùR, ù(ùPÙ S) ùS
  5. (PÙ Q)® R, ùRÚ S, ùS ùPÚ ùQ
  6. P® Q, Q® ùR, R, PÚ (JÙ S) JÙ S
  7. BÙ C, (B C)® (HÚ G) GÚ H
  8. (P® Q)® R, PÙ S, QÙ T R

2. Derive the following, using rule CP if necessary

    1. ùPÚ Q, ùQÚ R, R® S Þ P® S.

    2. P, P® (Q® (RÙ S)) Þ Q® S.

    3. P® Q Þ P® (PÙ Q).

    4. (PÚ Q)® R Þ (PÙ Q)® R.

    5. P® (Q® R), Q® (R® S) Þ P® (Q® S).


3. Show that the following sets of premises are inconsistent.

    1. P® Q, P® R, Q® ùR, P.

    2. A® (B® C), D® (BÙ ùC), AÙ D.


Hence show that P® Q, P® R, Q® ùR, PÞ M, and A® (B® C), D® (BÙ ùC), AÙ DÞ P.

4. Show the following (use indirect method if needed)
  1. (R® ùQ), RÚ S, S® ùQ, P® QÞ ùP.
  2. S® ùQ, SÚ R, ùR, ùR QÞ ùP.
  3. ù(P® Q)® ù(RÚ S), ((Q® P)Ú ùR), RÞ P Q.

5. Show the following
    1. PÞ (ùP® Q).
    2. PÙ ùPÙ QÞ R.
    3. RÞ (PÚ ùPÚ Q)
    4. ù (PÙ Q)Þ ùPÚ ùQ

Posted by at
Labels:

No comments:

Post a Comment

Subscribe to: Post Comments (Atom)