Files in this item



application/pdfFive Isomorphic ... al Decision Procedures.pdf (658kB)
(no description provided)PDF


Title:Five Isomorphic Boolean Theories and Four Equational Decision Procedures
Author(s):Rocha, Camilo; Meseguer, José
Subject(s):computer science
Abstract: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.
Issue Date:2007-02
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2007-2818
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-21

This item appears in the following Collection(s)

Item Statistics