Automating Reasoning with Standpoint Logic via Nested Sequents
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
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
Original language | English |
---|---|
Title of host publication | Proceedings of the 19th International Conference on the Principles of Knowledge Representation and Reasoning (KR'22) |
Editors | Gabriele Kern-Isberner, Gerhard Lakemeyer, Thomas Meyer |
Publisher | IJCAI Organization |
Pages | 257–266 |
Number of pages | 10 |
Publication status | Published - 2022 |
Peer-reviewed | Yes |
External IDs
ORCID | /0000-0003-3214-0828/work/173054736 |
---|---|
Mendeley | 33c49700-7d17-331f-94e9-af40808cfcc9 |
unpaywall | 10.24963/kr.2022/26 |