Publication:
Theorem Proving Modulo Based on Boolean Equational Procedures

Thumbnail Image
Files

Files

Theorem Proving Modulo Based on Boolean Equational Procedures.pdf (781.12 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Rocha, Camilo
Meseguer, José
Abstract (Spanish)
Deducción con reglas de inferencia Las reglas de cálculo del módulo juegan un papel importante en la deducción automatizada como un método eficaz para escalar. Presentamos cuatro teorías ecuacionales que son isomorfas a la teoría booleana tradicional y mostramos que cada una de ellas da lugar a un procedimiento de decisión booleano basado en un sistema canónico de reescritura módulo asociatividad y conmutatividad. Luego, presentamos dos extensiones modulares de nuestro procedimiento de decisión para la lógica proposicional de Dijkstra-Scholten al Cálculo Secuente para Lógica de Primer Orden ya la Lógica Silogística con Complementos de L. Moss. Estas extensiones toman la forma de teorías de reescritura que son sólidas y completas para realizar la deducción módulo de sus partes ecuacionales y exhiben buenas propiedades de mecanización. Ilustramos la utilidad práctica de este enfoque mediante una implementación directa de una de estas teorías en Maude, reescribiendo el lenguaje lógico y demostrando automáticamente un punto de referencia de desafío en la demostración de teoremas.
Abstract (English)
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.
Extent
15 páginas.
Rights

© Springer-Verlag Berlin Heidelberg 2008

URI: https://repositorio.escuelaing.edu.co/handle/001/1912
Collections

Collections

AD - CTG – Informática
References

Backhouse, R.: Program Construction: Calculating Implementations from Specifications. Willey, Chichester, UK (2003)

Barendregt, H.P., Barendsen, E.: Autarkic computations and formal proofs. Journal of Automated Reasoning 28(3), 321–336 (2002)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

de Recherche en, L.: Informatique. The CiME System (2007), http://cime.lri.fr/

Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, ch. 6, vol. B, pp. 243–320. North-Holland, Amsterdam (1990)

Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)q

Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning 31(1), 33–72 (2003)

Eker, S., Martí-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. In: Martí-Oliet, N. (ed.) Proc. Strategies 2006, ENTCS, pp. 417–441. Elsevier, Amsterdam (2007)

Girard, J.-Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)

Gries, D.: A calculational proof of Andrews’s challenge. Technical Report TR96-1602, Cornell University, Computer Science (August 28, 1996)

Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. In: Texts and Monographs in Computer Science, Springer, Heidelberg (1993)

Gries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett. 53(3), 145–152 (1995)

Hendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Technical Report UIUCDCS-R-2005-2635, University of Illinois Urbana-Champaign (2005)

Hsiang, J.: Topics in automated theorem proving and program generation. PhD thesis, University of Illinois at Urbana-Champaign (1982)

Jacobson, N.: Basic algebra, vol. I. W. H. Freeman and Co., San Francisco, Calif (1974)

Lifschitz, V.: On calculational proofs. Ann. Pure Appl. Logic 113(1-3), 207–224 (2001)

Łukasiewicz, J.: Aristotle’s Syllogistic, From the Standpoint of Modern Formal Logic. Oxford University Press, Oxford (1951)

Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd. edn., pp. 1–87. Kluwer Academic Publishers, 2002. First published as SRI Tech. Report SRI-CSL-93-05 (August 1993)

Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20(1–2), 123–160 (2007)

Moss, L.S.: Syllogistic logic with complements (Draft 2007)

Rocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical Report 2007-2818, University of Illinois at Urbana-Champaign (2007)

Rocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements. Revista Colombiana de Computación 8(2) (2007)

Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. Technical Report 2007-2922, University of Illinois at Urbana-Champaign (2007)

Simmons, G.F.: Introduction to topology and modern analysis. McGraw-Hill Book Co., Inc, New York (1963)

Socher-Ambrosius, R., Johann, P.: Deduction Systems. Springer, Berlin (1997)

Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 334–375. Springer, Heidelberg (2004)

Viry, P.: Adventures in sequent calculus modulo equations. Electr. Notes Theor. Comput. Sci. 15 (1998)

Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)