TY - CONF T1 - Constructive contextual modal judgments for reasoning from open assumptions T2 - Proceedings of the Computability in Europe 2010 Conference Y1 - 2010 A1 - Primiero, Giuseppe ED - Ferreira, F ED - Guerra, H ED - Mayordomo, E ED - Rasga, J AB -

Dependent type theories using a structural notion of context are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. In particular, types with modalities are already used for distributed and staged computation. This paper introduces a type system extended with judgmental modalities internalizing epistemically different modes of correctness to explore a calculus of provability from refutable assumptions.

JA - Proceedings of the Computability in Europe 2010 Conference PB - Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores ER -