A metatheory of a mechanized object theory |
| |
Authors: | Fausto Giunchiglia Paolo Traverso |
| |
Affiliation: | aMechanized Reasoning Group, IRST — Istituto per la Ricerca Scientifica e Tecnologica, 38050 Povo, Trento, Italy;bMechanized Reasoning Group, DISA, University of Trento, Via Imana 5, Trento, Italy |
| |
Abstract: | In this paper we propose a metatheory, MT, which represents the computation which implements its object theory, OT, and, in particular, the computation which implements deduction in OT. To emphasize this fact we say that MT is a metatheory of a mechanized object theory. MT has some “unusual” properties, e.g. it explicitly represents failure in the application of inference rules, and the fact that large amounts of the code implementing OT are partial, i.e. they work only for a limited class of inputs. These properties allow us to use MT to express and prove tactics, i.e. expressions which specify how to compose possibly failing applications of inference rules, to interpret them procedurally to assert theorems in OT, to compile them into the system implementation code, and, finally, to generate MT automatically from the system code. The definition of MT is part of a larger project which aims at the implementation of self-reflective systems, i.e. systems which are able to introspect their own code, to reason about it and, possibly, to extend or modify it. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|