Automating Reasoning with Standpoint Logic via Nested Sequents
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
Abstract
Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multiperspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics-proof systems that manipulate trees whose nodes are multisets of formulae-and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in the context of nested sequents, referred to as coloring, which consists of taking a formula as input, guessing a certain coloring of its subformulae, and then running proof-search in a nested sequent calculus on the colored input. Our technique lets us decide the validity of standpoint formulae in CoNP since proof-search only produces a partial proof relative to each permitted coloring of the input. We show how all partial proofs can be fused together to construct a complete proof when the input is valid, and how certain partial proofs can be transformed into a counter-model when the input is invalid. These “certificates” (i.e. proofs and counter-models) serve as explanations of the (in)validity of the input.
Details
Originalsprache | Englisch |
---|---|
Titel | Proceedings of the 19th International Conference on the Principles of Knowledge Representation and Reasoning (KR'22) |
Redakteure/-innen | Gabriele Kern-Isberner, Gerhard Lakemeyer, Thomas Meyer |
Herausgeber (Verlag) | IJCAI Organization |
Seiten | 257–266 |
Seitenumfang | 10 |
Publikationsstatus | Veröffentlicht - 2022 |
Peer-Review-Status | Ja |
Externe IDs
ORCID | /0000-0003-3214-0828/work/173054736 |
---|---|
Mendeley | 33c49700-7d17-331f-94e9-af40808cfcc9 |
unpaywall | 10.24963/kr.2022/26 |