Five Isomorphic Boolean Theories and Four Equational Decision Procedures
Camilo Rocha, José Meseguer · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2007
We present four equational theories that are isomorphic to the traditional Boolean theory and show that each one of them gives rise to a canonical rewrite system modulo associativity, thus providing four decision procedures for propositional logic. The four theories come in two pairs of isomorphic dual theories. The first pair corresponds to J. Hsiang's rewrite system for the theory of Boolean rings, and to a rewrite system we propose for Dijkstra-Scholten propositional logic. The second pair uses the same Boolean operators as the previous pair but in a ``twisted'' fashion. These procedures, when run on a high performance rewrite engine, are quite efficient, but can be further sped up by the use of **optimizing equations** that perform obvious simplifications in the input expression before a decision procedure is invoked. Based on their Maude implementation, we present experimental results comparing the performance of the different procedures, and showing that they outperform a DPLL(T)-based SAT-solver.