Download options

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 2020-08-31.

User interface for trying out all the functions:

proplog.html a barebones webpage without menus, design, bootstrap or jquery
proplog_ui.js calling the algorithms below

Solvers for experimenting with different algorithms are self-contained:

proplog_dpll.js the best solver among the ones provided
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:

proplog_parse.js parse formula and dimacs syntaxes
proplog_convert.js convert to cnf, rename variables, print formulas, build and print the full truth table
proplog_generate.js problem generators