Skip to content

Equivalence of natural deduction and sequent calculus in HOL4

License

Notifications You must be signed in to change notification settings

lxndrcx/proofTheoryHOL

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Summer Project 2018/2019: Equivalences of proof theories in HOL

See HOL folder for proof source. See releases tab for pdfs of report and presentation.

Done:

  • Proof in full intuitionistic logic
  • report
  • seminar

Incomplete:

  • classical logic