Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, and Gian Luca, Pozzato
TL;DR
This paper develops tableau calculi for various KLM nonmonotonic logics, providing decision procedures and complexity analysis, thus advancing formal reasoning methods in nonmonotonic logic systems.
Contribution
It introduces tableau calculi with modalities for KLM logics, enabling systematic reasoning and decision procedures for these nonmonotonic systems.
Findings
Decidable tableau proof procedures for all KLM logics
Complexity analysis of the reasoning procedures
Modal extensions effectively interpret conditionals
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Semantic Web and Ontologies