priitj/logictools

Simple algorithms for converting and solving propositional formulas: easy to hack and experiment with.

logictools

We help to study logic solvers by providing and collecting various easy-to-use, browser-based javascript tools: starting with classical propositional formulas and continuing with predicate logic later.

All the code is self-contained, no-dependencies, easy-to-hack javascript under the MIT licence.

The focus is on simplicity, ease of use, hacking and experimenting, not state of the art efficiency-wise.

Help and cooperation appreciated for improving the current code, writing and proposing new tools, etc. See the site with functioning code.

Site, initial solvers and utilities written by Tanel Tammet (tanel.tammet at gmail.com)

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