Pedagogical Natural Deduction Systems: the Propositional Case
Дата
Авторы
Colson,Loïc
Michel,David
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
This paper introduces the notion of pedagogical natural deduction systems, which are natural deduction systems with the following additional constraint: all hypotheses made in a proof must be motivated by some example. It is established that such systems are negationless. The expressive power of the pedagogical version of some propositional calculi are studied.
Ключевые слова
mathematical logic , negationless mathematics , constructive mathematics , natural deduction , typed λ-calculus