Reflective metalogical frameworks.
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.
Introduction
A logical framework is a formal logic with an associated methodology that is employed for representing
and using other logics, theories, and, more generally, formal systems. A minimum
requirement for a logical framework is that object logics and their entailment relations can be
conservatively represented in the framework logic. Typically we also demand more. For exam-
ple, that the representation preserves appropriate kinds of structure and that there is a small
conceptual distance between the object logic and its representation and use in the framework
logic.
To compare logical frameworks and analyze their eectiveness, it is helpful to make further
distinctions concerning their intended application. In particular, we can distinguish between
logical frameworks, where the emphasis is on reasoning in a logic, in the sense of simulating
its derivations in the framework logic, and metalogical frameworks, where the emphasis is on
reasoning about logics. Metalogical frameworks are more powerful, as they include the ability to
reason about a logic's entailment relation as opposed to merely being adequate to demonstrate
entailment. Moreover, if a metalogical framework should provide a basis for formal metathe-
ory, it should also support reasoning about relationships between logics. This is standard in
metamathematics and is common practice when reasoning about formal systems in computer
science.
The dierent kinds of applications make dierent demands on the framework logic. In a
logical framework it is sucient to use representations of proof rules to construct demonstrations
of (object logic) entailments. This is the approach taken in logical frameworks like Isabelle [28]
and the Edinburgh LF [15]. Note that under this approach one may formalize logics and theories
where induction is present within the theory (e.g., induction over the natural numbers in Peano
Arithmetic), but induction is not present over the encoded theories. That is, the framework
logic does not support induction over the terms and proofs of a theory, and in general there is
no reason to assume that sound induction principles exist.
In a metalogical framework, it is essential to have induction over theories. When reasoning
about logics, standard proof-theoretic arguments usually require induction over the formulae or
derivations of the object logic. Induction is also one of the key concepts in reasoning about formal
systems in computer science, e.g., programming language semantics.
Standard approaches to metalogical frameworks
Several approaches have been considered in the past to strengthen logical frameworks so that they
can function as metalogical frameworks. One approach, which we might summarize as \modules
with explicit induction," is to formalize theories in a framework logic supporting some notion
of a module, where each module comes with its own, explicitly given, induction principle. For
example, in [1], theories were specied by collections of parameterized modules (-types) within
the Nuprl type theory (a constructive, higher-order logic), and each module included its own
induction principle for reasoning about terms or proofs. This approach can be very powerful and
can be used to show, e.g., that rules are admissible, or to relate dierent theories.
An alternative approach is to formalize theories directly using inductive denitions in a frame-work
logic or framework theory that is strong enough to formalize the corresponding induction
principles. A simple example of this is the rst-order theory FS 0 of [13], which has been used
by [20] to carry out experiments in formal metatheory. In FS 0
, inductive denitions are terms
in the framework logic, and the framework logic has an induction rule for reasoning about such
terms. Another common choice is formalization of inductive denitions in strong \foundational"
framework logics like higher-order logic or set-theory [27, 14], or calculi like the calculus of constructions
with inductive denitions [26]. In higher-order logic and set theory one can internally
develop a theory of inductive denitions, where inductive denitions correspond to terms in
the metatheory (e.g., formalized as the least-xedpoint of a monotonic function) and, from the
denition, induction principles are formally derived within the framework logic. Alternatively,
in the calculus of constructions, given an inductive denition, induction principles are simply
added, soundly, to the metalogic. Current research in this area focuses on appropriate induction
principles for logics with higher-order quantication, which support higher-order abstract syntax
[11, 21, 29].
A new paradigm
In this paper we propose a new alternative: in some cases we can take the step from a logical
framework to a metalogical framework by augmenting the logical framework with re
ection
and induction. This is the case when formalization of theories in the framework logic support
induction principles that can be re
ected back into the framework logic. This proposal can
be summarized with the slogan \logical frameworks with re
ection and initiality are metalogical
frameworks," which can in turn be expressed by the formula
Logical Framework
ection Initiality =) Metalogical Framework. (1)
After making this idea precise, we present a concrete realization of it using rewriting logic,
which we use to support the thesis that combining a logical framework with re
ection can result
in an eective metalogical framework. Rewriting logic is not the only candidate for a re
ective
logical framework, but we believe it is a good one. Rewriting logic has been demonstrated to be
a good logical framework [17, 24]. Moreover the logic is balanced on a point where it is strong
enough to naturally formalize dierent entailment systems, but it is weak enough that its theories
or modules always have initial models. This means that induction on these initial models is a
sound reasoning principle. The key then is to re
ect these reasoning principles into the logic.
To sum up, we see our contributions as both theoretical and practical. Theoretically, our
work contributes to answering the question \what is a metalogical framework?" by proposing
re
ective logical frameworks, whose theories have initial models, as a possible answer. Moreover,
it illuminates the interrelationship between logical and metalogical frameworks, and the role of
re
ection as a key ingredient for turning a logical framework with initial models into a metalogical
one. Practically, our case study shows that rewriting logic, combined with re
ection, is an
eective metalogical framework that is well suited for nontrivial kinds of metatheoretic reasoning.
Re
ective metalogical frameworks
2.1 Re
ective logics
Intuitively, a re
ective logic is a logic in which important aspects of its metatheory can be
represented at the object level | that is, in the logic. Two standard metatheoretic notions that
can be so re
ected are theories 1 and entailment relations.
A general axiomatic notion of re
ective logic was recently proposed in [9, 4] . The key concept
is the notion of a universal theory. Let ' be the entailment relation dened in a logic, let T be a
theory over a signature , and let sen(T ) be the set of -sentences. Then, given a set of theories
C, a theory U is C-universal if there is a function, called a representation function,
such that for each T 2 C; ' 2 sen(T ),
A logic is re
ective when it contains a theory U that is C-universal and, in addition, U 2 C.
Note that in a re
ective logic, since U itself is representable, representation can be iterated; hence
we immediately have a \re
ective tower"
Note that if a framework logic is to support
exible metatheoretic reasoning, e.g., where we
can compare theories and reason about families of theories, then, in practice we require more
than a representation function. Namely, we require a theory representation calculus. We will not
formalize requirements for this here (see [12]), but such a calculus will typically treat theories
as rst-class objects and provide constructors, destructors, and discriminators, for building and
reasoning about theories.
2.2 Re
ecting induction
In the introduction, we proposed that logical frameworks with re
ection and initiality can be
used as eective metalogical frameworks. Above we have given a logic-independent account of
re
ection. We now consider what we require from a logical framework so that we can use re
ection
to augment theories with induction principles. In particular, if the combination is to be a useful
metalogical framework, we also require that:
1. the logical framework must be weak enough so that there are valid induction principles for
reasoning about all formalized theories, and
2. strong enough so that it really is a viable logical framework.
We argue this as follows. If 2 is satised, then object logics and their entailment relations can
be represented as theories in the logical framework, and if 1 is also satised, then theories in the
logical framework, including those representing object logics, admit induction. Now, if the logical
1 In this paper we consider a theory as a pair consisting of a language syntax , called a signature,
and a collection of axioms . A logician will typically treat the theory's language and its theorems extensionally
as sets. However, it is more practical (computationally) to specify the sets using constructors:  for building
formulae, and for building proofs of theorems.
framework is re
ective, then it contains a universal theory where theories can be represented. It
is then possible to extend the universal theory so that sound reasoning principles | in particular,
induction | for each theory in the logic can be re
ected ; that is, sound reasoning principles for
each theory can be added to the universal theory.
2.3 Induction and initiality
How can we capture the notion of induction in an abstract and logic-independent way? If the
framework logic is such that its theories have initial models, then inductive reasoning principles
can be soundly added to a theory to derive sentences valid in its initial model. This method is very
for example, for equational logic, induction and initiality are equivalent concepts [25],
and for dierent propositional calculi, cut elimination results can be seen as inductive properties
of their initial categorical models [16].
We are therefore interested in a re
ective metalogical framework having a universal theory
U such that each theory in the framework logic has initial models. Under such circumstances it
can be possible (as indeed it is the case for rewriting logic) to extend the theory U to a theory I
that adds sound inductive principles to each theory in the logic, including U itself. This means
that we can use re
ection in I to reason soundly about the inductive properties of any theory T .
This approach can be surprisingly powerful. Since U represents all theories in the logic,
by reasoning by induction on U or its extension I we may be able to inductively reason about
properties satised not only by a single theory, but by entire families of theories. We will give
an example of this later, namely, a metatheorem not just for a single logic, but for a family of
logics.
3 Rewriting logic as a re
ective metalogical framework
We now show how the above, abstractly presented, ideas can be concretely realized. Our realization
in rewriting logic supports re
ection and initiality as described above, and theories are
rst-class objects in the universal theory. Moreover, its implementation in the Maude system
supports object level reasoning via metalevel computation in (an extension of) the universal the-
ory: any reasoning in the object logics (e.g., to show that formulae are syntactically well-formed
or provable) can be performed by re
ection down, that is, by computation in the theory that
represents the object logic.
3.1 Rewriting logic
Rewriting logic [22] is a simple logic whose sentences are sequents of the form
with t and t 0 -terms on a given signature . From the logical point of view, we can think of
rewriting logic as a framework logic in which any inference system can be naturally formalized
by expressing each inference rule as a (possibly conditional) rewrite rule.
Theories in rewriting logic are triples (; E; R), with  a signature of operators, E a set
of -equations, and R a collection of (possibly conditional) rewrite rules. The inference rules
of rewriting logic [22] allow the derivation of all rewrites possible in a given theory. Rewriting
is understood modulo the equations E. This makes inference
exible and abstract since the
equations E can take care of structural bookkeeping. For example, structural rules for sequents
can be \internalized" by rewriting modulo appropriate equational axioms.
Since a rewrite theory (; E; R) has an underlying equational theory (; E), rewriting logic is
parameterized by the choice of the underlying equational logic. An attractive choice in terms of
expressiveness is membership equational logic [23], a logic that has sorts, subsorts, and overloading
of function symbols, and is capable of expressing partiality using equational conditions. Atomic
sentences are equations with s a sort. General axioms
are Horn clauses on such atoms. Since we can view an equational theory (; E) as a rewrite
theory (; E; ;), there is an obvious sublogic inclusion MEqtl  RWLogic, from membership
equational logic into rewriting logic. Both membership equational logic and rewriting logic have
initial models [23, 22].
3.2 Rewriting logic is a good logical framework
Rewriting logic is noncommittal about the structure and properties of the formulae expressed
by -terms. They are user-denable as an algebraic data type satisfying equational axioms, so
that rewriting deduction takes place modulo such axioms. Because of this ecumenical neutrality,
rewriting logic has good properties as a logical framework. In [17, 18, 19], many examples of
logic representations are given, including rst-order linear logic, sequent presentations of modal
and propositional logics, Horn logic with equality, and so on. In all such examples, the representational
distance between the object logic and its representation is practically zero, that is, the
representations are direct and faithfully mimic the original logics.
Note that there are several ways of conservatively representing a logic (with a nitary syntax
and inference system) within rewriting logic. A simple and direct way is to turn the inference
rules into rewrite rules, which may be conditional if the inference rules have side conditions.
Alternatively, we can use the underlying membership equational logic to represent theoremhood
in a logic as a sort in a membership equational theory. Conditional membership equations then
directly support the representation of rules as schemas, which is typically used in presenting
logics and formal systems. This is the approach we have adopted in the experimental work that
we report in Section 4.
3.3 Rewriting logic is re
ective
Rewriting logic is re
ective [10, 4]. There is a universal theory UNIVERSAL, and a representation
function encoding pairs consisting of a rewrite theory T and a sentence in it as sentences
in UNIVERSAL. For any nitely presented rewrite theory T (including UNIVERSAL itself) and any
terms t, t 0 in T , the representation function is dened by
where T , t, t 0 are terms in UNIVERSAL. Then, the equivalence (2) for rewriting logic that is proved
in [10, 4] takes the form
4 Maude and experimental work
In this section we report on a case study in metatheoretic reasoning that is based on the above
ideas. For our study we used Maude [8, 6], which is a re
ective logic based on rewriting logic.
Maude's implementation has been designed with the explicit aims of supporting executable spec-
ication and re
ective computation.
4.1 Maude's metalevel
Maude's language design and implementation make systematic use of the fact that rewriting logic
is re
ective to give the user a well-dened gateway to the metatheory of rewriting logic [5]. This
entry point is the predened module META-LEVEL, which provides the user with the functionality
necessary to exploit the universal theory for rewriting logic. In the module META-LEVEL, terms in
modules are reied as elements of a data type Term, and Maude modules (that is, theories with
initial semantics) are reied as elements of a data type Module.
We illustrate the general syntax for representing modules, with a simple example: a module
NAT for natural numbers with zero and successor and with a commutative addition operator.
fmod NAT is
sorts Zero Nat .
subsort Zero < Nat .
vars
The representation NAT of NAT in META-LEVEL is the term
fmod 'NAT is
nil
subsort 'Zero < 'Nat .
none
of sort Module.
The processes of reducing a term to normal form in a functional module (that is, a Church-Rosser
and terminating equational theory) and of rewriting a term in a system module (that
is, a rewrite theory) using Maude's default interpreter are reied respectively by functions
meta-reduce and meta-apply. In particular, meta-reduce takes as arguments the representations
of a module T , and of a term t or a membership predicate t : s in that module. When the
second argument is the representation t of a term t in T , meta-reduce returns the representation
of the fully reduced form of the term t using the equations in T . Similarly, when the second
argument of meta-reduce is the representation of a membership predicate t : s, the term t is
fully reduced using the equations in T and then the representation of the Boolean value of the
corresponding predicate is returned. Hence meta-reduce returns f'trueg'Bool if T
otherwise, it returns f'falseg'Bool.
4.2 Internal strategies
Since the Maude system is a particular implementation of the metatheory of rewriting logic, the
module META-LEVEL also provides gateway to the Maude system itself. By extending META-LEVEL,
the user can eectively customize Maude (in Maude) to t his particular computational needs.
Using rewriting rules at the metalevel, user-denable internal strategy languages can be dened
to change the (default) operational semantics of Maude for system modules (that is, for rewrite
theories that need not be Church-Rosser or terminating) [10, 4]. The idea is to use the functions
meta-reduce and meta-apply as basic strategies, and then to extend the module META-LEVEL
by additional (arbitrarily complex) strategy functions, dened by rewrite rules.
4.3 An inductive theorem prover in Maude
To re
ect and use induction principles, we formalize an appropriate deductive system in Maude.
Furthermore, we specify strategies for applying rules in this system by specifying rewriting strategies

In general, based on the concepts of re
ection and internal strategy languages, theorem-proving
tools have a simple \re
ective" design in Maude [7]. An inductive theorem prover, which
we implemented for metatheoretic reasoning, illustrates this. The idea is that the theory T ,
for which we want to prove inductive theorems, is at the object level; an inference system I
for inductive proofs uses T as data and therefore should be specied as a rewrite theory at the
metalevel; then, dierent proof tactics to guide the application of the rewrite rules specifying
the inference rules in I are strategies that can be represented at the meta-metalevel. This is
illustrated by the following picture:
?Meta-metalevel
Metalevel
?Object level Object theory
induction
ITP: inference rules for
inductive proofs
S-ITP: strategies for
The module ITP is an extension of the module META-LEVEL and realizes, for the case of rewriting
logic, the extension I of the universal theory U with inductive principles discussed in Section 2.3.
are represented in ITP as terms of sort Formula built with the constructors equality,
implication, conjunction, and VQuantification. For example, the formula
is represented in ITP by the term
The (sub)goals for the inductive theorem prover are represented with the constructors proveinInitial
and proveinVariety, for proofs in the initial model and proofs in the variety, respectively. Sets
of (sub)goals are built with the constructor goalSet, with emptyGoalSet the empty set of goals.
For example, the goal
is represented in ITP by the term
proveinInitial(I, NAT,
where I should be a string of positive numbers. The strings of positive numbers are used to
number the (sub)goals in a proof.
With this machinery in hand, it is possible to formalize in ITP induction principles for Maude
modules. In our work, we formalize rewrite rules that specify the rules of inference for proving
that a universally quantied formula is an inductive consequence of a given membership algebra
specication. For example, the rule induction below rewrites a (sub)goal representing the task
of proving inductively in a module M a given formula 8fx; Xg to a set of subgoals representing
the tasks of proving inductively the base case(s) and the induction step(s) that result from
induction on the variable x. The function getVars extracts the variable declaration from the
metarepresentation of the module M . The function findSortV nds the metarepresentation of
the sort s of the variable x in the module M . The function extractRuleSystem extracts from
the metarepresentation of the module M all the clauses that dene the set s in M . (Notice that
specications in membership equational logic coincide with a special case of many-sorted Horn
logic with equality.) Finally, the function makeNewGoalSetF generates from the dening clauses
of s the corresponding base case(s) and induction step(s).
IntString . var Mod : Module .
vars Alpha Beta : Formula .
rl [induction]:
proveInitial(Idx, Mod,
makeNewGoalSetF(intString(Idx, 1), Mod, Xs, X, Alpha,
extractRuleSystem(Mod, findSortV(X, getVars(Mod)))) .
Proving a theorem consists then in applying (with a strategy and, therefore, in the module S-ITP,
at the meta-metalevel) the rewrite rules in the module ITP to the term representing the initial
(sub)goals until it is rewritten to the term empty.
4.4 An example: the deduction theorem
As an example, consider the deduction theorem for minimal logic (of implication). This theorem
is interesting for several reasons. To begin with, it is a central metatheorem that holds for many
Hilbert systems and justies proof under temporary assumption in the manner of a natural
deduction proof system. Moreover, although relatively simple, it illustrates some subtle aspects
of formal metareasoning. For example, it is actually a metatheorem not about a particular
deductive system, but rather one that relates dierent deductive systems: one in which A ! B
is proven and a second (which is the rst, augmented by the axiom A) in which B is proven.
Indeed, as A is an arbitrary formula, the standard statement of the deduction theorem is actually
a statement about the relationship between a family of pairs of deductive systems. And as we
will see, it can be formalized even more generally than this.
The deduction theorem is proven by induction over the structure of derivations. We start
by specifying minimal logic as a module in Maude. The formulae of minimal logic correspond
to members of the set LM , built from the binary connective ! (written inx, associating to the
right) and sentential constants. Theorems correspond to members of a second set TM , and are
either instances of the standard Hilbert axiom schemata
and
or are generated by applying the rule modus ponens :
The module MINIMAL below represents minimal logic within membership equational logic (and
rewriting logic), in the sense that a formula  is a theorem in minimal logic if and only if its
representation  is a term of sort Theorem, that is, the membership assertion  : Theorem is true
in MINIMAL.
mod MINIMAL is
sorts SentConstant Formula Theorem .
subsort SentConstant < Formula .
subsort Theorem < Formula .
vars
mb A -> (B -> Theorem .
mb Theorem .
Theorem if Theorem and A : Theorem .
We write 'M A to denote that A 2 TM , and A 'M B to denote that if minimal logic is
extended with the additional axiom A, then B belongs to the resulting set of theorems. The
deduction theorem then states that for any A and B in LM ,
This metatheorem is proven by induction on the structure of derivations in minimal logic extended
with the axiom A.
According to our representation of minimal logic in rewriting logic, we can rephrase the
deduction theorem in the following terms: for any formulae A and B, if B:Theorem is true in the
module MINIMAL extended with the membership axiom mb A:Theorem, then A ! B:Theorem
is true in MINIMAL.
Notice that this theorem states an implication between the truth of two membership assertions
over two dierent membership equational theories. Since the truth of membership assertions over
theories is dened in the metatheory of rewriting logic, the \object" theory about which we have
to prove the deduction theorem is in fact, in our setting, the universal theory for rewriting logic.
This corresponds to the following goal for the inductive theorem prover, where A and B are
variables of sort Term in the module META-LEVEL:
meta-reduce(
(mod'ARROW is
including 'BOOL .
subsort 'SentConstant < 'Formula .
subsort 'Theorem < 'Formula .
'Theorem .
mb 'impl['A, 'impl['B, 'Theorem .
mb 'impl['impl['A, 'B],
'impl['impl['A, 'impl['B, 'C]], 'impl['A, 'Theorem .
' and [('impl['A,
none
none
meta-reduce(
(mod'ARROW is
including 'BOOL .
subsort 'SentConstant < 'Formula .
subsort 'Theorem < 'Formula .
mb 'impl['A, 'impl['B, 'Theorem .
mb 'impl['impl['A, 'B],
'impl['impl['A, 'impl['B, 'C]], 'impl['A, 'Theorem .
' and [('impl['A,
none
none
'impl[ A ,
Observe that applying induction on the variable B using the induction rule introduced
above will be of little use here: B is a variable of sort Term and, therefore, the base case(s) and
the induction step(s) that the function makeNewGoalSetF will generate correspond to the clauses
that dene the set Term in the module META-LEVEL. Instead what we need are the base case(s)
and the induction step(s) that correspond to the clauses dening the subset of the set Term that
includes only those terms of sort Term representing at the metalevel terms of sort Theorem in the
module MINIMAL extended with the membership axiom mb A :Theorem.
To generate the appropriate induction, we extend the module ITP with a new rule induction*.
This rule generates the appropriate base case(s) and induction step(s) when proving in the module
META-LEVEL a universally quantied implicative formula 8fx; induction
on a variable x of sort Term, if the implicative formula includes in its antecedent a clause  i that
restricts the scope of the variable x to metarepresentations of terms of a sort s in a module T .
The function makeNewGoalSetF* uses the set of clauses that dene the set s in the module T
(obtained with the function extractRuleSystem) to generate the appropriate base case(s) and
induction step(s).
rl [induction*]:
conjunction(Beta,
Alpha)))
makeNewGoalSetF*(intString(Idx, 1), META-LEVEL, Xs, X, Beta, Alpha,
extractRuleSystem(T, s)) .
Using the rule induction*, along with the rest of inference rules specied in ITP, we have
proven this metatheorem with a strategy dened in S-ITP that mirrors the standard presentation
of the proof of the deduction theorem.
4.5 Proving a parameterized deduction theorem in ITP
In [2, 3], Basin and Matthews showed how metatheorems that are parameterized by their scope
of application can be proved using a theory of parameterized inductive denitions as a metathe-
ory. To illustrate the notion of a scoped metatheorem they present a generalized version of the
deduction theorem that can be applied to all extensions of the language and axioms of minimal
logic as well as extensions of rules that satisfy certain conditions. From their theorem it follows,
for example, that the deduction theorem holds not just for minimal logic of implication, but also
for any propositional or rst-order extension, but not necessarily for extensions to modal logics
(which would require adding new rules, as opposed to axioms).
Since the requirements demanded of the metatheory in [2, 3] | namely, that we can build
families of sets using parameterized inductive denitions, and that we can reason about their
elements by induction | are indeed satised by rewriting logic and our theory representation
calculus, we should be able to formalize scoped metatheorems as goals in the extended module
ITP and prove them (probably using strategies) in the module S-ITP.
To illustrate this idea, we consider a generalized version of the deduction theorem that applies
to all extensions of minimal logic with a new rule of the form
that satises a certain condition; namely, in the step case we can use the assumptions A ! C
and A ! D to prove A ! E. This metatheorem corresponds to the following goal for the
inductive theorem prover, where A , B , C , D , and E are variables of sort Term in the module
((meta-reduce(ARROW+, 'impl[ A , C
meta-reduce(ARROW+, 'impl[ A , D
meta-reduce(ARROW+, 'impl[ A ,
meta-reduce(ARROW+, 'impl[ A ,
where ARROW+ is shorthand for the term
(mod'ARROW is
including 'BOOL .
subsort 'SentConstant < 'Formula .
subsort 'Theorem < 'Formula .
mb 'impl['A, 'impl['B, 'Theorem .
mb 'impl['impl['A, 'B],
'impl['impl['A, 'impl['B, 'C]], 'impl['A, 'Theorem .
' and ['impl['A,
none
none
and ARROW+A is shorthand for the term
(mod'ARROW is
including 'BOOL .
subsort 'SentConstant < 'Formula .
subsort 'Theorem < 'Formula .
'Theorem .
mb 'impl['A, 'impl['B, 'Theorem .
mb 'impl['impl['A, 'B],
'impl['impl['A, 'impl['B, 'C]], 'impl['A, 'Theorem .
' and ['impl['A,
none
none
endm).
Using the rule induction*, along with the rest of the inference rules specied in ITP, we
have proven this metatheorem with a strategy dened in S-ITP that follows the expected proof
strategy, beginning with induction on the variable B .
5 Conclusion
We have presented, both abstractly and concretely, a new approach to metatheoretic reasoning
based on using re
ective logical frameworks whose theories have initial models. Initial experiments
with these ideas are encouraging. We can formalize theories as modules in Maude and use
the Maude system as a logical framework to prove theorems in the theories. Moreover, using
re
ective reasoning we can exploit the initiality of these modules by re
ectively formalizing induction
principles over them. This yields a formalization well-suited for reasoning about theories
and their interrelationships.



--R

Metalogical frameworks.
Scoped metatheorems.
Structuring metatheory on inductive de
Re ection in General Logics and in Rewriting Logic with Applications to the Maude Language.



Principles of Maude.
Axiomatizing re ective logics and languages.
Re ection and strategies in rewriting logic.


Finitary inductively presented logics.
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.
A framework for de
Why commutative diagrams coincide with equivalent proofs.



Experience with FS0 as a framework theory.
A logic for reasoning with higher-order abstract syntax
Conditional rewriting logic as a uni
Membership algebra as a semantic framework for equational speci
Research directions in rewriting logic.
Initiality, induction and computability.
Inductive De

Isabelle : a generic theorem prover

--TR
The concept of a supercompiler
Models and equality for logical programming
Meta-programming in logic programming
Analysis of meta-programs
Conditional rewriting logic as a unified model of concurrency
A framework for defining logics
Institutions: abstract model theory for specification and programming
Introduction to HOL
Reflecting the semantics of reflected proof
The GoMYAMPERSANDuml;del programming language
Metalogical frameworks
Experience with <italic>FS</italic>10<subscrpt>0</subscrpt> as a framework theory
General logics and logical frameworks
Meta-logics and logic programming
Metamathematics, machines, and GoMYAMPERSANDuml;del''s proof
The Semantics of Predicate Logic as a Programming Language
Specification and proof in membership equational logic
Structuring metatheory on inductive definitions
Reflection in Rewriting Logic
The Art of the Metaobject Protocol
Fundamentals of Algebraic Specification I
Metalogical Frameworks II
Rewriting logic
Maude
Reflection in conditional rewriting logic
Meta-Programming in Logic
Logic Programming Synthesis and Transformation - Meta-Programming in Logic
A Type-Theoretic Approach to Induction with Higher-Order Encodings
Inductive Definitions in the system Coq - Rules and Properties
Primitive Recursion for Higher-Order Abstract Syntax
Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving
Membership algebra as a logical framework for equational specification
Maude as a Formal Meta-tool
Programming
Introducing Institutions
Computational Metatheory in Nuprl
A Fixedpoint Approach to Implementing (Co)Inductive Definitions
Automated Theorem Proving in a Simple Meta-Logic for LF
System Description
A Logic for Reasoning with Higher-Order Abstract Syntax
Reflection and semantics in LISP
The Art of the Interpreter or, The Modularity Complex (Parts Zero, One, and Two)

--CTR
Francisco Durn , Jos Meseguer, Maude's module algebra, Science of Computer Programming, v.66 n.2, p.125-153, April, 2007
Bow-Yaw Wang, Modeling and analyzing applications with domain-specific languages by reflective rewriting: a case study, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
Steven Eker , Narciso Mart-Oliet , Jos Meseguer , Alberto Verdejo, Deduction, Strategies, and Rewriting, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.11, p.3-25, July, 2007
Manuel Clavel , Jos Meseguer , Miguel Palomino,  Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Theoretical Computer Science, v.373 n.1-2, p.70-91, March, 2007
Roberto Bruni , Jos Meseguer, Semantic foundations for generalized rewrite theories, Theoretical Computer Science, v.360 n.1, p.386-414, 21 August 2006
rewriting logic;metalogics;reflection;membership equational logic