GitHub - colin-mcd/SequentCalculus: Implementation of the Cut-Elimination Theorem for PK

Currently, this repo just stores an implementation of the cut-elimination theorem for Buss' version of PK.

To build:

make

Then to run the program:

cat sample_proof.txt | ./CutElim.exe | tex/tex2pdf.sh

And it will write a nice LaTeX proof in cut-free-proof.tex.

Name		Name	Last commit message	Last commit date
Latest commit History 42 Commits
tex		tex
CutElim.agda		CutElim.agda
CutElim.agda-lib		CutElim.agda-lib
CutElim.hs		CutElim.hs
Helpers.agda		Helpers.agda
Helpers.hs		Helpers.hs
Main.hs		Main.hs
Makefile		Makefile
Parse.hs		Parse.hs
Proofs.agda		Proofs.agda
README.md		README.md
Show.hs		Show.hs
Types.agda		Types.agda
Types.hs		Types.hs
_config.yml		_config.yml
index.html		index.html
lib.agda		lib.agda
sample_proof.pdf		sample_proof.pdf
sample_proof.txt		sample_proof.txt

Provide feedback