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

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


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

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 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.