A tableau prover for domain minimization
type: Item
instance of: scholarly article
title: A tableau prover for domain minimization
zbMATH Open document ID: 0815.03004
DOI: 10.1007/BF00881950
author: Sven Lorenz
published in: Journal of Automated Reasoning
publication date: 1995-02-22T00:00:00Z
review text: Domain minimization is a form of nonmonotonic reasoning that, roughly speaking, expresses the conjecture that the known entities are all there are. McCarthy suggested a Domain Circumscription Schema which relates a formula \(\varphi\) with a second-order formula \(\varphi'\) that adds the information to \(\varphi\) that there are no other entities in the domain than the known ones. Minimal entailment is an entailment relation that takes into account the domain minimization. As a syntactic calculus for minimal entailment, Hintikka has proposed a variation of a tableau calculus with a modified \(\delta\)-rule. The \(\delta\)-rule instantiates existentially quantified variables with new Skolem constants. The modified \(\delta\)-rule splits the current branch in the tableaux by adding the cases that the existentially quantified entity is equal to one of the already known constants (there are no function symbols allowed in this system). In the paper it is shown that Hintikka's mini-consequence is not well behaved because equivalent but syntactically different formulae may give different results. It is shown that a slight modification of Hintikka's modified \(\delta\)-rule overcomes this problem. This modified mini- consequence relation is in fact equivalent to domain circumscription. The method is implemented in a tableau theorem prover called MiniTab. MiniTab works for order-sorted predicate logic and allows for function symbols in those sorts whose domains are not to be minimized. In this way the problem of having no function symbols is partially overcome.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 724136
zbMATH Keywords: nonmonotonic logic
zbMATH Keywords: tableau theorem proving
zbMATH Keywords: domain minimization
zbMATH Keywords: minimal entailment
zbMATH Keywords: domain circumscription
reviewed by: Hans Jürgen Ohlbach
MaRDI profile type: Publication
cites work: The mathematics of non-monotonic reasoning
cites work: Formalizing nonmonotonic reasoning systems
cites work: Q3996619
cites work: A circumscriptive theorem prover
cites work: The liberalized \(\delta\)-rule in free variable semantic tableaux
cites work: Circumscription - a form of non-monotonic reasoning
cites work: On the relative merits of path dissolution and the method of analytic tableaux
cites work: Tableaux and sequent calculus for minimal entailment
cites work: An algorithm to compute circumscription
cites work: First-order syntactic characterizations of minimal entailment, domain- minimal entailment, and Herbrand entailment
full work available at URL: https://doi.org/10.1007/bf00881950
OpenAlex ID: W2081898972
description: scientific article; zbMATH DE number 724136