Tableaux and sequent calculus for minimal entailment (Q688552)

Using standard deduction methods, it is shown that a formalization of the nonmonotonic (propositional) minimal entailment relation can be given. The idea of minimal entailment plays a significant role in some major approaches to nonmonotonic reasoning as Circumscription and Closed World Assumption reasoning. Instead of developing nonstandard tools as has been the case in these latter approaches, a slight adaptation of two standard methods (semantic tableaux and Gentzen's sequent calculus) is presented to capture preferential and minimal entailment relations. Correctness and completeness of the methods with respect to the entailment relations are shown. An extension to so-called dynamic minimal entailment is presented to point out the relation with Variable Circumscription and the Extended Closed World Assumption. The extension to the first-order case is discussed.