The whole site
Download everything on this site from
Github.
Predicate logic and json
The gkc prover used for proving the examples and converting formats
can be downloaded from
Github with the
AGPL v3 licence.
Instead of checking out the current development
version we recommend to download the
latest release
containing the pre-compiled no-dependencies command line
binaries for Linux, Windows, MacOS and Wasm.
Gkc uses the
WhiteDb main memory database
for internal structures.
The JSON-LD-LOGIC proposal is available
here.
Propositional logic
The propositional logic provers is a set of self-contained, no-dependencies,
easy-to-hack javascript code under the
MIT licence.
Either download everything from
from Github or as separate files:
Release 2026-07-21.
User interface for trying out all the functions:
Solvers for experimenting with different algorithms are self-contained:
- proplog_cdcl.js conflict-driven clause learning (CDCL): the algorithm
the modern high-performance solvers are built upon; together with proplog_dpll.js the best
solver among the ones provided
- proplog_dpll.js improved dpll with two watched literals and learned
variable weights; shares the best-solver spot with proplog_cdcl.js
- proplog_olddpll.js old-style dpll: no learning and full pure literal elimination
- proplog_naivedpll.js naive minimal dpll, easy to understand
- proplog_res.js optimized resolution method: better than table search, worse than dpll
- proplog_naiveres.js naive minimal resolution, easy to understand
- proplog_searchtable.js basic table search: both leaves-only and all-nodes test options
Utilities are also self-contained: