Automated deduction procedures for modal logics, and related decidable fragments of first-order logic, are used in many real-world applications. A popular way of obtaining decision procedures for these logics is to base them on semantic tableau calculi. We focus on calculi that use unification, instead of the more widely employed approach of generating ground instantiations over the course of a derivation. The most common type of tableaux with unification are so-called free-variable tableaux, where variables are treated as global to the entire tableau. A long-standing open problem for procedures based on free-variable tableaux is how to ensure fairness, in the sense that "equivalent" applications of the closure rule are prevented from being done over and over again. Some solutions such as using depth-first iterative deepening are known, but those are unnecessary in theory, and not very efficient in practice. This is a main reason why there are hardly any decision procedures for modal logics based on free-variable tableaux. In this thesis, we review existing work on incorporating unification into first-order and modal tableau procedures, show how the closure fairness problem arises, and discuss existing solutions to it. For the first-order case, we outline a calculus which addresses the closure fairness problem. As opposed to free-variable tableaux, closure fairness is much easier to achieve in disconnection tableaux and similar clausal calculi. We therefore focus on using clausal first-order tableau calculi for decidable classes, in particular the two-variable fragment. Using the so-called unrestricted blocking mechanism for enforcing termination, we present the first ground tableau decision procedure for this fragment. Even for such a ground calculus, guaranteeing that depth-first terminations terminate is highly non-trivial. We parametrise our procedure by a so-called lookahead amount, and prove that this parameter is crucial for determining whether depth-first derivations terminate or not. Extending these ideas to tableaux with unification, we specify a preliminary disconnection tableau procedure which uses a non-grounding version of the unrestricted blocking rule.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:553436 |
| Date | January 2012 |
| Creators | Reker, Hilverd Geert |
| Contributors | Schmidt, Renate |
| Publisher | University of Manchester |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | https://www.research.manchester.ac.uk/portal/en/theses/tableaubased-reasoning-for-decidable-fragments-of-firstorder-logic(f47e0c7d-399d-48c9-8745-a907c5475f7d).html |
Page generated in 0.0128 seconds