%0 Journal Article %1 Lyon2022-kz %A Lyon, Tim S %A Álvarez, Luc\'ıa Gómez %D 2022 %I arXiv %K topic_knowledge %T Automating reasoning with standpoint logic via nested sequents %X Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective 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.

@article{Lyon2022-kz, abstract = {Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective 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.}, added-at = {2024-09-10T11:56:37.000+0200}, author = {Lyon, Tim S and {\'A}lvarez, Luc{\'\i}a G{\'o}mez}, biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/24225f14c8986964f731b6006294dc3e1/scadsfct}, interhash = {d4db53726f04ede2866cfeaa2e36c412}, intrahash = {4225f14c8986964f731b6006294dc3e1}, keywords = {topic_knowledge}, publisher = {arXiv}, timestamp = {2024-11-28T17:41:12.000+0100}, title = {Automating reasoning with standpoint logic via nested sequents}, year = 2022 }