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]

Warnings:

The 'description' field should be longer than the 'synopsis' field. It's useful to provide an informative 'description' to allow Haskell programmers who have never heard about your package to understand the purpose of your package. The 'description' field content is typically shown by tooling (e.g. 'cabal info', Haddock, Hackage) below the 'synopsis' which serves as a headline. Please refer to <https://www.haskell.org/cabal/users-guide/developing-packages.html#package-properties> for more details.

Theorem prover for intuitionistic propositional logic using G4ip

[Skip to Readme]

Properties

Versions	0.1.0.0, 0.1.0.1, 2.0.0.0, 2.0.0.0
Change log	None available
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:55:01Z

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

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.