When reasoning with implicitly defined contexts or theories, a general notion of context is more appropriate than classical uses of reflection rules. Proofs in a multicontext framework can still be carryed out by switching to a context, reasonoing within it, an exporting the results. Context switching however does not correspond to reflection or reification but involves changing the level of nesting of theories within another theory. We introduce a generalized rule for proof in context and a convnient notation to express nesting of contexts, which allows us to perform reasoning in and across contexts in a safe and natural way.
Building Proofs in Context
ATTARDI, GIUSEPPE;SIMI, MARIA
1994-01-01
Abstract
When reasoning with implicitly defined contexts or theories, a general notion of context is more appropriate than classical uses of reflection rules. Proofs in a multicontext framework can still be carryed out by switching to a context, reasonoing within it, an exporting the results. Context switching however does not correspond to reflection or reification but involves changing the level of nesting of theories within another theory. We introduce a generalized rule for proof in context and a convnient notation to express nesting of contexts, which allows us to perform reasoning in and across contexts in a safe and natural way.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.
