David Basin
Manuel Clavel
Skip Abstract Section
Abstract
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be good metalogical frameworks when their theories always have initial models and they support reflective and parameterized reasoning.We develop this thesis both abstractly and concretely. Abstractly, we formalize our proposal as a set of requirements and explain how any logic satisfying these requirements can be used for metalogical reasoning. Concretely, we present membership equational logic as a particular metalogic that satisfies these requirements. Using membership equational logic, and its realization in the Maude system, we show how reflection can be used for different, nontrivial kinds of formal metatheoretic reasoning. In particular, one can prove metatheorems that relate theories or establish properties of parameterized classes of theories.
- Abramson, H. and Rogers, M., Eds. 1989. Metaprogramming in Logic Programming. MIT Press, Cambridge, MA.]] Google Scholar
- Aczel, P. 1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, Amsterdam, The Netherlands, 739--782.]]Google Scholar
- Aitken, W. E., Constable, R. L., and Underwood, J. L. 1999. Metalogical frameworks II: Developing a reflected decision procedure. J. Automat. Reason. 22, 2(2), 171--221.]] Google Scholar
- Allen, S. F., Constable, R. L., Howe, D. J., and Aitken, W. 1990. The semantics of reflected proof. In Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA.]]Google Scholar
- Apt, K. and Turini, F., Eds. 1995. Meta-Logics and Logic Programming. Logic Programming Series. MIT Press, Cambridge, MA.]] Google Scholar
- Basin, D. and Constable, R. 1993. Metalogical frameworks. In Logical Environments, G. Huet and G. Plotkin, Eds. Cambridge University Press, Cambridge, MA, 1--29.]] Google Scholar
- Basin, D. and Matthews, S. 1998. Scoped metatheorems. In Second International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 15. Elsevier, Amsterdam, The Netherlands, 1--12.]]Google Scholar
- Basin, D. and Matthews, S. 2000. Structuring metatheory on inductive definitions. Inform. Computat. 162, 1--2 (Oct./Nov.), 80--95.]] Google Scholar
- Basin, D. and Matthews, S. 2002. Logical frameworks. In Handbook of Philosophical Logic, 2nd ed., vol. 9, D. Gabbay and F. Guenthner, Eds. Kluwer Academic Publishers, Dordrecht, The Netherlands, 89--164.]]Google Scholar
- Bouhoula, A., Jouannaud, J.-P., and Meseguer, J. 2000. Specification and proof in membership equational logic. Theoret. Comput. Sci. 236, 35--132.]] Google Scholar
- Boyer, R. S. and Moore, J. S. 1981. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. Academic Press, New York, NY, 103--185.]]Google Scholar
- Bruynooghe, M., Ed. 1990. Proceedings Second Workshop on Meta-Programming in Logic. K. U. Leuven, Leuven, Belgium.]]Google Scholar
- Clavel, M. 2000. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications, CSLI Publications, Stanford, CA.]] Google Scholar
- Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., and Quesada, J. F. 2002a. Maude: Specification and programming in rewriting logic. Theoret. Comput. Sci. 285, 2, 187--244.]] Google Scholar
- Clavel, M., Durán, F., Eker, S., and Meseguer, J. 2000a. Building equational proving tools by reflection in rewriting logic. In CAFE: An Industrial-Strength Algebraic Formal Method, K. Futatsugi, A. T. Nakagawa, and T. Tamai, Eds. Elsevier, Amsterdam, The Netherlands, 1--31.]]Google Scholar
- Clavel, M., Durán, F., Eker, S., Meseguer, J., and Stehr, M.-O. 1999. Maude as a formal meta-tool. In FM'99---Formal Methods, J. Wing and J. Woodcock, Eds. Lecture Notes in Computer Science, vol. 1709. Springer-Verlag, Berlin, Germany, 1684--1703.]] Google Scholar
- Clavel, M., Durán, F., and Martí-Oliet, N. 2000b. Polytypic programming in Maude. In Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam, The Netherlands, 339--360.]]Google Scholar
- Clavel, M., Eker, S., Lincoln, P., and Meseguer, J. 1996. Principles of Maude. In First International Workshop on Rewriting Logic and its Applications, J. Meseguer, Ed. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam, The Netherlands, 65--89.]]Google Scholar
- Clavel, M., Martí-Oliet, N., and Palomino, M. 2004. Formalizing and proving semantics relations between specifications by reflection. In Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology (AMAST'04), Stirling, UK.]]Google Scholar
- Clavel, M. and Meseguer, J. 1996. Axiomatizing reflective logics and languages. In Proceedings of Reflection'96, G. Kiczales, Ed. Xerox PARC, San Francisco, CA, 263--288.]]Google Scholar
- Clavel, M. and Meseguer, J. 2002. Reflection in conditional rewriting logic. Theoret. Comput. Sci. 285, 2, 245--288.]] Google Scholar
- Clavel, M., Meseguer, J., and Palomino, M. 2002b. Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. In Fourth International Workshop on Rewriting Logic and its Applications, F. Gadducci and U. Montanari, Eds. Electronic Notes in Theoretical Computer Science, vol. 71. Elsevier, Amsterdam, The Netherlands, 63--78.]]Google Scholar
- Cointe, P., Ed. 1999. Proceedings of Reflection'99. Lecture Notes in Computer Science, vol. 1616. Springer-Verlag, Berlin, Germany.]]Google Scholar
- Constable, R. L. 1995. Using reflection to explain and enhance type theory. In Proof and Computation, H. Schwichtenberg, Ed. Computer and System Sciences, vol. 139. Springer-Verlag, Berlin, Germany, 109--144.]]Google Scholar
- Demers, F.-N. and Malenfant, J. 1995. Reflection in logic, functional and object-oriented programming: A short comparative study. In Proceedings of IJCAI'95---Workshop on Reflection and Metalevel Architectures and their Applications in AI. 29--38.]]Google Scholar
- Despeyroux, J., Pfenning, F., and Schürmann, C. 1997. Primitive recursion for higher-order abstract syntax. In Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications (TLCA'97) (Nancy, France). Lecture Notes in Computer Science, vol. 1210. Springer-Verlag, Berlin, Germany.]] Google Scholar
- Durán, F. 1999. A reflective module algebra with applications to the Maude language. Ph.D. dissertation. University of Málaga, Málaga, Spain.]]Google Scholar
- Ehrig, H. and Mahr, B. 1985. Fundamentals of Algebraic Specification 1. EATCS Monographs on Theoretical Computer Science, vol. 6. Springer-Verlag, Berlin, Germany.]] Google Scholar
- Feferman, S. 1988. Finitary inductively presented logics. In Logic Colloquium '88. North-Holland, Amsterdam, The Netherlands, 191--220.]]Google Scholar
- Fribourg, L. and Turini, F., Eds. 1994. Logic Program Synthesis and Transformation--Meta-programming in Logic. Lecture Notes in Computer Science, vol. 883. Springer-Verlag, Berlin, Germany.]] Google Scholar
- Gardner, P. 1992. Representing logics in type theory. Ph.D. dissertation. University of Edinburgh, U.K. Also published as ECS-LFCS-92-227.]]Google Scholar
- Giunchiglia, F., Traverso, P., Cimatti, A., and Pecchiari, P. 1992. A system for multi-level reasoning. In IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency, Tokyo, Japan, 190--195.]]Google Scholar
- Goguen, J. and Burstall, R. 1984. Introducing institutions. In Logic of Programming Workshop, E. Clarke and D. Kozen, Eds. Lecture Notes in Computer Science, vol. 164. Springer-Verlag, Berlin, Germany, 221--256.]] Google Scholar
- Goguen, J. and Burstall, R. 1992. Institutions: Abstract model theory for specification and programming. J. ACM 39, 1 (Jan.), 95--146.]] Google Scholar
- Goguen, J. and Meseguer, J. 1987. Models and equality for logical programming. In Proceedings of TAPSOFT'87, H. Ehrig, G. Levi, R. Kowalski, and U. Montanari, Eds. Lecture Notes in Computer Science, vol. 250. Springer-Verlag, Berlin, Germany, 1--22.]] Google Scholar
- Gordon, M. and Melham, T. 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, U.K.]] Google Scholar
- Harper, R., Honsell, F., and Plotkin, G. 1993. A framework for defining logics. J. ACM 40, 1 (Jan.), 143--184.]] Google Scholar
- Harrison, J. 1995. Metatheory and reflection in theorem proving: a survey and critique. Tech. Rep. CRC-053, SRI Cambridge, Cambridge U.K.]]Google Scholar
- Hill, P. and Lloyd, J. 1989. Analysis of meta-programs. In Meta-Programming in Logic Programming, H. D. Abramson and M. H. Rogers, Eds. MIT Press, Cambridge, MA, 23--52.]] Google Scholar
- Hill, P. and Lloyd, J. 1994. The Gödel Programming Language. MIT Press, Cambridge, MA.]] Google Scholar
- Howe, D. J. 1988. Computational metatheory in Nuprl. In 9th International Conference on Automated Deduction (Argonne, IL). Lecture Notes in Computer Science, vol. 310. Springer-Verlag, Berlin, Germany, 238--257.]] Google Scholar
- Howe, D. J. 1990. Reflecting the semantics of reflected proof. In Proof Theory, P. Aczel, H. Simmons, and S. Wainer, Eds. Cambridge University Press, Cambridge, U.K., 229--250.]] Google Scholar
- Jeuring, J. and Jansson, P. 1996. Polytypic programming. In Proceedings of the Second International Summer School on Advanced Functional Programming Techniques, J. Launchbury, E. Meijer, and T. Sheard, Eds. Lecture Notes in Computer Science, vol. 1129. Springer-Verlag, Berlin, Germany, 68--114.]] Google Scholar
- Kiczales, G., Ed. 1996. Proceedings of Reflection'96, G. Kiczales, ed. Xerox PARC, San Francisco, CA.]]Google Scholar
- Kiczales, G., des Rivieres, J., and Bobrow, D. G. 1991. The Art of the Metaobject Protocol. MIT Press, Cambridge, MA.]] Google Scholar
- Knoblock, T. B. and Constable, R. L. 1986. Formalized metareasoning in type theory. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA., 237--248.]]Google Scholar
- Makowsky, J. A. 1984. Model theoretic issues in theoretical computer science, part I: Relational data bases and abstract data types. In Logic Colloquium '82 (Florence, Italy). North Holland, Amsterdam, The Netherlands, 303--343.]]Google Scholar
- Martí-Oliet, N. and Meseguer, J. 1994. General logics and logical frameworks. In What is a Logical System?, D. Gabbay, Ed. Oxford University Press, Oxford, U.K., 355--392.]] Google Scholar
- Martí-Oliet, N. and Meseguer, J. 2002a. Rewriting logic as a logical and semantic framework. In Handbook of Philosophical Logic, 2nd ed., D. Gabbay and F. Guenthner, Eds. Kluwer Academic Publishers, Amsterdam, The Netherlands, 1--87. First published as SRI Tech. Report SRI-CSL-93-05, August 1993.]]Google Scholar
- Martí-Oliet, N. and Meseguer, J. 2002b. Rewriting logic: Roadmap and bibliography. Theoret. Comput. Sci. 285, 121--154.]] Google Scholar
- Matthews, S. 1992. Reflection in logical systems. See Smith and Yonezawa {1992}, 178--183.]]Google Scholar
- Matthews, S., Smaill, A., and Basin, D. 1993. Experience with FS0 as a framework theory. In Logical Environments, G. Huet and G. Plotkin, Eds. Cambridge University Press, Cambridge, U.K., 61--82.]] Google Scholar
- McDowell, R. and Miller, D. 1997. A logic for reasoning with higher-order abstract syntax. In Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA., 434--445.]] Google Scholar
- Meseguer, J. 1989. General logics. In Logic Colloquium'87, H.-D. Ebbinghaus et al., Eds. North-Holland, Amsterdam, The Netherlands, 275--329.]]Google Scholar
- Meseguer, J. 1992. Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96, 1, 73--155.]] Google Scholar
- Meseguer, J. 1998a. Membership algebra as a semantic framework for equational specification. In Proceedings of WADT'97, F. Parisi-Presicce, Ed. Lecture Notes in Computer Science, vol. 1376. Springer-Verlag, Berlin, Germany, 18--61.]] Google Scholar
- Meseguer, J. 1998b. Research directions in rewriting logic. In Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29--August 6, 1997, U. Berger and H. Schwichtenberg, Eds. Springer-Verlag, Berlin, Germany.]]Google Scholar
- Paulin-Mohring, C. 1993. Inductive definitions in the system Coq---rules and properties. In Proceedings of the Conference on Typed Lambda Calculi and Applications, M. Bezem and J.-F. Groote, Eds. Lecture Notes in Computer Science, vol. 664. Springer-Verlag, Berlin, Germany. LIP Res. rep. 92--49.]] Google Scholar
- Paulson, L. C. 1994a. A fixedpoint approach to implementing (co)inductive definitions. In Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (Nancy, France). Lecture Notes in Artificial Intelligence, vol. 814. Springer-Verlag, Berlin, Germany.]] Google Scholar
- Paulson, L. C. 1994b. Isabelle : A Generic Theorem Prover; with Contributions by Tobias Nipkow. Lecture Notes in Computer Science, vol. 828. Springer, Berlin, Germany.]]Google Scholar
- Pettorossi, A., Ed. 1992. Proceedings of the Third Workshop on Meta-programming in Logic. Lecture Notes in Computer Science, vol. 649. Springer-Verlag, Berlin, Germany.]] Google Scholar
- Pfenning, F. and Schürmann, C. 1999. System description: Twelf---a meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, Berlin, Germany, 202--206.]] Google Scholar
- Ruess, H. 1995. Formal meta-programming in the calculus of constructions. Ph.D. dissertation. Universität Ulm, Ulm, Germany.]]Google Scholar
- Ruess, H. 1997. Computational reflection in the calculus of constructions and its application to theorem proving. In Proceedings for the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97) (Nancy, France), R. Hindley, Ed. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 319--335.]] Google Scholar
- Schürmann, C. 2000. Automating the meta theory of deductive systems. Ph.D. dissertation. Carnegie Mellon University, Pittsburgh, PA. Also published as CMU-CS-00-146.]]Google Scholar
- Schürmann, C. 2001. A type-theoretic approach to induction with higher-order encodings. In Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001). Lecture Notes in Computer Science, vol. 2250. Springer-Verlag, Berlin, Germany, 266--281.]] Google Scholar
- Schürmann, C. and Pfenning, F. 1998. Automated theorem proving in a simple meta-logic for LF. In Proceedings of the 15th International Conference on Automated Deduction (CADE-15) (Lindau, Germany), C. Kirchner and H. Kirchner, Eds. Lecture Notes in Computer Science, vol. 1421. Springer-Verlag, Berlin, Germany, 286--300.]] Google Scholar
- Scott, D. 1974. Completeness and axiomatizability in many-valued logic. In Proceedings of the Tarski Symposium, L. Henkin, Ed. American Mathematical Society, Providence, RI, 411--435.]]Google Scholar
- Shankar, N. 1994. Metamathematics, Machines, and Gödel's Proof. Cambridge University Press, Cambridge, U.K.]] Google Scholar
- Smith, B. and Yonezawa, A., Eds. 1992. Proc. IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency, Tokyo, Japan.]]Google Scholar
- Smith, B. C. 1984. Reflection and semantics in Lisp. In Proceedings of POPL'84. ACM Press, New York, NY, 23--35.]] Google Scholar
- Smorynski, C. 1977. The incompleteness theorems. In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, Amsterdam, The Netherlands, 821--865.]]Google Scholar
- Smullyan, R. M. 1994. Diagonalization and Self-Reference. Oxford University Press, Oxford, U.K.]]Google Scholar
- Steele, Jr., G. L. and Sussman, G. J. 1978. The art of the interpreter or, the modularity complex. Tech. Rep. AIM-453. MIT AI-Lab, Cambridge, MA.]] Google Scholar
- Stehr, M.-O. 2000. CINNI---a generic calculus of explicit substitutions and its application to λ-, ς- and π-calculi. In Third International Workshop on Rewriting Logic and its Applications, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam, The Netherlands, 71--92.]]Google Scholar
- Stehr, M.-O. and Meseguer, J. 1999. Pure type systems in rewriting logic. In Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France. Available online at http://www.cs.bell-labs.com/∼felty/LFM99/.]]Google Scholar
- Stehr, M.-O., Naumov, P., and Meseguer, J. 2000. A proof-theoretic approach to the HOL-Nuprl connection with applications to proof translation. Manuscript, SRI International, Menlo Park, CA. Available online at http://www.csl.sri.com/ stehr/fi_eng.html.]]Google Scholar
- Turchin, V. F. 1986. The concept of a supercompiler. ACM Trans. Programm. Lang. Syst. 8, 3, 292--325.]] Google Scholar
- van Emden, M. and Kowalski, R. 1976. The semantics of predicate logic as a programming language. J. ACM 23, 733--42.]] Google Scholar
- Wand, M. and Friedman, D. P. 1988. The mystery of the tower revealed. Lisp Symbol. Computat. 1, 1, 11--38.]]Google Scholar
- Weyhrauch, R. W. 1980. Prolegomena to a theory of mechanized formal reasoning. Art. Intell. 13, 133--170.]]Google Scholar
Index Terms
- Reflective metalogical frameworks
Recommendations
Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is ...
Metalogical Frameworks II: Developing a Reflected Decision Procedure
Proving theorems is a creative act demanding new combinations of ideas and on occasion new methods of argument. For this reason, theorem proving systems need to be extensible. The provers should also remain correct under extension, so there must be a ...
Operational Termination of Membership Equational Programs: the Order-Sorted Way
Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) context-sensitive rewriting. Specifically, we ...
Comments