Logical Forms +

1)      Write a paragraph which says something significant about Jacques Herbrand and his contribution to symbolic logic.

R) Jacques Herbrand made contributions to mathematical logic creating the Herbrand`s theorem that stablishes a link between quantification theory and sentential logic which is important in that it gives a method to test a formula in quantification theory by successively testing formulas for sentential validity.

2)      Write a paragraph which says something significant about Alfred Horn and his contribution to symbolic logic.

R) Alfred Horn wrote the paper “On sentences which are true of direct unions of algebra”, and in this paper he describes Horn Clauses and Horn sentences. Later that clauses turned into the foundation of logic programming.

3)      Write a paragraph which says something significant about John Alan Robinson and his contribution to symbolic logic.

R) John Alan Robinson major contribution is to the foundation of automated theorem proving. Robinson also created the resolution principle. In 1996 he received the Herbrand Awards because of his research.

4)      Define disjunctive normal form.

R) A formula is said to be in disjunctive normal form if it has this form F1 \/ F2 \/ ….. Fn. Where each F is a conjunction of literals. Example: ( P /\ Q )\/( Q /\ P).

5)      Transform the following into disjunctive normal forms:

a)      (~P /\ Q) -> R

~(~P /\ Q ) \/ R    LQ2

 ( P \/ ~Q) \/ R      LQ5

b)      ~(P \/ ~Q)/\ (S ->T)

~(P \/ ~Q) /\ ( ~S \/ T) LQ2

 ( ~P /\ Q) /\ ( ~S \/ T)  LQ4

((~P /\ Q) /\ ~S) \/ (( ~P /\ Q) /\ T))   LQ7

c)       (P -> Q ) -> R

( ~P \/ Q) -> R LQ2

~( ~P \/ Q) \/ R   LQ2

( P/\ ~Q) \/ R    LQ4

6)      Define conjunctive normal form

R) Conjunctive normal form if it has this form F1 /\ F2 /\ ….Fn. Where each F is a disjunction of literals. Example: (p\/q) /\ ( p\/ q)

7)      Transform the following into conjunctive normal forms:

a)      P \/ (~P /\ Q /\ R)

(P \/ ~P) /\ ( P \/ Q) /\ (P \/ R)   LQ6

 True /\ ( P \/ Q) /\ ( P \/ R)

b)      ~(P -> Q)

~( ~ P \/ Q)   LQ2

(P /\ ~Q) LQ4

c)       (P -> Q) -> r

( ~P \/ Q) -> r LQ2

~( ~P \/ Q) \/ R LQ2

( P /\ ~Q) \/ R  LQ4

(R \/ P) /\ ( R \/ ~Q) LQ6

8)      State the resolution principle

                R) any two clauses C1 and C2, if there is a literal L1 and C1 that is complementary to a literal L2 in C2,then delete L1 and L2 from C1 and C2 , and construct disjunction of the remained clauses .The constructed clause is called the resolve of C1 and C2              

9)      Define what is meant by resolution deduction

R) Given a set S of clauses, a resolution deduction of clause C from S is a finite sequence C1,C2,…Cn

Of clauses such that C = cn and each Ci is either a clause in S or A resolve of clauses preceding Ci, A deduction of square from S is said to be a proof of j.

10)   Show by means of resolution that the formula U is logical consequence of the three formulas ( P ->S) and ( S -> U) and P

R)

1) (P -> S) part of G

 2) (S -> U) part of G

3) P part of G

4) ~U negation of Goal

5) (~P \/ S)  DNF

6) (~S \/ U) DNF'
7) S ( Resolving of 5+3)
8)~S(Resolving of  6+4)

9) SQUARE

11)   Show by means of the inconsistency truth table approach that the formula U is  a logical consequence of the three formulas ( P->S) and ( S -> U) and P

R)

12)   Define Horn clause

R) A Horn clause is a clause (a disjunction of literals) with at most one positive, unnegated  , literal. Conversely, a disjunction of literals with at most one negated literal is called a dual-Horne Clause.

13)   Can the formula ( P/\ Q /\ R) -> s be converted to a Horn clause

R) Yes.

~(P /\ Q /\ R) \/ S

(~P /\ ~Q /\ ~R ) \/ S

(~P \/ S) /\ (~Q \/ S) /\ (~R\/S)

(P -> S) /\ ( Q -> S) /\ (R -> S)