Automating Reasoning with Standpoint Logic via Nested Sequents
- URL: http://arxiv.org/abs/2205.02749v1
- Date: Thu, 5 May 2022 16:27:57 GMT
- Title: Automating Reasoning with Standpoint Logic via Nested Sequents
- Authors: Tim S. Lyon and Luc\'ia G\'omez \'Alvarez
- Abstract summary: Standpoint logic advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints.
We show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- 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.
Related papers
- $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof [0.0]
Classifying languages according to the expressiveness of grammars able to generate them is a fundamental problem in computational linguistics.
This paper analyses the existing proofs from the computational and the proof-theoretical point of views systematically studying whether each proof can lead to a verified (i.e., checked by a proof assistant) algorithm parsing balanced languages via MCFGs.
arXiv Detail & Related papers (2024-05-15T14:51:11Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity.
We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points.
We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
arXiv Detail & Related papers (2024-02-14T05:57:58Z) - Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving [0.0]
We propose a framework for completing incomplete conjectures and incomplete proofs.
The framework can turn a conjecture with missing assumptions into a proper theorem.
Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof.
arXiv Detail & Related papers (2024-01-22T12:49:08Z) - Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm.
Prove-It is unique in its ability to express sophisticated mathematical statements, including statements about quantum circuits.
arXiv Detail & Related papers (2023-04-05T01:21:00Z) - Logical Satisfiability of Counterfactuals for Faithful Explanations in
NLI [60.142926537264714]
We introduce the methodology of Faithfulness-through-Counterfactuals.
It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation.
It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
arXiv Detail & Related papers (2022-05-25T03:40:59Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
We present a novel stepwise method NLProofS (Natural Language Proof Search)
NLProofS learns to generate relevant steps conditioning on the hypothesis.
It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
arXiv Detail & Related papers (2022-05-25T02:22:30Z) - Logical Credal Networks [87.25387518070411]
This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability.
We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
arXiv Detail & Related papers (2021-09-25T00:00:47Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules.
A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer.
In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
arXiv Detail & Related papers (2021-06-02T17:58:35Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant.
Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps.
Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
arXiv Detail & Related papers (2020-12-20T18:15:12Z) - Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
We give a sound and strongly complete axiomatization that can be parametrized to cover essentially every real-valued logic.
Our class of sentences are very rich, and each describes a set of possible real values for a collection of formulas of the real-valued logic.
arXiv Detail & Related papers (2020-08-06T02:13:11Z) - Understanding the QuickXPlain Algorithm: Simple Explanation and Formal
Proof [0.0]
This paper presents a proof of correctness of Ulrich Junker's QuickXPlain algorithm.
It can be used as a guidance for proving other algorithms.
It also provides the possibility of providing "gapless" correctness of systems that rely on results computed by QuickXPlain.
arXiv Detail & Related papers (2020-01-07T01:37:41Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.