Proceedings

Reflective Reasoning with and between a Declarative Metatheory and the Implementation Code

Fausto Giunchiglia, Paolo Traverso

Download BibTeX Cite

Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 111-116.

Abstract

The goal of this paper is to present a theorem prover where the underlying code has been written to behave as the procedural metalevel of the object logic. We have then defined a logical declarative metatheory MT which can be put in a one-to..one relation with the code and automatically generated from it. MT is proved correct and complete in the sense that, for any object level deduction, the wff representing it is a theorem of MT, and viceversa. Such theorems can be translated back in the underlying code. This opens up the possibility of deriving control strategies automatically by metatheoretic theorem proving, of mapping them into the code and thus of extending and modifying the system itself. This seems a first step towards "really" self-reflective systems, ie. systems able to reason deductively about and modify their underlying computation mechanisms. We show that the usual logical reflection rules (so called reflection up and down) are derived inference rules of the system.

Fausto Giunchiglia, and Paolo Traverso. 1991. Reflective Reasoning with and between a Declarative Metatheory and the Implementation Code. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91. IJCAI, 111–116. https://ijcai.org/proceedings/1991/17
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards