Abstract
We study the question of when a given set of derivable rules in some basic analytic propositional sequent calculus forms itself an analytic calculus. First, a general syntactic criterion for analyticity in the family of pure sequent calculi is presented. Next, given a basic calculus admitting this criterion, we provide a method to construct weaker pure calculi by collecting simple derivable rules of the basic calculus. The obtained calculi are analytic-by-construction. While the criterion and the method are completely syntactic, our proofs are semantic, based on interpretation of sequent calculi via non-deterministic valuation functions. In particular, this method captures calculi for a wide variety of paraconsistent logics, as well as some extensions of Gurevich and Neeman’s primal infon logic.
This research was supported by The Israel Science Foundation (grant no. 280-10).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Anderson, A.R., Belnap, N.D.: Entailment: The Logic of Relevance and Neccessity, vol. I. Princeton University Press (1975)
Avron, A.: Simple consequence relations. Inf. Comput. 92(1), 105–139 (1991)
Avron, A., Konikowska, B., Zamansky, A.: Modular construction of cut-free sequent calculi for paraconsistent logics. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer science (LICS), pp. 85–94 (2012)
Avron, A., Lev, I.: Non-deterministic multiple-valued structures. Journal of Logic and Computation 15(3), 241–261 (2005)
Beklemishev, L., Gurevich, Y.: Propositional primal logic with disjunction. Journal of Logic and Computation 24(1), 257–282 (2014)
Béziau, J.-Y.: Sequents and bivaluations. Logique et Analyse 44(176), 373–394 (2001)
Cotrini, C., Gurevich, Y.: Basic primal infon logic. Journal of Logic and Computation (2013)
Kamide, N.: A hierarchy of weak double negations. Studia Logica 101(6), 1277–1297 (2013)
Lahav, O., Avron, A.: A unified semantic framework for fully structural propositional sequent systems. ACM Trans. Comput. Logic 27, 1–33 (2013)
Lahav, O., Zohar, Y.: Sat-based decision procedure for analytic pure sequent calculi. To appear in Proceedings of the 7th International Joint Conference on Automated Reasoning, IJCAR (2014)
Miller, D., Pimentel, E.: A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science 474(0), 98–116 (2013)
Sette, A.M.: On the propositional calculus P1. Mathematica Japonicae 18(13), 173–180 (1973)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lahav, O., Zohar, Y. (2014). On the Construction of Analytic Sequent Calculi for Sub-classical Logics. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2014. Lecture Notes in Computer Science, vol 8652. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44145-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-44145-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44144-2
Online ISBN: 978-3-662-44145-9
eBook Packages: Computer ScienceComputer Science (R0)