Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 1, February 2002: pp. 167-208

A Foundation for Metareasoning Part I: The Proof Theory

Giovanni Criscuolo1, Fausto Giunchiglia2 and Luciano Serafini3

1Dipartimento di Scienze Fisiche, University of Naples, 80125 Napoli, Italy. E-mail: vanni@na.infn.it
2Dipartimento di Informatica e Studi Aziendali, University of Trento, 38100 Trento, Italy, and ITC-IRST, Centro per la Ricerca Scientifica e Tecnologica, 38050 Trento, Italy. E-mail: fausto@artemide.itc.it
3ITC-IRST, Centro per la Ricerca Scientifica e Tecnologica, 38050 Trento, Italy. E-mail: serafini@itc.it

We propose a framework, called OM pairs, for the formalization of metareasoning. OM pairs allow us to generate deductively pairs composed of an object theory and a metatheory related via a so called reflection principle. This is done by imposing, via appropriate reflection rules, the relation we want to hold between the object theory and the metatheory. In this paper we concentrate on the proof theory of OM pairs. We study them from various points of view: we compare the strength of the object theory and the metatheories generated by different combination of reflection rules; for each combination we characterize the object theory and metatheory, both axiomatically (when possible), and by means of fix-point equations. Finally we present four important case studies.

Keywords: Metatheory; reflection; contextual reasoning

Table of Contents   Full-Text PDF (426 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement