Proof Search on Bilateralist Judgments over Non-deterministic Semantics

DOI10.1007/978-3-030-86059-2_8MaRDI QIDQ6373052arXivFDO

Authors Vitor Greati, Sérgio Marcelino, João Marcos

Publication date 17 July 2021

Published in arXiv

Full work available at URL https://doi.org/10.1007/978-3-030-86059-2_8

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

arXiv classification

cs.LOmath.LO

Abstract: The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to reason over bilateralist judgments using symmetrical two-dimensional analytical Hilbert-style calculi. We also provide a proof-search algorithm for finite analytic calculi that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned calculus.

This page was built for publication: Proof Search on Bilateralist Judgments over Non-deterministic Semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6373052)