judge alternatives and similar packages
Based on the "Logic" category.
Alternatively, view judge alternatives based on common mentions on social networks and blogs.
tamarin-prover9.8 0.0 judge VS tamarin-proverMain source code repository of the Tamarin prover for security protocol verification.
smcdel7.9 0.0 judge VS smcdelA symbolic model checker for Dynamic Epistemic Logic.
hatt7.7 0.0 judge VS hattTruth-table generator for classical propositional logic
tip-haskell-frontend7.5 0.0 judge VS tip-haskell-frontendConvert from Haskell to Tip
picosat6.9 0.0 L2 judge VS picosatHaskell bindings for PicoSAT solver
picologic6.7 0.0 judge VS picologicSymbolic logic expressions
atp-haskell6.6 0.0 judge VS atp-haskellHaskell version of the code from "Handbook of Practical Logic and Automated Reasoning"
jukebox6.5 0.0 judge VS jukeboxA theorem prover
hout6.3 0.0 judge VS houtA non-interactive proof assistant using the Haskell type system
Heyting Algebras5.8 0.0 judge VS Heyting AlgebrasHeyting Algebras in Haskell
logic-classes5.7 0.0 judge VS logic-classesFramework for propositional and first order logic, theorem proving
Folly5.6 0.0 judge VS FollyFirst order logic in Haskell
obdd5.4 0.0 judge VS obddpure Haskell implementation of reduced ordered binary decision diagrams
structural-induction3.9 0.0 judge VS structural-inductionSII: Structural Induction Instantiator over any strictly-positive algebraic data type.
qed3.9 0.0 judge VS qedExperiments writing a prover
g4ip-prover3.4 0.0 judge VS g4ip-proverTheorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip
tpdb3.0 0.0 judge VS tpdbparser and prettyprinter for TPDB syntax (termination problem data base)
satchmo3.0 0.0 judge VS satchmoSAT encoder
g4ip2.1 0.0 judge VS g4ipA theorem prover using G4ip
minisat2.1 0.0 judge VS minisatMinisat Haskell bundle
haskhol-core0.8 0.0 judge VS haskhol-coreThe core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
Access the most powerful time series database as a service
* 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?
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
judge can be installed through
cabal sandbox init cabal install judge
A recommended alternative is to use Stack, for which you will need to clone the repository and do:
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
justification are recognised). It also provides the
rules of inference. See the [logic](logic) directory for example
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
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
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.