Theorem Proving Modulo Based on Boolean Equational Procedures

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.

• Autores: Rocha, Camilo; Meseguer, José
• Tipo de recurso: http://purl.org/coar/resource_type/c_f744
• Fecha de publicación: 2008
• Institución: Escuela Colombiana de Ingeniería Julio Garavito
• Repositorio: Repositorio Institucional ECI
• Idioma: eng
• OAI Identifier: oai:repositorio.escuelaing.edu.co:001/1912
• Acceso en línea: https://repositorio.escuelaing.edu.co/handle/001/1912
• Palabra clave: Procedimiento de decisión; Lógica proposicional; Prueba del teorema; Teoría Ecuacional; Cálculo Secuencial; Decision Procedure; Propositional Logic; Theorem Prove; Equational Theory; Sequent Calculus
• Rights: closedAccess
• License: © Springer-Verlag Berlin Heidelberg 2008