### Semi-analytic tableaux for propositional normal modal logics with application to nonmonotonicity

#### Abstract

The propositional monotonic modal logics K45, K45D, S4.2, S4R and S4F elegantly capture the semantics o f many current nonmonotonic formalisms as long as (strong) deducibility of A from a theory I', A, allows the use of necessitation on the members of F. This is usually forbidden in modal logic where F is required to be empty, resulting in a weaker notion of deducibility.

Recently, Marek, Schwarz and Truszczyliski have given algorithms to compute the stable expansions of a finite theory I' in various such nonmonotonic formalisms. Their algorithms assume the existence of procedures for deciding (strong) deducibility in these monotonic modal logics and consequently such decision procedures are important for automating nonmonotonic deduction.

We first give a sound, (weakly) complete and cut-free, semi-analytic tableau calculus for monotonic S4R, thus extending the cut elimination results of Schwarz for monotonic K45 and K45D. We then give sound and complete semi-analytic tableau calculi for monotonic K45, K45D, S4.2 and S4F by adding an (analytic) cut rule. The proofs of tableau completeness yield a deterministic satisfiability test to determine theoremhood (weak deducibility), 1—, A, because all proofs are constructive. The techniques are due to Hintikka and Rautenberg. We then show that the tableau calculi extend trivially to handle (strong) deducibility, F I— A, for finite r.

Using a general theorem due to Rautenberg we also obtain the (weak) interpolation theorem for K45, K45D, S4.2 and S4R.

Recently, Marek, Schwarz and Truszczyliski have given algorithms to compute the stable expansions of a finite theory I' in various such nonmonotonic formalisms. Their algorithms assume the existence of procedures for deciding (strong) deducibility in these monotonic modal logics and consequently such decision procedures are important for automating nonmonotonic deduction.

We first give a sound, (weakly) complete and cut-free, semi-analytic tableau calculus for monotonic S4R, thus extending the cut elimination results of Schwarz for monotonic K45 and K45D. We then give sound and complete semi-analytic tableau calculi for monotonic K45, K45D, S4.2 and S4F by adding an (analytic) cut rule. The proofs of tableau completeness yield a deterministic satisfiability test to determine theoremhood (weak deducibility), 1—, A, because all proofs are constructive. The techniques are due to Hintikka and Rautenberg. We then show that the tableau calculi extend trivially to handle (strong) deducibility, F I— A, for finite r.

Using a general theorem due to Rautenberg we also obtain the (weak) interpolation theorem for K45, K45D, S4.2 and S4R.

#### Full Text:

PDF### Refbacks

- There are currently no refbacks.