judge alternatives and similar packages
Based on the "Logic" category.
Alternatively, view judge alternatives based on common mentions on social networks and blogs.

tamarinprover
Main source code repository of the Tamarin prover for security protocol verification. 
structuralinduction
SII: Structural Induction Instantiator over any strictlypositive algebraic data type. 
haskholcore
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
InfluxDB  Power RealTime Data Analytics at Scale
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of judge or a related project?
README
judge
judge
is a modular implementation of a decision procedure for classical and
justification logics, through a tableaubased 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.