Logique et Analyse

TitleA contextual type theory with judgemental modalities for reasoning from open assumptions
Publication TypeJournal Article
Year of Publication2012
AuthorsPrimiero, G
JournalLogique et Analyse

Contextual type theories are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. The combination of a constructive language with a modal extension of contexts appears crucial to explore the attractive idea of a type-theoretical calculus of provability from refutable assumptions for non-monotonic reasoning. This paper introduces such a language: the modal operators are meant to internalize two different modes of correctness, respectively with necessity as the standard notion of constructive verification and possibility as provability up to refutation of contextual conditions.

Citation Key3094113
Download PDF (Author PDF)