We propose a framework, called OM pairs, for the formalization of meta-reasoning. OM pairs allow us to generate deductively pairs composed od an object theory and a meta theory 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 meta theory. In this paper we concentrate on th proof theory of OM pairs. We study them from various points of view: we compare the strength of the object and the meta theories generated by different combination of reflection rules; for each combination we characterize the object theory and meta theory, both axiomatically (when possible), and by means of fix-point equations. Finally we study four important case studies
A Foundation for Metareasoning Part I: The Proof Theory
Giunchiglia, Fausto;Serafini, Luciano
2002-01-01
Abstract
We propose a framework, called OM pairs, for the formalization of meta-reasoning. OM pairs allow us to generate deductively pairs composed od an object theory and a meta theory 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 meta theory. In this paper we concentrate on th proof theory of OM pairs. We study them from various points of view: we compare the strength of the object and the meta theories generated by different combination of reflection rules; for each combination we characterize the object theory and meta theory, both axiomatically (when possible), and by means of fix-point equations. Finally we study four important case studiesI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
