CIS 301:
Logical Foundations
of Programming
Module: Natural Deduction
Lecture: Propositional Logic Proof Checker
Copyright 2014, Dave Schmidt, John Hatcliff, Torben Amtoft. The syllabus and all lectures for this course are copyrighted
materials and may not be used in other course settings outside of Kansas State University in their current form or modified
form without the express written permission of one of the copyright holders. During this course, students are prohibited
from selling notes to or being paid for taking notes by any person or commercial firm without the express written
permission of one of the copyright holders.
CIS 301 --- Nat Ded - Prop Logic Proofs
Objectives
 
 
Understand the main modes of use for
our Natural Deduction Proof Checker for
propositional logic
Understand the correspondence between
 
 
proof rules and proof steps
hand-written proofs and proofs in the Proof
Checker
CIS 301 --- Nat Ded - Prop Logic Proofs
Outline
 
 
 
 
 
Sequents
Proof rules and hand-written proofs
Hand-written proofs and proofs in the
Natural Deduction Proof Checker
Proof contexts, assumptions, and proof
boxes
Other tool options
CIS 301 --- Nat Ded - Prop Logic Proofs
Sequents
Sequents are a notation for stating the goal of the proof along with
premises that can be used in a proof of the goal
“P0, P1, ..., Pm entail Q”
P0, P1, ..., Pm |− Q
Premises
CIS 301 --- Nat Ded - Prop Logic Proofs
Goal, Consequent
Sequents
Sequents are a notation for stating the goal of the proof along with
premises that can be used in a proof of the goal
(P ^ Q) -> R, P --> Q, P |- R
Premises
CIS 301 --- Nat Ded - Prop Logic Proofs
Goal, Consequent
Proofs
Natural deduction proofs apply proof rules to prove the goal of the sequent
(the last line in the proof). Propositions of the left side the sequent can be
used as premises in the proof.
(P ^ Q) -> R, P --> Q, P |- R
1.
2.
3.
4.
5.
6.
(p ^ q) -> r
p
p -> q
q
p ^ q
r
CIS 301 --- Nat Ded - Prop Logic Proofs
premise
premise
premise
->e 3,2
^i 2,4
->e 1,5
Proof Rules in Proofs
We usually present proof rules (aka deduction rules, inference rules) in a “stacked” notation with
propositions that have already been deduced on top of line and the proposition that can be
deduced under the line. When we use the rule in proofs (in unstacked form), we use line
numbers to make the correspondence with propositions that have already been deduced.
(P ^ Q) -> R, P --> Q, P |- R
1.
2.
3.
4.
5.
6.
(p ^ q) -> r
p
p -> q
q
p ^ q
r
CIS 301 --- Nat Ded - Prop Logic Proofs
premise
premise
premise
->e 3,2
^i 2,4
->e 1,5
^i
P
Q
P ^ Q
Tool View
The Natural Deduction Proof Checker has window sections (columns) to
organize the main elements of natural deduction proofs.
Line Numbers
Line Numbers
Representing
“arguments” (inputs)
for Proof Rules
Propositions
Deduced
Proof Rule
Names
CIS 301 --- Nat Ded - Prop Logic Proofs
Representing Sub-Proofs
Some proof rules such as ->I and vE require “sub-proofs”. When we hand-write
proofs with sub-proofs, we often indicate the sub-proofs using indentation.
1. p
2. (q ^ p) -> r
... 3. q
... 4. q ^ p
... 5. r
6. q -> r
CIS 301 --- Nat Ded - Prop Logic Proofs
premise
premise
assumption
^i 3,1
->e 2,4
Sub-Proof
->i 3-5
Representing Sub-Proofs
Some proof rules such as ->I and vE require “sub-proofs”. When we hand-write
proofs with sub-proofs, we often indicate the sub-proofs using indentation.
P v Q,
1. P v
2. S
... 3.
... 4.
... 5.
S
|- (P ^ S) v (Q ^ S)
Q
P
P ^ S
(P ^ S) v (Q ^ S)
premise
premise
assumption
^i 3,2
vi 1,4
... 6. Q
... 7. Q ^ S
... 8. (P ^ S) v (Q ^ S)
assumption
^i 6,2
vi 2,7
9.
ve 1, 3-5, 6-8
(P ^ S) v (Q ^ S)
CIS 301 --- Nat Ded - Prop Logic Proofs
Representing Sub-Proofs
Some proof rules such as ->I and vE require “sub-proofs”. When we hand-write
proofs with sub-proofs, we often indicate the sub-proofs using indentation.
p --> r,
q --> r
|-
(p v q) --> r
1. p --> r
2. q --> r
... 3. p v q
premise
premise
assumption
... ... 4. p
... ... 5. r
assumption
->e 1,4
... ... 6. q
... ... 7. r
assumption
->e 2,6
... 8. r
9. (p v q) --> r
ve 3,4-5,6-7
->i 3-8
CIS 301 --- Nat Ded - Prop Logic Proofs
Other Features
The Natural Deduction Proof Checker tool has other useful features that you
will use in your homework and class exercises
 
 
 
Exporting
Saving proof
Generating LaTeX descriptions
CIS 301 --- Nat Ded - Prop Logic Proofs
Acknowledgements
 
The material in this lecture is based on Chapter 5 from…
 
 
Programming Logic, Dr. David A. Schmidt
The Natural Deduction Proof Checker tool was designed
and built by Brian Mulanda and Dr. Rod Howell
CIS 301 --- Nat Ded - Prop Logic Proofs

Universität des Saarlandes