logic library

This is an attempt at formalizing different logics and deductive systems.

Agda

Agda is a dependently typed functional language developed by Norell at the Chalmers University of Technology as his Ph.D. Thesis. It also works as an interactive proof assistant, because of the Curry-Howard correspondence.

The current library release works with Agda-2.6.2 and stdlib-1.5.

Content

Up to now, he have:

in Intuitionistic Propositional Logic:

• Formalized inference rules for the systems NJ, LJ and LJT.
• Formalized inference rules for Bi-directional Natural Deduction.
• Proved soundness and completeness properties for Bi-directional Natural Deduction.
• Proved properties of Sequent Calculus such as weakening, contraction and cut.
• Proved Natural Deduction's consistency.