Abstract
We identify a wide family of analytic sequent calculi for propositional non-classical logics whose derivability problem can be uniformly reduced to SAT. The proposed reduction is based on interpreting these calculi using non-deterministic semantics. Its time complexity is polynomial, and, in fact, linear for a useful subfamily. We further study an extension of such calculi with Next operators, and show that this extension preserves analyticity and is subject to a similar reduction to SAT. A particular interesting instance of these results is a HORNSAT-based linear-time decision procedure for Gurevich and Neeman’s primal infon logic and several natural extensions of it.
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
References
Avron, A.: Simple consequence relations. Inf. Comput. 92(1), 105–139 (1991)
Avron, A.: Classical gentzen-type methods in propositional many-valued logics. In: Fitting, M., Orłowska, E. (eds.) Beyond Two: Theory and Applications of Multiple-Valued Logic. Studies in Fuzziness and Soft Computing, vol. 114, pp. 117–155. Physica-Verlag HD (2003)
Avron, A., Konikowska, B., Zamansky, A.: Modular construction of cut-free sequent calculi for paraconsistent logics. In: 2012 27th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 85–94 (2012)
Avron, A., Konikowska, B., Zamansky, A.: Cut-free sequent calculi for c-systems with generalized finite-valued semantics. Journal of Logic and Computation 23(3), 517–540 (2013)
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 (2012)
Béziau, J.-Y.: Sequents and bivaluations. Logique et Analyse 44(176), 373–394 (2001)
Bjørner, N., de Caso, G., Gurevich, Y.: From primal infon logic with individual variables to datalog. In: Erdem, E., Lee, J., Lierler, Y., Pearce, D. (eds.) Correct Reasoning. LNCS, vol. 7265, pp. 72–86. Springer, Heidelberg (2012)
Blass, A., Gurevich, Y.: Abstract hilbertian deductive systems, infon logic, and datalog. Information and Computation 231, 21–37 (2013)
Cai, J., Paige, R.: Using multiset discrimination to solve language processing problems without hashing. Theoretical Computer Science 145(12), 189–228 (1995)
Cotrini, C., Gurevich, Y.: Basic primal infon logic. Journal of Logic and Computation (2013)
Degtyarev, A., Voronkov, A.: The inverse method. In: Handbook of Automated Reasoning, vol. 1, pp. 179–272 (2001)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. The Journal of Logic Programming 1(3), 267–284 (1984)
Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation. Foundations of Artificial Intelligence, vol. 3, pp. 89–134. Elsevier (2008)
Gurevich, Y., Neeman, I.: Logic of infons: The propositional case. ACM Trans. Comput. Logic 9, 1–9 (2011)
Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Mathematical Logic Quarterly 33(5), 423–432 (1987)
Kowalski, R.: Logic for Problem-solving. North-Holland Publishing Co., Amsterdam (1986)
Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 8, pp. 61–145. Springer (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Lahav, O., Zohar, Y. (2014). SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-08587-6_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08586-9
Online ISBN: 978-3-319-08587-6
eBook Packages: Computer ScienceComputer Science (R0)