A Sequent Calculus for Intuitionistic Default Logic 

by Uwe Egly and Hans Tompits 
Technische Universität Wien, Austria 

Abstract 

Abstract Current research on non-monotonic reasoning shows growing interest on implementation 
details, so the need for concrete calculi formalizing non-monotonic logics is clearly recognized. 
On the other hand, there is also an increased number of works combining intuitionistic logic with 
various kinds of non-monotonic formalisms. As a case in point, intuitionistic versions of both de-
fault and autoepistemic logics have been proposed, and tight connections between intuitionistic 
logic and logic programs (or deductive databases) using hypothetical inferences have been estab-
lished.

In this paper, we present a sequent calculus for default reasoning in the style of Bonatti with intu-
itionistic logic as the underlying logical structure. In contrast to other proposals, Bonatti's tech-
nique allows a very simple and intuitive specification of the calculus, making it an ideal tool for 
implementation purposes.