Premium
Computational reflection via mechanized logical deduction
Author(s) -
Cimatti Alessandro,
Traverso Paolo
Publication year - 1996
Publication title -
international journal of intelligent systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.291
H-Index - 87
eISSN - 1098-111X
pISSN - 0884-8173
DOI - 10.1002/(sici)1098-111x(199605)11:5<279::aid-int3>3.0.co;2-l
Subject(s) - correctness , automated theorem proving , computer science , reflection (computer programming) , gas meter prover , extension (predicate logic) , computation , feature (linguistics) , logical conjunction , calculus (dental) , programming language , algorithm , theoretical computer science , mathematics , mathematical proof , medicine , linguistics , philosophy , geometry , dentistry
In this article, we show how a system for automated deduction can be given computational reflection, i.e., can affect its own computation mechanism, by using the very same machinery implementing logical deduction. This feature, which we call computational reflection via mechanized logical deduction, provides both theoretical and practical advantages. First, the theorem prover can inspect, extend, and modify its own underlying theorem‐proving strategies automatically. Second, mechanized logical deduction can be used to reason about the ways these strategies can be extended and modified and to prove correctness statements. This opens up the possibility of building systems that are able to perform correct and safe, reflective self‐extension and self‐modification. © 1996 John Wiley & Sons, Inc.