A Proof Assistant inside Coq

Project information

This experimental project aims to build a proof assistant for propositional logic inside another proof assistant: Coq. The main idea is to implement natural deduction rules from the GLoIn-Lecture directly in Coq in order to have a suitable environment to prove stuff in Fitch-Style inside of Coq.

Coq

70 Commits
1 Branch
0 Tags

README
GNU General Public License v3.0 or later

Created on

March 22, 2024

Loading