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

Logicians are weird

• Logical meaning ≠ English (etc.) meaning

• “If 1=2, then I’m the Man in the Moon.”

• “She is either a lawyer or a professor.”

• “I’ve won every World Cup game I’ve 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

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

\begin{matrix}α & (¬α) \\ T & F \\ F & T \end{matrix}

NC State University

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

11 / 77

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

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

12 / 77

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

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

13 / 77

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

Truth valuations

• Truth assignment A : L → {T , F}

• Truth valuation V : L(L) → {T , F}

• Required to respect truth tables in every connective

• Valuations must agree on a proposition whenever they agree on the proposition’s support

NC State University

16 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

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 T ’s

• 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 ∧, ∨, ¬ • Define 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

• Satisfiability

• Provability

NC State University

19 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

Adequacy

What can one say with a specific 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

Satisfiability

• α is satisfiable iff some valuation makes it true • α is possibly true

• α is unsatisfiable 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

Consistency

• Σ is consistent just in case some valuation makes every statement in Σ true

• For finite Σ, just in case ⋀ Σ is satisfiable

• Σ 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

Logical consequence

• α ⊧ β means

• V(β) = T whenever V(α) = T

• α entails β

• Σ ⊧ β means

• V(β) = T whenever V(α) = 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

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 • V a model of Σ iff V(α) = T for each α ∈ Σ

• M(Σ) = {V | ∀α ∈ Σ.V(α) = T } is the set of all models of Σ.

• Σ ⊆ Σ′ implies M(Σ′) ⊆ M(Σ)

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 flaws as seems fit

• Continue this process until convergence

NC State University

31 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

The N“C” 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

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  \begin{matrix}T (¬α) \\ Fα \end{matrix}  \begin{matrix}F(¬α) \\ T α \end{matrix}

NC State University

35 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

Atomic propositional tableaux

[figure: \begin{matrix}T (α ∧ β) \\ T α \\ T β \end{matrix}; F(α ∧ β); T α; T β; T (α ∨ β); T α; T β; \begin{matrix}F(α ∨ β) \\ Fα \\ Fβ \end{matrix}]

NC State University

36 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

Atomic propositional tableaux

[figure: T (α → β); Fα; T β; \begin{matrix}F(α → β) \\ T α \\ Fβ \end{matrix}; T (α ↔ β); T α; Fα; T β; Fβ; F(α ↔ β); T α; Fα; Fβ; T β]

NC State University

37 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

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 finished iff it is contradictory or every entry on P is reduced on P

• τ is finished iff every path is finished

• τ 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

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 finished

• If a CST is contradictory, it contains a finite contradictory tableau τ_{m}

• Thus if a CST is a proof, it is a finite tableau.

• Every CST is finite

NC State University

42 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

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

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

Completeness of tableau proof

• Each finished 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 finished 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 finite subset Σ′ ⊆ Σ • One only needs finitely many premises to get

any particular consequence

• An infinite set Σ is satisfiable iff every finite subset of Σ is satisfiable

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 finite 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-finger” argument

• Axiomatic proofs

• Natural Deduction proofs

NC State University

52 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

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

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  Justification 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 finite sets of literals

• Empty clause □ is always false

• Formulae as finite 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

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

• A ⊧ S

• Means assignment A satisifies formula (set) S • For each C ∈ S, C ∩ A ≠ ∅

• S (un)satisfiable iff there is an (no) assignment that satisfies 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

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

Resolution deduction

A resolution deduction of C from S consists of • A finite 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

Resolution refutations

A resolution refutation of S is a resolution proof of □ from S

• Resolution preserves satisfiability

• 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

Resolution closure

The resolution closure R(S) of a set of clauses S is the closure of S under the operation of taking resolutions

• S ⊆ R(S)

• If C_{1}, C_{2} ∈ R(S) and C is a resolvent of C_{1} and C_{2}, then C ∈ R(S)

There is a resolution refutation of S iff □ ∈ R(S)

NC State University

67 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

Semantic analysis

Formula S, literal ℓ

• Literal reductions:

S(ℓ) = {C ∈ R(S) | ℓ, ¬ℓ ∉ C}

• If S is unsatisfiable, then so is S(ℓ)

• S^{ℓ} = {C − {ℓ} | C ∈ S ∧ ℓ ∉ C}

• Formula reduced by assuming ℓ is true

• If S is unsatisfiable, both S^{ℓ} and S^{¬ℓ} must be unsatisifable

NC State University

68 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

Soundness and completeness

• S is satisfiable iff either S^{ℓ} or S^{¬ℓ} is satisfiable • The unsatisifiable sentences U are generated

by

• If □ ∈ S, then S ∈ U

• If S^{ℓ} ∈ U and S^{¬ℓ} ∈ U, then S ∈ U

• If S is unsatisfiable, then □ ∈ R(S)

NC State University

69 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle

Propositional logic  Resolution

Computational complexity

SAT = set of all satisfiable formulae

Is S satisfiable?

• 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 falsified 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

Refinements

• LD-resolution = linear definite resolution

• Ordered literals = definite clauses

• Resolutions maintain ordering within insertions

• SLD-resolution = selected linear definite

resolution

• Resolutions follow syntactic ordering of literals • Prolog: always resolve on first 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 = find □ on path • Failure = end path with no □

• Search all paths until success or exhaustion

• Depth-first search, breadth-first search, etc.

• Pure backtracking DFS can fail!

• “Intelligent” backtracking schemes

NC State University

77 / 77

CSC 503 Fall 2005 ◯^{c} 2005 by Jon Doyle