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]

Implementation of a theorem prover for intuitionistic propositional logic using G4ip


[Skip to ReadMe]

Properties

Versions0.1.0.0, 0.1.0.1, 0.1.0.1
Change logNone available
Dependenciesarray (>=0.5 && <1.0), base (==4.9.*), directory (>=1.0 && <2.0), system-filepath (>=0.4 && <1.0) [details]
LicenseMIT
AuthorJosh Acay, Klntsky
Maintainerklntsky@gmail.com
CategoryLogic
Source repositoryhead: git clone git://github.com/8084/g4ip-prover.git
Executablesg4ip-prover
UploadedMon Dec 4 08:03:48 UTC 2017 by klntsky

Downloads

Maintainers' 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

File Structure

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.