This paper shows how a system for automated deduction can be given computational reflection, i.e. can compute about and affect its own computation mechanism, by using the very same machinery implementing logical deduction. This feature, that 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

Computational Reflection via Mechanized Logical Deduction

Cimatti, Alessandro;Traverso, Paolo
1996

Abstract

This paper shows how a system for automated deduction can be given computational reflection, i.e. can compute about and affect its own computation mechanism, by using the very same machinery implementing logical deduction. This feature, that 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
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/986
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact