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)
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)
