A tableau prover for domain minimization (Q1344878)
From MaRDI portal
![]() | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A tableau prover for domain minimization |
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A tableau prover for domain minimization |
scientific article |
Statements
A tableau prover for domain minimization (English)
0 references
22 February 1995
0 references
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.
0 references
nonmonotonic logic
0 references
tableau theorem proving
0 references
domain minimization
0 references
minimal entailment
0 references
domain circumscription
0 references