CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWhen reasoning about reasoning one often needs to carry out some proof steps within a different theory and to lift the conclusions back to the original theory. The deductive rules to carry out these steps involve different reflection principles or some other notion of proof in context. Reflection principles have to be carefully restricted in order to avoid paradodex. Such restrictions however. we show that proof in context can replace the most common uses of reflection prionciples. We introduce a generalized rule for proof in context and a convenient notation to express nesting of contexts, which allows us to carry out resanong about reasoning in a safe and natural way.
| Titolo: | Proofs in context |
| Autori: | ATTARDI G.; SIMI M |
| Autori interni: | |
| Anno del prodotto: | 1994 |
| Abstract: | When reasoning about reasoning one often needs to carry out some proof steps within a different theory and to lift the conclusions back to the original theory. The deductive rules to carry out these steps involve different reflection principles or some other notion of proof in context. Reflection principles have to be carefully restricted in order to avoid paradodex. Such restrictions however. we show that proof in context can replace the most common uses of reflection prionciples. We introduce a generalized rule for proof in context and a convenient notation to express nesting of contexts, which allows us to carry out resanong about reasoning in a safe and natural way. |
| Appare nelle tipologie: | 2.1 Contributo in volume (Capitolo o Saggio) |
File in questo prodotto:
http://hdl.handle.net/11568/25086
Copyright © 2021