g4ip-prover: Theorem prover for intuitionistic propositional logic using G4ip

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Implementation of a theorem prover for intuitionistic propositional logic using G4ip

[Skip to Readme]

Properties

Versions	0.1.0.0, 0.1.0.0, 0.1.0.1, 2.0.0.0
Change log	None available
Dependencies	array (>=0.5 && <1.0), base (>=4.9 && <4.10) [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	by klntsky at 2017-09-14T22:26:09Z

Downloads

g4ip-prover-0.1.0.0.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

klntsky

For package maintainers and hackage trustees

edit package information

Readme for g4ip-prover-0.1.0.0

[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

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 are lower-case english words or characters.
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.