Popularity
3.6
Declining
Activity
0.0
Stable
7
3
0
Monthly Downloads: 7
Programming language: Haskell
License: MIT License
Latest version: v2.0.0.0
Add another 'g4ip' Package
Popular Comparisons
README
G4ip
Description
Implementation of a theorem prover for intuitionistic propositional logic using G4ip in Haskell.
Fork of cacay/G4ip.
G4ip rules
[G4ip rules](g4ip.png)
Improvements over the original code
- proof trees are now constructing explicitly
- added proposition parser
- added exporting of the proof tree to LaTeX
File Structure
- G4ipProver/Proposition.hs -- Definition of propositions and some syntactic sugar
- G4ipProver/Prover.hs -- The actual theorem prover
- G4ipProver/Parser.hs -- Parser for propositions
- G4ipProver/LaTeXExporter.hs -- Exporter for proofs
- G4ipProver.hs -- Re-exports the above modules
- Main.hs -- g4ip-prover binary
Running
Use stack: stack exec g4ip-prover
Usage
g4ip-prover [OPTIONS] PROPOSITION
g4ip-prover [OPTIONS]
If the proposition was not specified, the user will be prompted to enter it interactively.
Options
--proof-header <file> Template header file for proof.
Default value: static/proof-header.txt
--proof-footer <file> Template footer file for proof.
Default value: static/proof-footer.txt
--context-header <file> Template header file for context.
Default value: static/context-header.txt
--context-footer <file> Template footer file for context.
Default value: static/context-footer.txt
--proof-file <file> Proof file name. If the file exists, it will be overwritten.
Default value: output/proof.tex
--context-file <file> Context file name. If the file exists, it will be overwritten.
Default value: output/context.tex
Proposition syntax
Variables must consist of lower-case english characters and numbers.
Propositional connectives (with precedence level):
~ , - - negation, 1
/\, & - conjunction, 2
\/, | - disjunction, 3
->, => - implication, 4
<-, <= - implication, 4
<->, <=> - equivalency, 5
Logical constants:
T - True
F - False
Converting to PDF
Use bussproofs and pdflatex.