Sequent calculi for default and autoepistemic logics

Two sequent calculi, for default logic and autoepistemic logic, will be introduced in this paper. The main goal is improving our proof-theoretic understanding of non-monotonic formalisms. Credulous reasoning will be axiomatized for the first time, and a link will be established between non-monotonic reasoning and the branch of logic devoted to axiomatic rejection methods. In this way, some aspects of non-monotonic reasoning, which were not explicitly axiomatized in previous approaches, will be completely characterized in proof-theoretic terms.