English

Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning

Logic in Computer Science 2007-05-23 v1 Artificial Intelligence

Abstract

We present tableau calculi for some logics of nonmonotonic reasoning, as defined by Kraus, Lehmann and Magidor. 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.

Keywords

Cite

@article{arxiv.cs/0611046,
  title  = {Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning},
  author = {Laura Giordano and Valentina Gliozzi and Nicola Olivetti and Gian Luca Pozzato},
  journal= {arXiv preprint arXiv:cs/0611046},
  year   = {2007}
}

Comments

54 pages + appendix with proofs