TY - GEN
T1 - Theorem proving modulo based on boolean equational procedures
AU - Rocha, Camilo
AU - Meseguer, José
N1 - Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.
PY - 2008
Y1 - 2008
N2 - Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.
AB - Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.
UR - http://www.scopus.com/inward/record.url?scp=70349326217&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349326217&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-78913-0_25
DO - 10.1007/978-3-540-78913-0_25
M3 - Conference contribution
AN - SCOPUS:70349326217
SN - 354078912X
SN - 9783540789123
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 337
EP - 351
BT - Relations and Kleene Algebra in Computer Science - 10th Int. Conference on Relational Methods in Comput. Sci. and 5th Int. Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008, Proceedings
PB - Springer
T2 - 10th International Conference on Relational Methods in Computer Science and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008
Y2 - 7 April 2008 through 11 April 2008
ER -