Pages
FB
Links
Music
MTG
Blogaden
About
Contact
Terminus
MBOLIntro
- Intro
- Syntax
- HTML usage
- Latex usage
I'm attending the course "Logic in Computer Science". For that we have to make proofs using natural deduction. I like doing those kind of proofs, some of them requires some creativity and fun thinking. However I have found it very nice to have some proof assistance - these proofs are quite formal. I have been using Coq for some time now. I like Coq, but since I'm a DIKU student we have to use BoxProver. To be honest I'm gaining a liking for BoxProver over Coq for the main reason that BoxProver is straight ahead proving where as Coq is sort of starting backwards. Not to mention BoxProver is made by a friend of mine. However, I have started an exercise solutions-page on this here website, and on that I would like to paste in proofs in BoxProver syntax and then print some sort of HTML-formatted result. Therefore I have made a parser for BoxProver that transform BoxProver code into either HTML markup or Latex markup. The last to be used with the latex boxproof plugin.
