Five Isomorphic Boolean Theories and Four Equational Decision Procedures

Rocha, Camilo; Meseguer, José

Permalink

https://hdl.handle.net/2142/11295 Copy

Description

Title

Five Isomorphic Boolean Theories and Four Equational Decision Procedures

Author(s)

• Rocha, Camilo
• Meseguer, José

Issue Date

2007-02

Keyword(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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11295

Copyright and License 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).

Owning Collections