article

Reflective metalogical frameworks

Authors:

José MeseguerAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 5, Issue 3

Pages 528 - 576

https://doi.org/10.1145/1013560.1013566

Published: 01 July 2004 Publication History

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.

References

[1]

Abramson, H. and Rogers, M., Eds. 1989. Metaprogramming in Logic Programming. MIT Press, Cambridge, MA.]]

[2]

Aczel, P. 1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, Amsterdam, The Netherlands, 739--782.]]

[3]

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.]]

[4]

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.]]

[5]

Apt, K. and Turini, F., Eds. 1995. Meta-Logics and Logic Programming. Logic Programming Series. MIT Press, Cambridge, MA.]]

[6]

Basin, D. and Constable, R. 1993. Metalogical frameworks. In Logical Environments, G. Huet and G. Plotkin, Eds. Cambridge University Press, Cambridge, MA, 1--29.]]

[7]

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.]]

[8]

Basin, D. and Matthews, S. 2000. Structuring metatheory on inductive definitions. Inform. Computat. 162, 1--2 (Oct./Nov.), 80--95.]]

[9]

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.]]

[10]

Bouhoula, A., Jouannaud, J.-P., and Meseguer, J. 2000. Specification and proof in membership equational logic. Theoret. Comput. Sci. 236, 35--132.]]

[11]

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.]]

[12]

Bruynooghe, M., Ed. 1990. Proceedings Second Workshop on Meta-Programming in Logic. K. U. Leuven, Leuven, Belgium.]]

[13]

Clavel, M. 2000. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications, CSLI Publications, Stanford, CA.]]

[14]

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.]]

[15]

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.]]

[16]

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.]]

[17]

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.]]

[18]

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.]]

[19]

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.]]

[20]

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.]]

[21]

Clavel, M. and Meseguer, J. 2002. Reflection in conditional rewriting logic. Theoret. Comput. Sci. 285, 2, 245--288.]]

[22]

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.]]

[23]

Cointe, P., Ed. 1999. Proceedings of Reflection'99. Lecture Notes in Computer Science, vol. 1616. Springer-Verlag, Berlin, Germany.]]

[24]

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.]]

[25]

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.]]

[26]

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.]]

[27]

Durán, F. 1999. A reflective module algebra with applications to the Maude language. Ph.D. dissertation. University of Málaga, Málaga, Spain.]]

[28]

Ehrig, H. and Mahr, B. 1985. Fundamentals of Algebraic Specification 1. EATCS Monographs on Theoretical Computer Science, vol. 6. Springer-Verlag, Berlin, Germany.]]

[29]

Feferman, S. 1988. Finitary inductively presented logics. In Logic Colloquium '88. North-Holland, Amsterdam, The Netherlands, 191--220.]]

[30]

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.]]

[31]

Gardner, P. 1992. Representing logics in type theory. Ph.D. dissertation. University of Edinburgh, U.K. Also published as ECS-LFCS-92-227.]]

[32]

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.]]

[33]

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.]]

[34]

Goguen, J. and Burstall, R. 1992. Institutions: Abstract model theory for specification and programming. J. ACM 39, 1 (Jan.), 95--146.]]

[35]

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.]]

[36]

Gordon, M. and Melham, T. 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, U.K.]]

[37]

Harper, R., Honsell, F., and Plotkin, G. 1993. A framework for defining logics. J. ACM 40, 1 (Jan.), 143--184.]]

[38]

Harrison, J. 1995. Metatheory and reflection in theorem proving: a survey and critique. Tech. Rep. CRC-053, SRI Cambridge, Cambridge U.K.]]

[39]

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.]]

[40]

Hill, P. and Lloyd, J. 1994. The Gödel Programming Language. MIT Press, Cambridge, MA.]]

[41]

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.]]

[42]

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.]]

[43]

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.]]

[44]

Kiczales, G., Ed. 1996. Proceedings of Reflection'96, G. Kiczales, ed. Xerox PARC, San Francisco, CA.]]

[45]

Kiczales, G., des Rivieres, J., and Bobrow, D. G. 1991. The Art of the Metaobject Protocol. MIT Press, Cambridge, MA.]]

[46]

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.]]

[47]

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.]]

[48]

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.]]

[49]

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.]]

[50]

Martí-Oliet, N. and Meseguer, J. 2002b. Rewriting logic: Roadmap and bibliography. Theoret. Comput. Sci. 285, 121--154.]]

[51]

Matthews, S. 1992. Reflection in logical systems. See Smith and Yonezawa {1992}, 178--183.]]

[52]

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.]]

[53]

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.]]

[54]

Meseguer, J. 1989. General logics. In Logic Colloquium'87, H.-D. Ebbinghaus et al., Eds. North-Holland, Amsterdam, The Netherlands, 275--329.]]

[55]

Meseguer, J. 1992. Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96, 1, 73--155.]]

[56]

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.]]

[57]

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.]]

[58]

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.]]

[59]

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.]]

[60]

Paulson, L. C. 1994b. Isabelle : A Generic Theorem Prover; with Contributions by Tobias Nipkow. Lecture Notes in Computer Science, vol. 828. Springer, Berlin, Germany.]]

[61]

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.]]

[62]

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.]]

[63]

Ruess, H. 1995. Formal meta-programming in the calculus of constructions. Ph.D. dissertation. Universität Ulm, Ulm, Germany.]]

[64]

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.]]

[65]

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.]]

[66]

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.]]

[67]

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.]]

[68]

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.]]

[69]

Shankar, N. 1994. Metamathematics, Machines, and Gödel's Proof. Cambridge University Press, Cambridge, U.K.]]

[70]

Smith, B. and Yonezawa, A., Eds. 1992. Proc. IMSA'92---International Workshop on Reflection and Meta-Level Architecture. Information-Technology Promotion Agency, Tokyo, Japan.]]

[71]

Smith, B. C. 1984. Reflection and semantics in Lisp. In Proceedings of POPL'84. ACM Press, New York, NY, 23--35.]]

[72]

Smorynski, C. 1977. The incompleteness theorems. In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, Amsterdam, The Netherlands, 821--865.]]

[73]

Smullyan, R. M. 1994. Diagonalization and Self-Reference. Oxford University Press, Oxford, U.K.]]

[74]

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.]]

[75]

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.]]

[76]

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/&sim;felty/LFM99/.]]

[77]

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.]]

[78]

Turchin, V. F. 1986. The concept of a supercompiler. ACM Trans. Programm. Lang. Syst. 8, 3, 292--325.]]

[79]

van Emden, M. and Kowalski, R. 1976. The semantics of predicate logic as a programming language. J. ACM 23, 733--42.]]

[80]

Wand, M. and Friedman, D. P. 1988. The mystery of the tower revealed. Lisp Symbol. Computat. 1, 1, 11--38.]]

[81]

Weyhrauch, R. W. 1980. Prolegomena to a theory of mechanized formal reasoning. Art. Intell. 13, 133--170.]]

Cited By

Cerone A(2025)Multifaceted formal methods and their interdisciplinary role — From the cathedral of ‘components as coalgebras’ to the HCI context and the open source software bazaarJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.101006142(101006)Online publication date: Jan-2025
https://doi.org/10.1016/j.jlamp.2024.101006
Olivieri FGovernatori GCristani MRotolo ASattar A(2023)Deontic meta-rulesJournal of Logic and Computation10.1093/logcom/exac081Online publication date: 26-Sep-2023
https://doi.org/10.1093/logcom/exac081
Olarte CPimentel ERocha C(2023)A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100827130(100827)Online publication date: Jan-2023
https://doi.org/10.1016/j.jlamp.2022.100827
Show More Cited By

Index Terms

Reflective metalogical frameworks
1. Computing methodologies
  1. Machine learning
    1. Machine learning approaches
      1. Logical and relational learning
        Inductive logic learning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation

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

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 5, Issue 3

July 2004

192 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/1013560

Issue’s Table of Contents

Copyright © 2004 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2004

Published in TOCL Volume 5, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
625
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cerone A(2025)Multifaceted formal methods and their interdisciplinary role — From the cathedral of ‘components as coalgebras’ to the HCI context and the open source software bazaarJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.101006142(101006)Online publication date: Jan-2025
https://doi.org/10.1016/j.jlamp.2024.101006
Olivieri FGovernatori GCristani MRotolo ASattar A(2023)Deontic meta-rulesJournal of Logic and Computation10.1093/logcom/exac081Online publication date: 26-Sep-2023
https://doi.org/10.1093/logcom/exac081
Olarte CPimentel ERocha C(2023)A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100827130(100827)Online publication date: Jan-2023
https://doi.org/10.1016/j.jlamp.2022.100827
Durán FEker SEscobar SMartí-Oliet NMeseguer JRubio RTalcott C(2022)Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)Automated Reasoning10.1007/978-3-031-10769-6_31(529-540)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_31
Olivieri FGovernatori GCristani MSattar A(2021)Computing Defeasible Meta-logicLogics in Artificial Intelligence10.1007/978-3-030-75775-5_6(69-84)Online publication date: 17-May-2021
https://dl.acm.org/doi/10.1007/978-3-030-75775-5_6
Durán FMeseguer J(2018)Maude's module algebraScience of Computer Programming10.1016/j.scico.2006.07.00266:2(125-153)Online publication date: 31-Dec-2018
https://dl.acm.org/doi/10.1016/j.scico.2006.07.002
Meseguer J(2018)Symbolic Reasoning Methods in Rewriting Logic and MaudeLogic, Language, Information, and Computation10.1007/978-3-662-57669-4_2(25-60)Online publication date: 27-Jun-2018
https://doi.org/10.1007/978-3-662-57669-4_2
Ibañez YMossakowski TSannella DTarlecki A(2015)Modularity of Ontologies in an Arbitrary InstitutionLogic, Rewriting, and Concurrency10.1007/978-3-319-23165-5_17(361-379)Online publication date: 27-Aug-2015
https://doi.org/10.1007/978-3-319-23165-5_17
Meseguer J(2012)Twenty years of rewriting logicThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2012.06.00381:7-8(721-781)Online publication date: Oct-2012
https://doi.org/10.1016/j.jlap.2012.06.003
Clavel MMartí-Oliet NPalomino M(2011)Parameterized metareasoning in membership equational logicFormal modeling10.5555/2074591.2074610(277-298)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.5555/2074591.2074610
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents