Bài giảng Discrete Structures for Computing - Chapter 1a: Propositional Logic
Propositional Logic
Nguyen An Khuong,
Huynh Tuong Nguyen
Chapter 1a
Propositional Logic
Discrete Structures for Computing (CO1007)
Contents
Introduction
Declarative Sentences
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
(Materials drawn from Chapter 1 in:
“Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and
Reasoning about Systems, 2nd Ed., Cambridge University Press, 2006.”)
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Nguyen An Khuong, Huynh Tuong Nguyen
Faculty of Computer Science and Engineering
University of Technology, VNU-HCM
Required
Texts/Materials
1a.1
Propositional Logic
Contents
Nguyen An Khuong,
Huynh Tuong Nguyen
1 Propositional Calculus: Declarative Sentences
2 Propositional Calculus: Natural Deduction
Sequents
Contents
Rules for natural deduction
Basic and Derived Rules
Excursion: Intuitionistic Logic
Introduction
Declarative Sentences
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
3 Propositional Logic as a Formal Language
4 Semantics of Propositional Logic
Meaning of Logical Connectives
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and Completeness
Preview: Soundness and
Completeness
5 Conjunctive Normal Form
6 Required Texts/Materials
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.2
Propositional Logic
Nguyen An Khuong,
Huynh Tuong Nguyen
1 Propositional Calculus: Declarative Sentences
2 Propositional Calculus: Natural Deduction
3 Propositional Logic as a Formal Language
4 Semantics of Propositional Logic
5 Conjunctive Normal Form
Contents
Introduction
Declarative Sentences
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Meaning of Logical
Connectives
6 Required Texts/Materials
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.3
Propositional Logic
Propositional Calculus
Nguyen An Khuong,
Huynh Tuong Nguyen
Study of atomic propositions
Propositions are built from sentences whose internal structure is
not of concern.
For “atomic propositions”, see slide 1a.59
Contents
Introduction
Building propositions
Declarative Sentences
Natural Deduction
Sequents
Boolean operators are used to construct propositions out of
simpler propositions.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Example for Propositional Calculus
Meaning of Logical
Connectives
•
•
Atomic proposition: One plus one equals two.
Preview: Soundness and
Completeness
Atomic proposition: The earth revolves around the sun.
Normal Form
•
Combined proposition: One plus one equals two and the
earth revolves around the sun.
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.4
Propositional Logic
Goals and Main Result of Propositional Calculus
Nguyen An Khuong,
Huynh Tuong Nguyen
Meaning of formula
Associate meaning to a set of formulas by assigning a value true or
false to every formula in the set.
Contents
Introduction
Declarative Sentences
Proofs
Natural Deduction
Sequents
Symbol sequence that formally establishes whether a formula is
always true.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Soundness and completeness
Meaning of Logical
Connectives
The set of provable formulas is the same as the set of formulas
which are always true.
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.5
Propositional Logic
Uses of Propositional Calculus
Hardware design
Nguyen An Khuong,
Huynh Tuong Nguyen
The production of logic circuits uses propositional calculus at all
phases; specification, design, testing.
Contents
Introduction
Declarative Sentences
Verification
Natural Deduction
Sequents
Verification of hardware and software makes extensive use of
propositional calculus.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Problem solving
Meaning of Logical
Connectives
Decision problems (scheduling, timetabling, etc) can be expressed
as satisfiability problems in propositional calculus.
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.6
Propositional Logic
Predicate Calculus: Central ideas
Richer language
Nguyen An Khuong,
Huynh Tuong Nguyen
Instead of dealing with atomic propositions (biến mệnh đề/mệnh
đề nguyên tử), predicate calculus provides the formulation of
statements involving sets, functions and relations on these sets.
Contents
Introduction
Declarative Sentences
Natural Deduction
Sequents
Quantifiers
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Predicate calculus provides statements that all or some elements
of a set have specified properties.
Formal Language
Semantics
Compositionality
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
Similar to propositional calculus, formulas can be built from
composites using logical connectives.
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.7
Propositional Logic
The uses of Predicate Calculus
Nguyen An Khuong,
Huynh Tuong Nguyen
Progamming Language Semantics
The meaning of programs such as
Contents
ifx >= 0theny := sqrt(x)elsey := abs(x)
Introduction
can be captured with formulas of predicate calculus:
Declarative Sentences
√
∀x∀y(x0 = x ∧ (x ≥ 0 → y0 = x) ∧ (¬(x ≥ 0) → y0 = |x|))
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Other Uses of Predicate Calculus
Formal Language
Semantics
•
Specification: Formally specify the purpose of a program in order to
serve as input for software design,
Meaning of Logical
Connectives
•
Verification: Prove the correctness of a program with respect to its
specification.
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.8
Propositional Logic
An Example for Specification
Nguyen An Khuong,
Huynh Tuong Nguyen
Let P be a program of the form
Contents
Introduction
while a <> b do
Declarative Sentences
if a > b then a := a - b else a:= b - a;
Natural Deduction
Sequents
The specification of the program is given by the formula
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
{a ≥ 0 ∧ b ≥ 0} P {a = gcd(a, b)}
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.9
Propositional Logic
Logic in Theorem Proving, Logic Programming, and Other
Systems of Logic
Nguyen An Khuong,
Huynh Tuong Nguyen
Theorem proving
Formal logic has been used to design programs that can
automatically prove mathematical theorems.
Logic programming
Contents
Introduction
Research in theorem proving has led to an efficient way of proving
formulas in predicate calculus, called resolution, which forms the
basis for logic programming.
Declarative Sentences
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Some Other Systems of Logic
Formal Language
Semantics
•
Three-valued logic: A third truth value (denoting “don’t
know” or “undetermined”) is often useful.
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
•
Intuitionistic logic: A mathematical object is accepted only
if a finite construction can be given for it.
Normal Form
Homeworks and Next
Week Plan?
•
Temporal logic: Integrates time-dependent constructs such
as (“always” and “eventually”) explicitly into a logic
Required
Texts/Materials
framework; useful for reasoning about real-time systems.
1a.10
Propositional Logic
Nguyen An Khuong,
Huynh Tuong Nguyen
1 Propositional Calculus: Declarative Sentences
2 Propositional Calculus: Natural Deduction
3 Propositional Logic as a Formal Language
4 Semantics of Propositional Logic
5 Conjunctive Normal Form
Contents
Introduction
Declarative Sentences
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Meaning of Logical
Connectives
6 Required Texts/Materials
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.11
Propositional Logic
Declarative Sentences
Nguyen An Khuong,
Huynh Tuong Nguyen
The language of propositional logic is based on propositions or
declarative sentences.
Declarative Sentences
Sentences which one can—in principle—argue as being true or
false.
Contents
Introduction
Examples
Declarative Sentences
Natural Deduction
Sequents
1 The sum of the numbers 3 and 5 equals 8.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
2 Jane reacted violently to Jack’s accusations.
3 Every natural number > 2 is the sum of two prime numbers.
4 All Martians like pepperoni on their pizza.
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
Not Examples
Normal Form
•
•
Homeworks and Next
Week Plan?
Could you please pass me the salt?
Ready, steady, go!
Required
Texts/Materials
•
May fortune come your way.
1a.12
Propositional Logic
Putting Propositions Together
Example 1.1
Nguyen An Khuong,
Huynh Tuong Nguyen
If the train arrives late and
there are no taxis at the station then
John is late for his meeting.
John is not late for his meeting.
The train did arrive late.
Contents
Introduction
Declarative Sentences
Natural Deduction
Sequents
Therefore, there were taxis at the station.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Example 1.2
Formal Language
Semantics
If it is raining and
Meaning of Logical
Connectives
Jane does not have her umbrella with her then
she will get wet.
Preview: Soundness and
Completeness
Normal Form
Jane is not wet.
Homeworks and Next
Week Plan?
It is raining.
Required
Texts/Materials
Therefore, Jane has her umbrella with her.
1a.13
Propositional Logic
Focus on Structure
Nguyen An Khuong,
Huynh Tuong Nguyen
We are primarily concerned about the structure of arguments in
this class, not the validity of statements in a particular domain.
We therefore simply abbreviate sentences by letters such as p, q, r,
p1, p2 etc.
From Concrete Propositions to Letters - Example 1.1
Contents
Introduction
If the train arrives late and
Declarative Sentences
there are no taxis at the station then
John is late for his meeting.
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
John is not late for his meeting.
The train did arrive late.
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
Therefore, there were taxis at the station.
Normal Form
becomes
Homeworks and Next
Week Plan?
Letter version
Required
Texts/Materials
If p and not q, then r. Not r. p. Therefore, q.
1a.14
Propositional Logic
Focus on Structure
Nguyen An Khuong,
Huynh Tuong Nguyen
From Concrete Propositions to Letters - Example 1.2
If it is raining and
Jane does not have her umbrella with her then
she will get wet.
Contents
Introduction
Declarative Sentences
Jane is not wet.
It is raining.
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Therefore, Jane has her umbrella with her.
Meaning of Logical
Connectives
has
Preview: Soundness and
Completeness
the same letter version
Normal Form
If p and not q, then r. Not r. p. Therefore, q.
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.15
Propositional Logic
Logical Connectives
Notations/Symbols
Nguyen An Khuong,
Huynh Tuong Nguyen
Sentences like “If p and not q, then r.” occur frequently. Instead
of English words such as “if...then”, “and”, “not”, it is more
convenient to use symbols such as →, ∧, ¬.
Contents
Introduction
Declarative Sentences
¬: negation of p is denoted by ¬p.
Natural Deduction
Sequents
∨: disjunction of p and r is denoted by p ∨ r, meaning at least
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
one of the two statements is true.
∧: conjunction of p and r is denoted by p ∧ r, meaning both are
Formal Language
Semantics
true.
Meaning of Logical
Connectives
→: implication between p and r is denoted by p → r, meaning
that r is a logical consequence of p. p is called the antecedent
(mệnh đề đứng trước), and r the consequent (mệnh đề kết
quả).
Preview: Soundness and
Completeness
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.16
Propositional Logic
Example 1.1 Revisited
From Example 1.1
Nguyen An Khuong,
Huynh Tuong Nguyen
If the train arrives late and
there are no taxis at the station then
John is late for his meeting.
Contents
Introduction
Declarative Sentences
Symbolic Propositions
Natural Deduction
Sequents
We replaced “the train arrives late” by p, etc.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
The statement becomes: If p and not q, then r.
Formal Language
Semantics
Meaning of Logical
Connectives
Symbolic Connectives
Preview: Soundness and
Completeness
With symbolic connectives, the statement becomes:
Normal Form
p ∧ ¬q → r
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.17
Propositional Logic
Nguyen An Khuong,
Huynh Tuong Nguyen
1 Propositional Calculus: Declarative Sentences
2 Propositional Calculus: Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Contents
Introduction
Excursion: Intuitionistic Logic
Declarative Sentences
Natural Deduction
Sequents
3 Propositional Logic as a Formal Language
4 Semantics of Propositional Logic
5 Conjunctive Normal Form
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
Normal Form
6 Required Texts/Materials
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.18
Propositional Logic
Introduction
Objective
Nguyen An Khuong,
Huynh Tuong Nguyen
We would like to develop a calculus for reasoning about
propositions, so that we can establish the validity of statements
such as Example 1.1.
Contents
Introduction
Declarative Sentences
Natural Deduction
Sequents
Idea
We introduce proof rules that allow us to derive a formula ψ from
a number of other formulas φ1, φ2, . . . φn.
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Notation
Meaning of Logical
Connectives
We write a sequent φ1, φ2, . . . , φn ` ψ
Preview: Soundness and
Completeness
to denote that we can derive ψ (conclusion - kết luận) from
φ1, φ2, . . . , φn (premises - các tiền đề).
Normal Form
Homeworks and Next
Week Plan?
Required
Texts/Materials
1a.19
Propositional Logic
Example 1.1 Revisited
English
Nguyen An Khuong,
Huynh Tuong Nguyen
If the train arrives late and
there are no taxis at the station then
John is late for his meeting.
Contents
John is not late for his meeting.
The train did arrive late.
Therefore, there were taxis at the station.
Sequent
Introduction
Declarative Sentences
Natural Deduction
Sequents
Rules for natural deduction
Basic and Derived Rules
Intuitionistic Logic
Formal Language
Semantics
Meaning of Logical
Connectives
Preview: Soundness and
Completeness
p ∧ ¬q → r, ¬r, p ` q
Normal Form
Homeworks and Next
Week Plan?
Remaining task
Required
Texts/Materials
Develop a set of proof rules that allows us to establish such
sequents.
1a.20
Tải về để xem bản đầy đủ
78 trang
18680
Free
Bạn đang xem 20 trang mẫu của tài liệu "Bài giảng Discrete Structures for Computing - Chapter 1a: Propositional Logic", để tải tài liệu gốc về máy hãy click vào nút Download ở trên
File đính kèm:
- bai_giang_discrete_structures_for_computing_chapter_1a_propo.pdf
