The judge package

[ Tags: gpl, library, logic, program ] [ Propose Tags ]

An implementation of a decision procedure for classical logic and justification logic.


[Skip to Readme]

Properties

Versions 0.1.2.0
Change log CHANGELOG.md
Dependencies aeson (>=0.11.3.0 && <1.2.3.1), ansi-wl-pprint (>=0.6.7.3 && <0.6.8.1), attoparsec (>=0.13.1.0 && <0.13.3.0), base (>=4.7 && <5), bytestring (>=0.10.8.1 && <0.10.8.3), containers (>=0.5.7.1 && <0.5.10.3), directory (>=1.3.0.0 && <1.3.2.0), filepath (>=1.4.1.1 && <1.4.2.0), judge, mtl (==2.2.1), optparse-applicative (>=0.12.1.0 && <0.14.0.0), pointedlist (==0.6.1), terminal-size (==0.3.2.1), texmath (>=0.10.1 && <0.11.0), text (==1.2.2.2), transformers (==0.5.2.0), unordered-containers (==0.2.8.0), utf8-string (==1.0.1.1), vector (>=0.11.0.0 && <0.12.0.2), yaml (>=0.8.23 && <0.8.26) [details]
License GPL-3
Author ns@slak.ws
Maintainer ns@slak.ws
Category Logic
Home page https://github.com/slakkenhuis/judge#readme
Source repo head: git clone https://github.com/slakkenhuis/judge
Uploaded Mon Feb 5 15:16:12 UTC 2018 by slakkenhuis
Distributions NixOS:0.1.2.0
Executables judge
Downloads 25 total (25 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2018-02-05 [all 1 reports]
Hackage Matrix CI

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for judge-0.1.2.0

[back to package description]

judge

judge is a modular implementation of a decision procedure for classical and justification logics, through a tableau-based theorem prover.

Installation

After cloning the repository, the recommended installation method is through Stack:

stack install judge

Alternatively, judge can be installed through Cabal.

Usage

judge expects a logical system to be defined in the YAML or JSON format. This file will specify the type of proof system and the logical family (although at the moment, only the respective values tableau and justification are recognised). It also provides the rules of inference. See the logic directory for examples.

If no target formula(s) are provided via -g, formulas are read off the standard input. If no output file is provided via -o, the result is written to the standard output. By default, the format is plain text; add -f LaTeX to obtain LaTeX code instead.

For example, the following will construct proofs for theorems of the logic Jcs (with c:(A→B→A) ∊ CS), and produces a PDF file to visualise them:

judge logic/J.yml \
    -a "c:(A->B->A)" \
    -f LaTeX \
     < formulas.txt \
     | pdflatex

Contributing

Notable missing features are detailed on the issue tracker (export).

Contributions that extend judge to different logical families (modal, first order...) or proof systems (sequent, natural deduction...) are welcomed.