Theorem proving modulo based on boolean equational procedures

Camilo Rocha, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationRelations 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
PublisherSpringer
Pages337-351
Number of pages15
ISBN (Print)354078912X, 9783540789123
DOIs
StatePublished - 2008
Event10th International Conference on Relational Methods in Computer Science and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008 - Frauenworth, Germany
Duration: Apr 7 2008Apr 11 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4988 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other10th International Conference on Relational Methods in Computer Science and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008
Country/TerritoryGermany
CityFrauenworth
Period4/7/084/11/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Theorem proving modulo based on boolean equational procedures'. Together they form a unique fingerprint.

Cite this