Automating Reasoning with Standpoint Logic via Nested Sequents

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelProceedings of the 19th International Conference on the Principles of Knowledge Representation and Reasoning (KR'22)
Redakteure/-innenGabriele Kern-Isberner, Gerhard Lakemeyer, Thomas Meyer
Herausgeber (Verlag)IJCAI Organization
Seiten257–266
Seitenumfang10
PublikationsstatusVeröffentlicht - 2022
Peer-Review-StatusJa

Externe IDs

ORCID /0000-0003-3214-0828/work/173054736
Mendeley 33c49700-7d17-331f-94e9-af40808cfcc9
unpaywall 10.24963/kr.2022/26