Chris Groeneboer, James P. Delgrande
This paper presents an extension of the semantic tableaux approach to theorem proving for the class of normal conditional logics. These logics are based on a possible worlds semantics, but contain a binary "variable conditional" operator => instead of the usual operator for necessity. The truth of A => B depends both on the accessibility relation between worlds, and on the proposition expressed by the antecedent A. Such logics have been shown to be appropriate for representing a wide variety of commonsense assertions, including default and prototypical properties, counterfactuals, notions of obligation, and others. The approach consists in attempting to find a truth assignment which will falsify a sentence or set of sentences. If successful, then a specific falsifying truth assignment is obtained; if not, then the sentence is valid. The approach is arguably more natural and intuitive than those based on proof-theoretic methods. The approach has been proven correct with respect to determining validity in the class of normal conditional logics. In addition, the approach has been implemented and tested on a number of different conditional logics. Various heuristics have been incorporated, and the implementation, while exponential in the worst case, is shown to be reasonably efficient for a large set of test cases.