Strongly Analytic Calculi for KLM Logics with SMT-Based Prover
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.
Agata Ciabattoni
Professor of Non-Classical Logics in Computer Science
Agata Ciabattoni is a full professor of non-classical logics in computer science. She is an expert in proof theory for non-classical logics and their applications in various fields. Among other things, she has been investigating proof theory for deontic logic, its applications in AI, connections to legal reasoning, and formalisation of the deontic reasoning of the Mı̄māmsā school of Indian philosophy.