A experimental prover written in Common Lisp, based on clause resolution and Knuth-Bendix completion algorithm.
lisp common-lisp logic theorem-proving proof-assistant logic-programming symbolic-computation prover mathematical-logic term-rewriting theorem-prover knuth-algorithm refutation-tree
-
Updated
Jun 19, 2022 - Common Lisp