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.
%0 Journal Article
%1 Lyon2022-kz
%A Lyon, Tim S
%A Álvarez, Luc\'ıa Gómez
%D 2022
%I arXiv
%K
%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 = {},
publisher = {arXiv},
timestamp = {2024-09-10T15:15:57.000+0200},
title = {Automating reasoning with standpoint logic via nested sequents},
year = 2022
}
