Popularity
1.5
Growing
Activity
0.8
Growing
1
1
0

Monthly Downloads: 27
Programming language: Haskell
License: GNU General Public License v3.0 only
Tags: Logic    
Latest version: v0.1.3.0

judge alternatives and similar packages

Based on the "Logic" category

Do you think we are missing an alternative of judge or a related project?

Add another 'Logic' Package

README

judge

judge is a modular implementation of a decision procedure for classical and justification logics, through a tableau-based theorem prover. It is based on my Master's thesis, which is freely available at the Utrecht University Repository.

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](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](formulas.txt) of the logic [LP](logic/LP.yml) (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.