Files in this item



application/pdfTheorem Proving ... Equational Procedures.pdf (411kB)
(no description provided)PDF


Title:Theorem Proving Modula Based on Boolean Equational Procedures
Author(s):Rocha, Camilo; Meseguer, José
Subject(s):computer science
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 the Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.
Issue Date:2007-12
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2007-2922
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-22

This item appears in the following Collection(s)

Item Statistics