Propositional Calculus in Coq

Preprint English OPEN
van Doorn, Floris;
(2015)
  • Subject: Mathematics - Logic | Computer Science - Logic in Computer Science
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES | TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
    arxiv: Computer Science::Logic in Computer Science

I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and seq... View more
  • References (7)

    [1] Matt Bishop. Foundations of constructive analysis. 1967.

    [2] Georges Gonthier. A computer-checked proof of the four colour theorem. 2005.

    [3] Georges Gonthier. Engineering Mathematics: The Odd Order Theorem Proof. SIGPLAN Not., 48(1):1-2, January 2013.

    [4] The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2013. Version 8.4.

    [5] Russell O'Connor. Essential Incompleteness of Arithmetic Verified by Coq. 2005.

    [6] Vincent Siles and Hugo Herbelin. Pure Type System conversion is always typable. Journal of Functional Programming, 22(2):153 - 180, May 2012.

    [7] Floris van Doorn, Herman Geuvers, and Freek Wiedijk. Explicit Convertibility Proofs in Pure Type Systems. LFMTP '13, pages 25-36. ACM, 2013.

  • Metrics
Share - Bookmark