CSI5110 Term Project
Made by Zhiheng Yi (7475788)
Email:zyi093@uottawa.ca

Logical Connectives in this program:

• Conjunction: &
• Disjunction: v
• Not: ~
• Implication: =>

This proof assistant implements 11 basic natural deduction rules from the text book, which are shown on the right panel.

Rules patterns:

• And Intro (&I) : p, q |- q & q
• And Elim 1 (&E1) : p & q |- p
• And Elim 2 (&E2) : p & q |- q
• Or Intro 1 (vI1) : p |- p v q
• Or Intro 2 (vI2) : p |- q v p
• Or Elim (vE) : p v q, p => a, q => a |- a
• Implication Intro (=>I) : (p |- q) |- p => q
• Implication Elim (=>E) : p, p => q |- q
• Not Intro (~I) : p => (q & ~q) |- ~p
• Double Not Intro (~~I) : p |- ~~p
• Double Not Elim (~~E) : ~~p |- p