# Sequent-Type Proof Systems for Three-Valued Default Logic

## TL;DR

This paper develops sequent calculus systems for a three-valued default logic variant based on Łukasiewicz logic, enabling formal analysis of brave and skeptical reasoning in this nonmonotonic logic framework.

## Contribution

It introduces sequent calculi tailored for Radzikowska's three-valued default logic, addressing previous representational limitations and formalizing reasoning processes.

## Key findings

- Axiomatization of brave reasoning in the new calculus
- Axiomatization of skeptical reasoning in the new calculus
- Inclusion of a calculus for invalid formulas and consistency conditions

## Abstract

Sequent-type proof systems constitute an important and widely-used class of calculi well-suited for analysing proof search. In my master's thesis, I introduce sequent-type calculi for a variant of default logic employing \Lukasiewicz's three-valued logic as the underlying base logic. This version of default logic has been introduced by Radzikowska addressing some representational shortcomings of standard default logic. More specifically, the calculi discussed in my thesis axiomatise brave and skeptical reasoning for this version of default logic, respectively following the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti and Olivetti, which employ a complementary calculus for axiomatising invalid formulas, taking care of expressing the consistency condition of defaults.