|
Abstract : |
The goal of this paper is to present and discuss a simple and rather effective tableau calculus which combines modal logics of knowledge and belief with contextual reasoning. The system is made by a multiple combination. For modal proofs, it labels formulae as prefixed tableaux but uses message (knowledge) passing rules similar to those of sequentlike tableaux. For contextual deduction, it merges the metalevel information of the labelling system used by Multicontextual Languages with that used by Labelled Deductive Systems. Its semantics is also simple and intuitively based on a property of Kripke models. The resulting calculus (k-Clusters Tableaux) is effective for automated proofs, applicable to a wide range of modal logics, and adaptable to many search heuristics. It is also easy to use for proof presentation since its rule have intuitive epistemic interpretation (how knowledge and belief can be inherited up and down possible worlds). It is weak enough to satisfy a KB where two consistent modal statements may globally contradict each other (in classical logic), but strong enough to rule out an inconsistent statement. 1, |
