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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
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)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rocha, C., Meseguer, J. (2008). Theorem Proving Modulo Based on Boolean Equational Procedures. In: Berghammer, R., Möller, B., Struth, G. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2008. Lecture Notes in Computer Science, vol 4988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78913-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-78913-0_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78912-3
Online ISBN: 978-3-540-78913-0
eBook Packages: Computer ScienceComputer Science (R0)