KR2024Proceedings of the 21st International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning

Hanoi, Vietnam. November 2-8, 2024.

Edited by
  1. Pierre Marquis,
  2. Magdalena Ortiz
  3. Maurice Pagnucco

ISSN: 2334-1033
ISBN: 978-1-956792-05-8

Sponsored by
Published by

Copyright © 2024 International Joint Conferences on Artificial Intelligence Organization

Strongly Analytic Calculi for KLM Logics with SMT-Based Prover

  1. Agata Ciabattoni(TU Wien)
  2. Clemens Eisenhofer(TU Wien)
  3. Dmitry Rozplokhas(TU Wien)
PDF
BibTeX
https://doi.org/10.24963/kr.2024/27

Keywords

  1. Non-monotonic logics-General
  2. Computational aspects of knowledge representation-General
  3. Knowledge compilation, automated reasoning, satisfiability and model counting-General

Abstract

We introduce modular calculi for the logics for nonmonotonic reasoning defined by Kraus, Lehmann, and Magidor, featuring a strengthened form of analyticity. Our calculi are used to determine the computational complexity for the logics C, CL, CM, P (and M), and fragments thereof. The calculi are encoded into SMT solvers, yielding an efficient prover with countermodel generation capabilities. Our work encompasses known results and introduces new findings, including co-NP-completeness and a more effective semantics for C.