A tableau prover for domain minimization (Q1344878)

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.