Analytic tableaux calculi for KLM logics of nonmonotonic reasoning
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato · ACM Transactions on Computational Logic · 2009
We present tableau calculi for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative, and rational logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. We provide a decision procedure for the logics considered and we study their complexity.