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

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

Theorem prover for intuitionistic propositional logic using G4ip

[Skip to Readme]

Modules

[Index] [Quick Jump]

G4ipProver

Downloads

g4ip-prover-2.0.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

Candidates

0.1.0.0, 0.1.0.1, 2.0.0.0

Versions [RSS]	0.1.0.0, 0.1.0.1, 2.0.0.0
Dependencies	array (>=0.5 && <1.0), base (>=4.9 && <5), directory (>=1.0 && <2.0), filepath (>=1.4 && <2) [details]
License	MIT
Author	Josh Acay, Klntsky
Maintainer	klntsky@gmail.com
Category	Logic
Home page	https://github.com/8084/g4ip-prover
Source repo	head: git clone git://github.com/8084/g4ip-prover.git
Uploaded	by klntsky at 2018-12-28T21:57:51Z
Distributions	NixOS:2.0.0.0
Reverse Dependencies	1 direct, 0 indirect [details]
Executables	g4ip-prover
Downloads	2076 total (14 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs available [build log] Last success reported on 2018-12-28 [all 1 reports]

Readme for g4ip-prover-2.0.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

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.