PPT - University of Alberta

download report

Transcript PPT - University of Alberta

CMPUT 272
Formal Systems & Logic in CS
I. E. Leonard
University of Alberta
http://www.cs.ualberta.ca/~isaac/cmput272/f03
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
1
Chapter 2.1
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
All images are copyrighted to their respective copyright holders and reproduced here for academic purposes under the condition of “fair using”.
Today
2
Announcement
It is Ok for an assignment problem to
refer to the material that is:
Not covered in class by the due date
Not covered in class at all
Why?
Because the lectures only highlight the
material in the textbook
They are not a substitute for reading
the text
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
3
The Big Picture
Logic is being used to verify validity of
arguments
An argument is valid iff its conclusion logically
follows from the premises
Derivations are used to prove validity
Inference rules are used as part of
derivations
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
4
Summary
Logical implication/entailment:
A entails/logically implies B
B follows from A
AB is a valid argument
A is a sufficient condition for B
B is a necessary condition for A
If A holds then B holds
A may be “stronger than” B
Formula F=(AB) is a tautology
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
5
Summary
Equivalence:
AB
A holds iff B holds
A is a criterion for B, B is a criterion for A
A  B, B  A
A and B are “equivalently strong”
Formula F=(AB) is a tautology
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
6
Clarification #1
We have used the following expressions
synonymously:
A entails B
A logically implies B
(A therefore B) is a valid argument
B logically follows from A
In reality there are some subtle differences
Technically we mean:
“A logically implies B”
Every model for A is also a model for B
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
7
Clarification #2
Can computers generate a derivation/proof
given a conclusion and a set of premises?
Propositional logic is decidable:
the tabular method
application of inference rules
Predicate logic is semi-decidable
If a proof exists then it can (theoretically) be
found by machines
If the proof doesn’t exist then the algorithm may
not stop
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
8
Clarification #3
Derivation of a statement:
a sequence of statements
start with the premises
each statement logically follows from the
previous statements
at some point the conclusion is arrived at
Derivations are annotated with the
inference rules used
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
9
Questions?
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
10
De Morgan’s Laws
Let’s get some practice in deriving
Theorem 1.1.1 equivalences from
Boolean algebra
Page 14 in the text
A solution is posted on my webpage
under the “Notes” section
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
11
Questions?
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
12
Limitations of Propositional Logic
Let’s get back to Socrates
“All people are mortal”
“Socrates is a man”
“Socrates is mortal”
Can we formalize this in propositional logic?
Our previous attempt was:
“If Socrates is a man then Socrates is mortal”
“Socrates is a man”
“Socrates is mortal”
Clearly NOT the same!
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
13
What is the matter?
The problem is:
We operate with constant objects only
We have no domain context and no
domain variables
We cannot say “all”, “is a”, etc.
Solution?
Predicate Logic
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
14
Predicate Logic
Logic objects (constants/variables):
P, Q, R, …
true, false
Connectives:
&, v, , …
Domain objects (constants/variables):
Socrates, CMPUT272
Predicates:
Mortal(Socrates)
TaughtAtUofA(CMPUT272)
Happened(snow,yesterday)
Quantifiers:
For all, There exist
Statements/formulae:
Atomic, conjunctive, etc.
Quantified (universally / existentially)
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
15
Translation Examples
“Every man is mortal”
x [man(X)  mortal(x)]
“Socrates is a man”
man(Socrates)
“Socrates is mortal”
mortal(Socrates)
The last statement logically follows from
the premises (by universal elimination)
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
16
Translation Examples
“Nothing is better than God”
~[x better-than(x,God)]
“A sandwich is better than nothing”
x [sandwich(x)  better-than(x,Nothing)]
“A sandwich is better than God”
x [sandwich(x)  better-than(x,God)]
The last statement does not logically
follow from the premises
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
17
More translations
“Ducks fly”
x [duck(x)  flies(x)]
“F-16s fly”
x [F-16(x)  flies(x)]
“F-16s are ducks”
x [F-16(x)  duck(x)]
The last statement does not logically
follow from the premises
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
18
Translation Examples
“No man lives forever”
~[x [man(x) & lives-forever(x)]]
x [man(x)  ~lives-forever(x)]
“Every person is a Knave or a Knight”
x [person(x)  [Knave(x) v Knight(x)]]
“Every person is a Knave or a Knight
but not both”
x [person(x)  [Knave(x) v Knight(x)] &
~[Knave(x) & Knight(x)]]
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
19
Questions?
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
20
Predicate Logic
Logic objects (constants/variables):
P, Q, R, …
true, false
Connectives:
&, v, , …
Domain objects (constants/variables):
Socrates, CMPUT272
Predicates:
Mortal(Socrates)
TaughtAtUofA(CMPUT272)
Happened(snow,yesterday)
Quantifiers:
For all, Exists
Statements/formulae:
Atomic, conjunctive, etc.
Quantified (universally / existentially)
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
21
Domain Objects
We can now have variables and
constants of a non-Boolean nature:
Socrates is a constant (a specific member)
in the set of all people
X is a variable over the set of people
i.e., X can be any person
We can instantiate X=Socrates
Domain of a variable is the set of values
it can take on
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
22
Predicates
Predicates map from the domain sets of predicate
variables to {true,false}
General form:
P(v1,…,vN)
Example:
Mortal(X)
Mortal is the predicate name
X is the predicate variable runs over people and elves
Mortal(X) maps X to true/false depending on whether
X is mortal or not
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
23
Predicates
In other words:
Predicates take domain objects and map
them to true/false depending on the
properties of the objects
Thus, a predicate with all its variables
instantiated is a statement (i.e., true/false)
Example:
BetterThan(v1,v2)
BetterThan(Ferrari,nothing)=true
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
24
Truth Set
Suppose P(x) is “x is a factor of 8”
So how about the following:
P(1)
True
P(2)
True
P(0)
False
The set of all x such that P(x) holds is called
the truth set of P(x)
Here it would be {1,2,4,8}
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
25
Examples
Suppose P(x,y,r) is “x2+y2=r2”
What is the truth set of P(x,y,5)?
Circle with the radius of 5 centered in the
origin
Suppose P(n) is “n is an even threedigit prime number”
What is the truth set of P(n)?
An empty set
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
26
Questions?
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
27
A Lost Love?
But what about our dearly beloved
propositional statements?
PvQ
Here P and Q are propositional/Boolean
variables/statements
They don’t take any domain objects
They simply hold or don’t hold
How can we have them in the predicate
logic?
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
28
Fear Not!
A Boolean variable/constant (e.g.,
P=true) is simply a 0-arity predicate:
P()
So propositional logic is back!
Example: propositional Modus Ponens:
PQ
P
Thus, Q
Sept 16, 2003
P()  Q()
P()
Thus, Q()
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
29
Predicate Formulae
Everything from propositional logic
Boolean variables become 0-arity
predicates…
Additionally:
Predicates, e.g.:
Mortal(x)
Universally quantified formulae, e.g.:
x [man(x)  mortal(x)]
Existentially quantified formulae, e.g.:
x [man(x) & likes272(x)]
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
30
Recall: interpretation
In propositional logic interpretation is a
mapping/assignment of all propositional
variables to true/false
Example:
Formula: A v B
Interpretation: I
I(A)=true
I(B)=false
I(A v B)=true
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
31
Extended Interpretations
In predicate calculus to specify an interpretation we
need to:
Select domain sets
Assign all domain constants
Assign semantics to all predicates
Example:
Predicate formula: F=(x [likes(x,c272)])
A possible interpretation assigns:
Domain set for x : people
Domain value for 2nd argument of likes(a,b) : things
Domain value for constant c272 : class CMPUT 272
Semantics for predicate likes(a,b) : holds iff person a likes thing b
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
32
Evaluating formulae
Predicate formula: F=(x [likes(x,c272)])
A possible interpretation assigns:
Domain set for x : people
Domain value for 2nd argument of likes(a,b) : things
Domain value for constant c272 : class CMPUT 272
Semantics for predicate likes(a,b) : holds iff person a
likes thing b
So what is the value of formula F given the
interpretation? True/false?
How can we tell?
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
33
Evaluating Formula
0-arity predicate : P()
Interpretation directly
Predicate with variables : P(x)
Use the assignment of x and the semantics of P()
Universally quantified formula : x P(x)
Evaluates to true iff P(x) holds on all possible values of x
Existentially quantified formulae : x P(x)
Evaluates to true iff P(x) holds on at least one possible value of x
Sept 16, 2003
© Vadim Bulitko : CMPUT 272, Fall 2003, UofA
34