Automating Reasoning with Standpoint Logic via Nested Sequents

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-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 languageEnglish
Title of host publicationProceedings of the 19th International Conference on the Principles of Knowledge Representation and Reasoning (KR'22)
EditorsGabriele Kern-Isberner, Gerhard Lakemeyer, Thomas Meyer
PublisherIJCAI Organization
Pages257–266
Number of pages10
Publication statusPublished - 2022
Peer-reviewedYes

External IDs

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