| CARVIEW |
judge: Tableau-based theorem prover for justification logic.
An implementation of a decision procedure for classical propositional logic and justification logic.
[Skip to Readme]
Downloads
- judge-0.1.3.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
| Versions [RSS] | 0.1.2.0, 0.1.3.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.0-only |
| Author | ns@slak.ws |
| Maintainer | ns@slak.ws |
| Uploaded | by slakkenhuis at 2018-03-14T23:45:10Z |
| Category | Logic |
| Home page | https://github.com/slakkenhuis/judge#readme |
| Source repo | head: git clone https://github.com/slakkenhuis/judge |
| Distributions | |
| Executables | judge |
| Downloads | 1243 total (7 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-03-14 [all 1 reports] |
Readme for judge-0.1.3.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
judge can be installed through
Cabal:
cabal sandbox init
cabal install judge
A recommended alternative is to use Stack, for which you will need to clone the repository and do:
stack install
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 example
specifications.
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 LP (with c:(A→B→A) ∊ CS), and produces a PDF
file to visualise them:
judge LP \
-a "c:(A->B->A)" \
-f LaTeX \
< formulas.txt \
| pdflatex
Contributing
Notable missing features are detailed on the issue tracker.
Contributions that extend judge to different logical families (modal, first
order...) or proof systems (sequent, natural deduction...) are welcomed.