Tableaux and sequent calculus for minimal entailment
type: Item
instance of: scholarly article
title: Tableaux and sequent calculus for minimal entailment
zbMATH Open document ID: 0795.03033
DOI: 10.1007/BF00247828
author: N. Olivetti
published in: Journal of Automated Reasoning
publication date: 1994-09-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B60
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 444936
zbMATH Keywords: formalization of the nonmonotonic minimal entailment relation
zbMATH Keywords: semantic tableaux
zbMATH Keywords: nonmonotonic reasoning
zbMATH Keywords: Gentzen's sequent calculus
zbMATH Keywords: dynamic minimal entailment
zbMATH Keywords: Variable Circumscription
zbMATH Keywords: Extended Closed World Assumption
reviewed by: Cees Witteveen
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00247828
OpenAlex ID: W2014810198
description: scientific article; zbMATH DE number 444936