Transcript Introduction

Logic Seminar 1
Introduction
24.10.2005.
Slobodan Petrović
Introduction
• It has long been man’s ambition to find a general decision
procedure to prove theorems.
• This desire dates back to Leibniz (1646-1716).
• It was revived by Peano in the beginning of the 20th
century and by Hilbert's school in the 1920s.
• A very important theorem was proved by Herbrand in
1930: he proposed a mechanical method to prove
theorems.
• Unfortunately, his method was very difficult to apply since
it was extremely time consuming to carry out by hand.
Introduction
• With the invention of digital computers,
logicians regained interest in mechanical
theorem proving.
• In 1960, Herbrand’s procedure was
implemented by Gilmore on a digital
computer.
• A more efficient procedure was proposed by
Davis and Putnam.
Introduction
• A major breakthrough in mechanical theorem
proving was made by J. A. Robinson in 1965.
• He developed a single inference rule, the
resolution principle, which was shown to be
highly efficient and very easily implemented on
computers.
• Since then, many improvements of the resolution
principle have been made.
Introduction
• Mechanical theorem proving has been
applied to many areas, such as program
analysis, program synthesis, deductive
question-answering systems, problemsolving systems, and robot technology.
• In the field of computer security, it has been
applied in protocol analysis.
Introduction
• There are many points of view from which we can
study symbolic logic.
• Traditionally, it has been studied from
philosophical and mathematical orientations.
• We are interested in the applications of symbolic
logic to solving intellectually difficult problems.
• We want to use symbolic logic to represent
problems and to obtain their solutions.
Introduction
• A simple example.
•
•
Assume that we have the following facts:
– F1: If it is hot and humid, then it will rain.
– F2: If it is humid, then it is hot.
– F3: It is humid now.
The question is: Will it rain?
• Let P, Q, and R represent “It is hot,” “It is
humid,” and “It will rain,” respectively.
Introduction
• We shall use  to represent “and” and  to
represent “imply”.
• Then, the three facts are represented as:
– F1: P  Q  R
– F2: Q  P
– F3: Q.
• Thus, English sentences have been
translated into logical formulas.
Introduction
• It can be shown that whenever F1, F2, and F3
are true, the formula
– F4: R
• is true.
• Therefore, we say that F4 logically follows
from F1, F2, and F3.
• That is, it will rain.
Introduction
• Example. We have the following facts:
– F1: Confucius is a man.
– F2: Every man is mortal.
• To represent F1 and F2, we need a concept
of predicate.
• We may let P(x) and Q(x) represent “x is a
man” and “x is mortal,” respectively.
• We also use (x) to represent “for all x”.
Introduction
• We can now represent the facts by logical
expressions:
– F1: P(Confucius)
– F2: (x)(P(x)Q(x))
• From F1 and F2, we can logically deduce:
– F3: Q(Confucius)
• which means that Confucius is mortal.
Introduction
• In the examples, we essentially had to prove that a
formula logically follows from other formulas.
• We call a statement that a formula logically
follows from other formulas a theorem.
• A demonstration that a theorem is true, i.e. that a
formula logically follows from other formulas, is
called a proof of the theorem.
• The problem of mechanical theorem proving is to
consider mechanical methods for finding proofs of
theorems.