LoL : Lots of Logic

• This repository is my proof pool.

• My environment is WSL: Ubuntu-20.04, Windows 10.

Main Goals = 0 / 6

• Domain Theory (Complete Partial Order, Complete Lattice)

• Set Theory (Aczel Tree)

• Propositional Logic (Soundness, Completeness)

• Simply Typed Lambda Calculus (SN property)

• First-Order Logic (Soundness, Completeness)

• The Godel's Incompleteness Theorem (1st Thm)

Quick Start

eval `opam env`
coq_makefile -f _CoqProject -o Makefile
make -j4 -k

coqc -v

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 5.1.1

Thanks To

• SoonWon Moon

• Clare Jang

• Dominique Larchey-Wendling

References

1. stdlib

2. sflib

3. stdpp

4. CoqGym/goedel

5. formalmetatheory-stoughton

6. Murec_Extraction