UNIT-III

Syllabus

Logic concepts: Introduction, propositional calculus, proportional logic, natural deduction

system, axiomatic system, semantic tableau system in proportional logic, resolution refutation in
proportional logic, predicate logic.

INTRODUCTION TO LOGIC

Symbolic Logic was being used to represent knowledge even before the advent of digital
computers. Today First Order Predicate Logic (FOPL) or simple Predicate Logic plays an
important role in AI for the representation of knowledge. A familiarity with FOPL is important.
It offers the only formal approach to r4easoning that has a sound theoretical foundation, this is
important in the attempts to automate the reasoning process, because inference should be correct
and logically sound. The structure of FOPL is flexible and it permits accurate representation of
natural language reasonably well.

Logic is a formal method for reasoning. Many concepts which can be verbalized can be
translated into symbolic representations which closely approximate the meaning of these
concepts. These symbolic structures can then be manipulated in programs to deduce various
facts, to carry out a form of automated reasoning . in predicate logic statements from a natural
language like English are translated into symbolic structures comprised of predicates, functions,
variables, constants, quantifiers and logical connectives. The symbols form the basic building
blocks for the knowledge, and their combination into valid structures is accomplished using the
syntax of FOPL. Once structures have been created to represent basic facts, inference rules may
then be applied to compare, combine and transform these “assumed” structures into new
“deduced” structures. This is how automated reasoning or inferencing is performed.

PROPOSITIONAL CALCULUS, PROPORTIONAL LOGIC

Propositional calculus is a branch of logic. It is also called propositional logic, statement

logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with

48
propositions (which can be true or false) and argument flow. Compound propositions are formed
by connecting propositions by logical connectives. The propositions without logical connectives
are called atomic propositions.Unlike first-order logic, propositional logic does not deal with
non-logical objects, predicates about them, or quantifiers. However, all the machinery of
propositional logic is included in first-order logic and higher-order logics. In this sense,
propositional logic is the foundation of first-order logic and higher-order logic.

Propositional logic (PL) is the simplest form of logic where all the statements are made
by propositions. A proposition is a declarative statement which is either true or false. It is a
technique of knowledge representation in logical and mathematical form.

Example:

a) It is Sunday.

b) The Sun rises from West (False proposition)

c) 3+3= 7(False proposition)

d) 5 is a prime number.

Following are some basic facts about propositional logic:

Propositional logic is also called Boolean logic as it works on 0 and 1.

In propositional logic, we use symbolic variables to represent the logic, and we can use any
symbol for a representing a proposition, such A, B, C, P, Q, R, etc.

Propositions can be either true or false, but it cannot be both.

Propositional logic consists of an object, relations or function, and logical connectives.

Logical Connectives:

Logical connectives are used to connect two simpler propositions or representing a sentence
logically. We can create compound propositions with the help of logical connectives. There are
mainly five connectives, which are given as follows:

49
 1. Negation: A sentence such as ¬ P is called negation of P. A literal can be either Positive
literal or negative literal.
2. Conjunction: A sentence which has ∧ connective such as, P ∧ Q is called a conjunction.
Example: Rohan is intelligent and hardworking. It can be written as,
P= Rohan is intelligent,
Q= Rohan is hardworking. → P∧ Q.

3. Disjunction: A sentence which has ∨ connective, such as P ∨ Q. is called disjunction,

where P and Q are the propositions.
Example: "Ritika is a doctor or Engineer",
Here P= Ritika is Doctor. Q= Ritika is Doctor, so we can write it as P ∨ Q.
4. Implication: A sentence such as P → Q, is called an implication. Implications are also
known as if-then rules. It can be represented as
            If it is raining, then the street is wet.
        Let P= It is raining, and Q= Street is wet, so it is represented as P → Q
5. Biconditional: A sentence such as P⇔ Q is a Biconditional sentence, example If I am
breathing, then I am alive
            P= I am breathing, Q= I am alive, it can be represented as P ⇔ Q.

NATURAL DEDUCTION SYSTEM

Natural deduction is a kind of proof calculus in which logical reasoning is expressed by

inference rules closely related to the "natural" way of reasoning

In natural deduction each logical connective and quantifier is characterized by its

introduction rule(s) which specifies how to infer that a conjunction, disjunction, etc. is true. The
elimination rule for the logical constant tells what other truths we can deduce from the truth of a
conjunction, disjunction, etc. Introduction and elimination rules must match in a certain way in
order to guarantee that the rules are meaningful and the overall system can be seen as capturing
mathematical reasoning.

The first is a local soundness property: if we introduce a connective and then immediately
eliminate it, we should be able to erase this detour and find a more direct derivation of the

50
conclusion without using the connective. If this property fails, the elimination rules are too
strong: they allow us to conclude more than we should be able to know. The second is a local
completeness property: we can eliminate a connective in a way which retains sufficient
information to reconstitute it by an introduction rule. If this property fails, the elimination rules
are too weak: they do not allow us to conclude everything we should be able to know. We
provide evidence for local soundness and completeness of the rules by means of local reduction
and expansion judgments, which relate proofs of the same proposition.

Conjunction Elimination (  Elim ) Conjunction Introduction (  Intro )

{  }

⊢  (or ) {, }

⊢  

Disjunction Elimination (  Elim ) Disjunction Introduction (  Intro )

{   ,  ⊢ ,  ⊢ } { (or )}

⊢ ⊢  

Negation Elimination (  Elim ) Negation Introduction (  Intro )

{} { ⊢ }

⊢ ⊢ 

51
Contradiction Elimination (  Elim ) Contradiction Introduction (  Intro )

{} {, }

⊢ ⊢

Conditional Elimination (  Elim ) Conditional Introduction (  Intro )

{  , } { ⊢ }

⊢ ⊢

Biconditional Elimination (  Elim ) Biconditional Introduction (  Intro )

{   (or   ), } { ⊢ ,  ⊢ }

⊢ ⊢

AXIOMATIC SYSTEM

52
 Axiomatic System (Postulate System)

1. Undefined terms/primitive terms

2. Defined terms
3. Axioms/postulates - accepted unproved statements
4. Theorems - proved statements
An axiomatic system consists of some undefined terms (primitive terms) and a list of
statements, called axioms or postulates, concerning the undefined terms. One obtains a
mathematical theory by proving new statements, called theorems, using only the axioms
(postulates), logic system, and previous theorems. Definitions are made in the process in order to
be more concise.

Most early Greeks made a distinction between axioms and postulates. Evidence exists
that Euclid made the distinction that an axiom (common notion) is an assumption common to all
sciences and that a postulate is an assumption peculiar to the particular science being studied.
Now in modern times no distinction is made between the two; an axiom or postulate is an
assumed statement.

Usually an axiomatic system does not stand alone, but other systems are also assumed
to hold. For example, we will assume:

1. The real number system,

2. Some set theory,
3. Aristotelian logic system, and
4. The English language.
We will not develop any of these but use what we need from them.

One of the pitfalls of working with a deductive system is too great a familiarity with
the subject matter of the system. We need to be careful with what we are assuming to be true
and with saying something is obvious while writing a proof. We need to take extreme care that
we do not make an additional assumption outside the system being studied. A common error in
the writing of proofs in geometry is to base the proof on a picture. A picture may be misleading,
either by not covering all possibilities, or by reflecting our unconscious bias as to what is correct.
It is crucially important in a proof to use only the axioms and the theorems which have been

53
derived from them and not depend on any preconceived idea or picture. Pictures should only be
used as an intuitive aid in developing the proof, but each step in the proof should depend only on
the axioms and the theorems with no dependence upon any picture. Diagrams should be used as
an aid, since they are useful in developing conceptual understanding, but care must be taken that
the diagrams do not lead to misunderstanding. Two exercises in Chapter Two illustrate this
point: (1) A false proof that all triangles are isosceles. (2) A faulty proof of a valid theorem.

Usually not all the axioms are given at the beginning of the development of an
axiomatic system; this allows us to prove very general theorems which hold for many axiomatic
systems. An example from abstract algebra is: group theory → ring theory → field theory. A
second example is a parallel postulate is often not introduced early in studies of Euclidean
geometry, so the theorems developed will hold for both Euclidean and hyperbolic geometry
(called a neutral geometry).

Certain terms are left undefined to prevent circular definitions, and the axioms are
stated to give properties to the undefined terms. Undefined terms are of two types: terms that
imply objects, called elements, and terms that imply relationships between objects, called
relations. Examples of undefined terms (primitive terms) in geometry are point, line, plane, on,
and between. For these undefined terms, on and between would indicate some undefined
relationship between undefined objects such as point and line. An example would be: A point is
on a line. Early geometers tried to define these terms:

point Pythagoreans, “a monad having position"

Plato, “the beginning of a line"

Euclid, “that which has no part"

line Proclus, “magnitude in one dimension", “flux of a point"

Euclid, “breadthless length"

Euclid made the attempt to define all of his terms. (See Exit book to another
website.Euclid's Elements.) Now, points are considered to come before lines, but no effort is
made to define them a priori. Instead, material things are used as illustrations/models to obtain

54
the abstract idea. The famous mathematician David Hilbert (1862–1943) is quoted as saying,
“we may as well be talking about chairs, coffee tables and beer mugs." An axiomatic system
is consistent if there is no statement such that both the statement and its negation are axioms or
theorems of the axiomatic system. Since contradictory axioms or theorems are usually not
desired in an axiomatic system, we will consider consistency to be a necessary condition for an
axiomatic system. An axiomatic system that does not have the property of consistency has no
mathematical value and is generally not of interest.

A model of an axiomatic system is obtained if we can assign meaning to the undefined

terms of the axiomatic system which convert the axioms into true statements about the assigned
concepts. Two types of models are used concrete models and abstract models. A model is
concrete if the meanings assigned to the undefined terms are objects and relations adapted from
the real world. A model is abstract if the meanings assigned to the undefined terms are objects
and relations adapted from another axiomatic development.

SEMANTIC TABLEAU SYSTEM IN PROPORTIONAL LOGIC

A semantic tableau is a method for determining validity of arguments in a certain class of

logics. The method is perhaps not so well-known to the automated theorem proving community
as resolution, but it has long been present in the logic community. 1 As its name suggests, the
method uses semantic facts about the language in an attempt to generate a counter model for the
argument at hand (or to show that there is no such counter-model and that the argument is
therefore valid). In this, the method bears a strong similarity to Resolution, but it does not require
any conversion to a normal form. The method is also different in being an analytic system: each
non-initial formula in any proof is a sub formula of some earlier formula in the proof. Natural
deduction is not analytic in this sense, nor is any Resolution method other than Unit Resolution.
There are various different formats for stating the method of semantic tableaux. Participants in
this AAAI Symposium are doubtless familiar with the form given by Fitting (1988). The method
he uses is quite similar to the method I wish to employ, and there should be no difficulty in
transforming the one into the other. In this note, I am interested in extending my method to a

55
certain class of modal logics. In this extension we will only consider propositional logics – a fact
that lends some considerable simplification to the description of the tableaux method.

Semantic tableaux, when done in the method are fact trees; and the method of making a
tableau is in fact a method of tree construction. Like Resolution, it is a refutation method; and
therefore it starts with abnegated conclusion” form of an argument to be tested.(Unlike
Resolution, there is no further pre-processing of formulas, such as conversion to a normal form.)
The root of the tree contains all the premises and the negation of the conclusion. The
construction of the rest of the tree is governed by “branching rules”, which operate (by
decomposition) on formulas already in the tree.

RESOLUTION WITH REFUTATION METHOD

Resolution with refutation method uses a generalized version of the resolution rule of
inference we saw in the previous lecture. It has been mathematically proven to be refutation-
complete over first order logic. This means that if you write any set of sentences in first order
logic which are unsatisfiable (i.e., taken together they are false, in that they have no models),
then the resolution method will eventually derive the False symbol, indicating that the sentences
somehow contradict each other.

56
 In particular, if the set of first order sentences comprises a set of axioms and the negation
of a theorem you want to prove, the resolution method can be used in a proof-by-contradiction
approach. This means that, if your first order theorem is true then proof by contradiction using
the resolution method is guaranteed to find the proof to a theorem eventually. The underlining
here identifies some drawbacks to resolution theorem proving:It only works for true theorems
which can be expressed in first order logic: it cannot check at the same time whether a conjecture
is true or false, and it can't work in higher order logics. (There are related techniques which
address these problems, to varying degrees of success.)

While it is proven that the method will find the solution, in practice the search space is
often too large to find one in a reasonable amount of time, even for fairly simple theorems.
Notwithstanding these drawbacks, resolution theorem proving is a complete method: if your
theorem does follow from the axioms of a domain, then resolution can prove it. Moreover, it
only uses one rule of deduction (resolution), rather than the multitude we saw in the last lecture.
Hence, it is comparatively easy to understand how resolution theorem provers work. For these
reasons, the development of the resolution method was a major accomplishment in logic, with
serious implications to Artificial Intelligence research.

Resolution works by taking two sentences and resolving them into one, eventually
resolving two sentences to produce the False statement. The resolution rule is more complicated
than the rules of inference we've seen before, and we need to cover some preparatory notions
before we can understand how it works. In particular, we need to look at conjunctive normal
form and unification before we can state the full resolution rule at the heart of the resolution
method.

Binary Resolution

We saw unit resolution (a propositional inference rule) in the previous lecture:

A B, ¬B

57
We can take this a little further to propositional binary resolution:

A B, ¬B C

A C

Binary resolution gets its name from the fact that each sentence is a disjunction of exactly two
literals. We say the two opposing literals B and ¬B are resolved — they are removed when the
disjunctions are merged.The binary resolution rule can be seen to be sound because if both A and
C were false then then at least one of the sentences on the top line would be false. As this is an
inference rule, we are assuming that the top line is true. Hence we can't have both A and C being
false, which means either A or C must be true. So we can infer the bottom line.

PREDICATE LOGIC

A predicate is an expression of one or more variables defined on some specific domain.

A predicate with variables can be made a proposition by either assigning a value to the variable
or by quantifying the variable. The following are some examples of predicates − Let E(x, y)
denote "x = y".

We can form two different predicates. ... Definition: A predicate is a property that a
variable or a finite collection of variables can have. A predicate becomes a proposition when
specific values are assigned to the variables. P(x1,x2, ..., xn) is called a predicate of n variables
or n arguments.

58