CS262 Logic and Verification Lecture 8: Natural deduction
CS262 Logic and Verification 1 / 12
Introduction
Copyright By PowCoder代写 加微信 powcoder
Two proof systems we have seen so far: semantic tableau and resolution
Both are well-suited for automation and computer implementation (will implement a resolution prover as a coursework assignment)
This week we will look at another proof system: natural deduction
CS262 Logic and Verification 2 / 12
Natural deduction
Formalizes the kind of reasoning people do in informal arguments
Unlike tableau and resolution, natural deduction not well-suited for computer automation
Unlike the first two, natural deduction is not based on any normal form expansion (CNF or DNF)
Central notion: nested subordinate proofs (=‘lemmas’), in which we derive conclusions from certain assumptions, and then discharge the assumptions to produce assumption-free results
CS262 Logic and Verification 3 / 12
Typical rules
Implication rule: If one can derive Y from X as an assumption, then one can discharge the assumption and conclude that X → Y holds unconditionally
Subordinate proofs/lemmas are contained in boxes The first formula X in a box is an assumption
We can assume anything, but the question is whether the assumptions help in making useful conclusions
CS262 Logic and Verification
Typical rules
rule: From X and X → Y we can conclude Y X
A formula is called active at some stage if it does not occur in a closed box We may only use active formulas at any stage
Rules are paired, one for introducing → and one for eliminating →
CS262 Logic and Verification 5 / 12
Natural deduction proof of (p → (q → r)) → (q → (p → r))
CS262 Logic and Verification 6 / 12
Constant rules:
Negation rules:
Primary connective rules:
αE α α αI α1 α2
βE ¬β1 ¬β2 βI ββ
CS262 Logic and Verification 7 / 12
Primary connective rules come in two flavors: Introduction + Elimination Last two negation rules embody the principle of proof by contradiction Second constant rule has no premises
Order of premises does not matter, but all premises must be active
CS262 Logic and Verification 8 / 12
Derived rules
A rule is derived if it does not strengthen the proof system
Any occurence of the rule can be translated away using the ‘official’ rules
Double negation Copy rule
Implication
Modus ponens
Modus tollens
X→Y Excluded middle
CS262 Logic and Verification
Proof strategies
Think backwards: What rules could be applied in the last step, and based on that come up with assumptions that should be made to apply those rules.
In proving X, assume ¬X and produce ⊥, then use negation rule This needs a lot of practice and experience
Example: Prove p → (q → p)
CS262 Logic and Verification
Proving consequences
Want to prove propositional consequences S |= X
S-introduction rule for natural deduction: At any stage, any member
of S may be used as a line.
W.l.o.g., we may introduce them as the initial lines of the proof (recall
copy rule). These formulas are sometimes called premises (no boxes!). We write S ⊢d X if there is a natural deduction derivation of X from S Example: Prove{p→q,q→r}⊢d p→r
CS262 Logic and Verification
Soundness and completeness Theorem (Soundness and completeness)
WehaveS|=X ifandonlyifS⊢d X. Proof omitted here
CS262 Logic and Verification 12 / 12
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com