Computational Applied Logic

CSC 503 Fall 2005

Jon Doyle
Department of Computer Science
North Carolina State University
Propositional logic
NC State University 1 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Statements and their uses
What things can one express?
Sounds/exclamations/marks
Words
Statements
Sets of statements = theories
Partial statements
Sets of partial statements
Sequences of statements or sets of statements
NC State University 2 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Statements and their uses
How to do things with sentences
Declarative: facts and descriptions
Interrogative: questions
Imperative: commands and pleas
NC State University 3 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Statements and their uses
What can I express with statements?
Knowledge/facts/opinions/conditions
Ignorance/uncertainty
Goals/desires/intentions
Procedures/methods
Propositional attitudes
NC State University 4 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Language
Statements
Complete statements = propositions
Snow is white
Letters
snow-is-white
Four-score-and-seven-years-ago-
our-fathers-brought-forth-
on-this-continent-a-new-nation-
conceived-in-Liberty-
and-dedicated-to-the-proposition-
that-all-men-are-created-equal
Ignore spelling, just enumerate
A
1
, A
2
, . . .
NC State University 5 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Language
Propositional connectives
Disjunction or
Conjunction and
Negation not
Conditional implies
Biconditional iff = if and only if
+ Exclusive or xor
[ Sheffer stroke nand

n
at least n
And more besides, when we visit description logics
NC State University 6 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Language
Complex propositions
All combinators use parentheses to provide
unique parse tree.
We omit parentheses when parse is clear.
p = A B C
p = (((A) B) C)
Depth = depth of parse tree (root has depth 0)
Depth(p) = 3
Support = set of letters appearing in tree
Support(p) = A, B, C
NC State University 7 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Meaning of propositions
We only consider standard meanings at this time.
Standard meanings
True/False (= T/F, 1/0, /)
Multivalued logics
Elements of boolean lattices
Belnap 4-valued logic TT, TF, FT, FF
Probabilistic logics
Probability values in [0, 1]
Fuzzy logics
Possibility values in [0, 1]
NC State University 8 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Logicians are weird
Logical meaning ,= English (etc.) meaning
If 1=2, then Im the Man in the Moon.
She is either a lawyer or a professor.
Ive won every World Cup game Ive played.
Logical meaning is atemporal
10:00AM Assert
10:01AM Assert
Simple inconsistency, or change?
NC State University 9 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Truth functionality
Basic connectives are truth functional
Truth of compound statement determined by
truth of the connected substatements
Truth of compound a function of truth of
constituents
Truth tables represent these functions
NC State University 10 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Connective truth tables
( )
T T T
T F T
F T T
F F F
( )
T T T
T F F
F T F
F F F
()
T F
F T
NC State University 11 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Connective truth tables
( )
T T T
T F F
F T T
F F T
( )
T T T
T F F
F T F
F F T
NC State University 12 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Connective truth tables
( + )
T T F
T F T
F T T
F F F
( [ )
T T F
T F T
F T T
F F T
NC State University 13 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Truth tables
Complete truth tables
One column for each proposition in formation tree
Abbreviated truth tables
Omit one or more intermediate propositions
NC State University 14 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Non-truth-functional connectives
Truth values of component propositions do not
determine truth value of compound proposition.
because
causes
necessarily implies
preceded
is a shorter statement than
expresses more information than
is more likely than
Alice believes but Bob claims
NC State University 15 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Truth valuations
Truth assignment / : L T, F
Truth valuation 1 : L(L) T, F
Required to respect truth tables in every connective
Valuations must agree on a proposition
whenever they agree on the propositions
support
NC State University 16 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Logical equivalence

Means and are logically equivalent
Logical equivalence = agreement w.r.t. every
valuation
True just in case the truth table column for
contains only Ts
Each row corresponds to a class of valuations
Truth table summarizes all valuations restricted to
support of a proposition
NC State University 17 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Lattice of meanings
Propositional equivalence classes
[] = [
2
n
distinct truth tables over n letters
Thus 2
n
equivalence classes over n letters
Form a Boolean lattice with respect to , ,
Dene lattice order iff [ ] = []
NC State University 18 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Metalanguage vs. object language
is part of the logical metalanguage
Part of the language we use to talk about logical
statements
Not part of the logical object language in which
propositions are expressed.
Other metalinguistic notions:
Entailment
Satisability
Provability
NC State University 19 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Adequacy
What can one say with a specic set of connectives?
S is adequate iff every proposition is equivalent
to some proposition constructed using only
connectives in S
For every truth-functional , there is some
over S such that
Claim: , , is adequate. Why?
Claim: , is adequate. Why?
NC State University 20 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Normal forms
Literal = letter or negation of a letter: A, A
Clause = disjunction of literals: A
1
. . . A
n
Conjunct = conjunction of literals: A
1
. . . A
n
CNF = Conjunctive normal form
Conjunction of clauses
(A
1
. . . A
n
) . . . (B
1
. . . B
m
)
DNF = Disjunctive normal form
Disjunction of conjuncts
(A
1
. . . A
n
) . . . (B
1
. . . B
m
)
NC State University 21 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Linguistic expressiveness
Choose or change the basis connectives to improve
Consision of expression
Cardinality of expression
Complexity of expression
Clarity/comprehensibility/convenience of
expression
NC State University 22 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Validity
is valid iff every valuation makes it true
is a tautology
Taut = set of all tautologies
is nontrivial if neither nor are valid
NC State University 23 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Satisability
is satisable iff some valuation makes it true
is possibly true
is unsatisable iff no valuation makes it true
is a contradiction
is a tautology
NC State University 24 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Consistency
is consistent just in case some valuation
makes every statement in true
For nite , just in case

is satisable
is inconsistent if no valuation makes all
statements true
and are (in)consistent iff
, is (in)consistent
NC State University 25 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Logical consequence
[= means
1() = T whenever 1() = T
entails
[= means
1() = T whenever 1() = T for each
entails
Cn() is the set of consequences of
Cn() = [ [=
Taut = Cn()
NC State University 26 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Properties of consequences
Monotonic:
/
implies Cn() Cn(
/
)
Supra-tautologous: Taut Cn()
Idempotent: Cn(Cn()) = Cn()
Additive: Cn()
NC State University 27 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Completeness
A complete theory determines truth values for all
propositions
is complete iff for each p either
p Cn(), or
p Cn()
Is p, p complete?
NC State University 28 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Meaning
Models
Models = interpretations that make true
1 a model of iff 1() = T for each
/() = 1 [ .1() = T is the set of all
models of .

/
implies /(
/
) /()
NC State University 29 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Formalizing theories
So what good is logic?
Precise concepts for expressing theories
Precise concepts for critiquing theories
NC State University 30 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Formalizing theories
The process of logical formalization
Commence with initial formulation
Common sense
Expertise
Informed speculation
Wild guesses
Critique the formulation with respect to the
desired qualities
Correct the visible aws as seems t
Continue this process until convergence
NC State University 31 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Formalizing theories
The NC State Knowledge Discovery
Method
Commence to continuously correct the content
via the critique categories until convergence
Truth
Correctness
**Consistency
**Completeness
Categoricity
**Contingency
Chance
Coverage
Courageousness
Goodness
Computability
**Complexity
**Cardinality
Compromises
Convenience
Charity
Compactness
Beauty
Clarity
Comprehensibility
Cleavage
Cogency
Commonsensicality
Continuity
Perfection
Closeness
Cumulativity
Convergence
Constancy
NC State University 32 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Formalizing theories
Logical formalization as search
Different critiques might suggest incompatible
corrections; what to desire?
Applied corrections might not work
Confusion or contradiction can suggest retreat
to prior formulation; divergence
View this process as a search for the right
formulation
Process state as position in a space of assessment
dimensions
Assessment criteria as elements of heuristic
evaluation function
Correction methods as possible actions
NC State University 33 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Tableau proofs
Tableaux = tables
Labeled trees, built up from atomic tableaux
Various nice computational properties
We will consider other proof formalisms later
NC State University 34 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Atomic propositional tableaux
TA FA
T()
F
F()
T
NC State University 35 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Atomic propositional tableaux
T( )
T
T
F( )

T
d
d
T
T( )

T
d
d
T
F( )
F
F
NC State University 36 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Atomic propositional tableaux
T( )

F
d
d
T
F( )
T
F
T( )

T
d
d
F
T F
F( )

T
d
d
F
F T
NC State University 37 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Tableaux construction rules
Root is proposition under consideration
Apply atomic tableau to some proposition in tree
Append atomic tableau at end of branch beneath
Head of appended tableau duplicates proposition
being reduced
NC State University 38 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Tableau properties
Tableau , path P on , and E an entry on P
E is reduced iff all entries on the atomic tableau
with root E appear on P
P is contradictory iff both T and F appear on
P
P is nished iff it is contradictory or every entry
on P is reduced on P
is nished iff every path is nished
is contradictory iff every path is contradictory
NC State University 39 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Tableau proof
Proof by refutation
Tableau proof of = a contradictory tableau with
root F
means is tableau provable
Tableau refutation of = a contradictory tableau
with root T
is tableau refutable iff it has a tableau
refutation
NC State University 40 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Complete systematic tableaux
Construct increasing sequence of tableaux
Find highest level with unreduced noncontradictory
entry E
Find leftmost path containing such an entry
Adjoin atomic tableau with root E to each such path
Adjunction means
m

m+1
Limit (union) of this sequence is the CST
NC State University 41 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Properties of CST
Every CST is nished
If a CST is contradictory, it contains a nite
contradictory tableau
m
Thus if a CST is a proof, it is a nite tableau.
Every CST is nite
NC State University 42 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Soundness and completeness
What is the relationship between truth and proof?
Between entailment and provability?
Soundness means truth preserving
A logic is sound if p implies [= p
Completeness means proof preserving
A logic is complete if [= p implies p
Logicians often will use completeness proof to
mean a proof of both soundness and completeness
NC State University 43 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Soundness of tableau proof
Each satisfying valuation of a formula must
agree with the labels on some path through the
tableau
No valuation can agree with a contradictory path
In a proof, all paths are contradictory
NC State University 44 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Completeness of tableau proof
Each nished but noncontradictory path
provides a counterexample
Assign T to A if TA appears on the path
Assign F to A otherwise
NC State University 45 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Tableau proof from premises
Allow a set of premises for use in proofs
Add a new atomic tableau Tp for each premise p
Tp can be added to any path that does not
contradict it
NC State University 46 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Complete systematic tableaux from
premises
Assume an enumeration of the premises
Add premises sequentially to each
noncontradictory nished path
NC State University 47 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Soundness and completeness
Sound: p implies [= p
Complete: [= p implies p
NC State University 48 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Compactness
Propositional logic is a compact logic
[= p iff
/
[= p for some nite subset
/

One only needs nitely many premises to get
any particular consequence
An innite set is satisable iff every nite
subset of is satisable
NC State University 49 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Deductive closure
The deductive closure of a set of propositions
contains all the statements deducible from the set
Th() = p [ p
Soundness and completeness mean
Th() = Cn()
NC State University 50 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Deduction theorem
If is nite and

is the conjunction of these

statements, the following conditions are equivalent:
[=
[=

This shows the desired matching of truth and proof
NC State University 51 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Alternative proof systems
Proof by intimidation
Shut up, he explained.
Five-nger argument
Axiomatic proofs
Natural Deduction proofs
NC State University 52 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Axiomatic logics
Axioms
Maybe lots
Axiom schemata
( ( ))
(( ( )) (( ) ( )))
(( ) (( ) ))
Inference rules
Usually a small set
Modus ponens
p, p q q
NC State University 53 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Axiomatic proofs
Proof = sequence of statements
Each statement either
An axiom, or
A conclusion of an inference rule applied to preceding
statements
Final statement is the theorem
NC State University 54 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
Natural deduction proofs
No axioms
Lots of inference rules
Rules p correspond to axioms
Introduction and discharge of assumptions
Dependency tracking
NC State University 55 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Inference
A sample proof
In the style of Kalish and Montague
Line Statement Justication Deps.
1. A B Premise {1}
2. B C Premise {2}
3. A Hypothesis {3}
4. B MP 1,3 {1,3}
5. C MP 2,4 {1,2,3}
6. A C Discharge 3,5 {1,2}
7. A B B C -introduction {1,2}
8. (A B B C) (A C) Discharge 7,6 {}
NC State University 56 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Resolution
Language
Inference method
Proof automation
Logic programming
NC State University 57 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Language
CNF language:
Literals
Clauses
Formulas
Set notation:
Clauses as nite sets of literals
Empty clause is always false
Formulae as nite sets of clauses
Empty formula is always true
Sets mean syntactic irredundance
NC State University 58 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Linguistic models
Partial truth assignment = consistent set of
literals
Does not contain both A and A
Literals in set = what is assigned T
Complete truth assignment contains each letter
or its negation
/ [= S
Means assignment / satisies formula (set) S
For each C S, C / ,=
S (un)satisable iff there is an (no) assignment
that satises S
NC State University 59 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Prolog
Divide clauses into positive and negative literals
Interpret each clause as implication
A
1
. . . A
n
B
1
. . . B
m
B
1
. . . B
m
A
1
. . . A
n
Horn clause: at most one positive literal
Program clause: exactly one positive literal
Prolog program = set of program clauses
NC State University 60 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Prolog notation
Rule: some negative literals
Fact or unit clause: no negative literals
Goal clause: no positive literals
Rule A B
1
, . . . , B
m
A : B
1
, . . . , B
m
Fact A A :
Goal B
1
, . . . , B
m
: B
1
, . . . , B
m
Nomenclature for clause parts:
head : body
goal : subgoals
NC State University 61 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Modus Ponens in Clausal Form
Modus Ponens:
From and infer
From and infer
Cut rule generalizes Modus Ponens:
From and infer
From and infer
NC State University 62 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Resolution rule
Resolving on literal A:
Clause A C
1
Clause A C
2
Infer C
1
C
2
NC State University 63 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Resolution deduction
A resolution deduction of C from S consists of
A nite sequence C
1
, . . . , C
n
with C
n
= C
Each C
i
is either
A clause in S or
The resolvent of two preceding clauses in the
sequence
NC State University 64 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Resolution refutations
A resolution refutation of S is a resolution proof of
from S
Resolution preserves satisability
Clauses A C
1
, A C
2
Resolvent C
1
C
2
Hence refutation is sound
NC State University 65 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Resolution trees
A resolution tree deduction of C from S:
A labeled binary tree such that
The root is labeled with clause C
The leaves are labeled with the clauses of S
Each nonleaf node is labeled with resolvents of
its children
NC State University 66 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Resolution closure
The resolution closure 1(S) of a set of clauses S is
the closure of S under the operation of taking
resolutions
S 1(S)
If C
1
, C
2
1(S) and C is a resolvent of C
1
and
C
2
, then C 1(S)
There is a resolution refutation of S iff 1(S)
NC State University 67 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Semantic analysis
Formula S, literal
Literal reductions:
S() = C 1(S) [ , / C
If S is unsatisable, then so is S()
S

= C [ C S / C
Formula reduced by assuming is true
If S is unsatisable, both S

and S

must be
unsatisifable
NC State University 68 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Soundness and completeness
S is satisable iff either S

or S

is satisable
The unsatisiable sentences U are generated
by
If S, then S U
If S

U and S

U, then S U
If S is unsatisable, then 1(S)
NC State University 69 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Computational complexity
SAT = set of all satisable formulae
Is S satisable?
Resolution answer
2-SAT is linear time
SAT is NP-complete
3-SAT is NP-complete
This is good news too, not just bad;
more on this later
NC State University 70 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Restricted resolution
T-resolution: never resolve a tautology
Semantic resolution: one parent is falsied by
assignment A
Ordered resolution: order letters, always resolve
on highest-index letter possible
Support restriction: never resolve two clauses
outside support clauses
These are sound and complete, but others are not
NC State University 71 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Linear resolution
A linear resolution deduction of C from S is a
sequence of pairs C
0
, B
0
), . . . , C
n
, B
n
) such that
C = C
n
C
0
S
Each B
i
is either in S or is some preceding C
j
Each C
i +1
is a resolvent of C
i
and B
i
.
C is linearly deducible (refutable) from S if there is a
linear deduction (refutation) of C from S
NC State University 72 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Nomenclature
S = input clauses
C
0
= starting clauses
C
i
= center clauses
B
i
= side clauses
NC State University 73 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Soundness and completeness
Linear resolution is sound (by restriction)
Linear resolution is complete
NC State University 74 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Linear input resolution
Starts with goal clause
All side clauses are input clauses
Incomplete in general
Consider all clauses of two literals
Complete when all inputs are program clauses
NC State University 75 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Renements
LD-resolution = linear denite resolution
Ordered literals = denite clauses
Resolutions maintain ordering within insertions
SLD-resolution = selected linear denite
resolution
Resolutions follow syntactic ordering of literals
Prolog: always resolve on rst goal literal
Both are sound and complete
NC State University 76 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle
Propositional logic Resolution
Search and backtracking
Success and failure on resolution paths
Success = nd on path
Failure = end path with no
Search all paths until success or exhaustion
Depth-rst search, breadth-rst search, etc.
Pure backtracking DFS can fail!
Intelligent backtracking schemes
NC State University 77 / 77
CSC 503 Fall 2005
c 2005 by Jon Doyle