The g4ip-prover package

[ Tags: logic, mit, program ] [ Propose Tags ]

Implementation of a theorem prover for intuitionistic propositional logic using G4ip


[Skip to Readme]

Properties

Versions 0.1.0.0, 0.1.0.1
Dependencies array (>=0.5 && <1.0), base (==4.9.*), directory (>=1.0 && <2.0), system-filepath (>=0.4 && <1.0) [details]
License MIT
Author Josh Acay, Klntsky
Maintainer klntsky@gmail.com
Category Logic
Source repo head: git clone git://github.com/8084/g4ip-prover.git
Uploaded Mon Dec 4 08:09:42 UTC 2017 by klntsky
Distributions NixOS:0.1.0.1
Executables g4ip-prover
Downloads 333 total (13 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2017-12-04 [all 2 reports]
Hackage Matrix CI

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for g4ip-prover-0.1.0.1

[back to package description]

G4ip

Description

Implementation of a theorem prover for intuitionistic propositional logic using G4ip in Haskell.

Fork of cacay/G4ip.

G4ip rules

G4ip rules

Improvements over the original code

  • proof trees are now constructing explicitly
  • added proposition parser
  • added exporting of the proof tree to LaTeX

File Structure

  • G4ip/Proposition.hs -- Definition of propositions and some syntactic sugar
  • G4ip/Prover.hs -- The actual theorem prover
  • G4ip/Parser.hs -- Parser for propositions
  • G4ip/LaTeXExporter.hs -- Exporter for proofs

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.