A Natural Deduction Theorem Prover for Large-scale Expert Systems (treesolve)

Abstract

In this paper we introduce an algorithm that generates human-readable natural deduction proofs for propositional logic, by reducing the problem of determining if there exists such a proof of some bounded length to an instance of SAT. Specifically, the algorithm takes as input a set of sentences $\Gamma$, a target sentence $\phi$, and three parameters $p$, $s$, $m$. It then generates a SAT instance that is satisfiable if and only if there exists a natural deduction proof of $\phi$ from $\Gamma$ of length at most $p$, where at most $m$ undischarged assumptions appear at once within any sub-proof, and where the total length of all sentences that appear in the proof do not exceed $s$. A satisfying assignment to this SAT instance can then be translated into a natural deduction proof. The number of variables in the resulting SAT instance grows as $O(p^2m^2 + s^2 + psm)$, and the number of constraints grows as $O(p\cdot(p+s)^3 + p^2m^2)$. We show that this approach can find medium-sized proofs in a practical amount of time (e.g., 100 seconds for a 40-line proof). This is slower than specialised model-search engines applied to the same problem, but our algorithm has the notable benefit of producing proofs that are human-readable. Moreover, our algorithm is highly configurable, and can easily be adapted for classical logic, intuitionistic logic, and modal logic, etc.