Rewriting logic as a metalogical framework

David Basin, Manuel Clavel, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 logics support reflective reasoning and their theories always have initial models. We present a concrete realization of this idea in rewriting logic. Theories in rewriting logic always have initial models and this logic supports reflective reasoning. This implies that inductive reasoning is valid when proving properties about the initial models of theories in rewriting logic, and that we can use reflection to reason at the metalevel about these properties. In fact, we can uniformly reflect induction principles for proving metatheorems about rewriting logic theories and their parameterized extensions. We show that this reflective methodology provides an effective framework for different, non-trivial, kinds of formal metatheoretic reasoning; one can, for example, prove metatheorems that relate theories or establish properties of parameterized classes of theories. Finally, we report on the implementation of an inductive theorem prover in the Maude system, whose design is based on the results presented in this paper.

Original languageEnglish (US)
Title of host publicationFST TCS 2000
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 20th Conference, Proceedings
EditorsSanjiv Kapoor, Sanjiva Prasad
Number of pages26
ISBN (Print)3540414134, 9783540414131
StatePublished - 2000
Externally publishedYes
Event20th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2000 - New Delhi, India
Duration: Dec 13 2000Dec 15 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other20th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2000
CityNew Delhi

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Rewriting logic as a metalogical framework'. Together they form a unique fingerprint.

Cite this