Analytic sequent calculi with nonlogical axioms

A. Sakharov

Zapiski Nauchnykh Seminarov POMI, Representation theory, dynamical systems, combinatorial methods. Part XXXV, Tome 528 (2023), pp. 166-194

Résumé

This paper investigates a variety of sequent calculi including substructural ones and calculi with equality that can be used for characterizing AI systems. These calculi have introduction inference rules for logical connectives and contain nonlogical axioms. Nonlogical axioms represent domain knowledge. Derivations in these calculi can be restricted to a normal form and to an ordered form. Inference rules are constrained in these forms. It is proved that these calculi are analytic. Infinite branching can be avoided in inference procedures for these calculi.

Bibliographie

[1] O Arieli, Ch. Straßer, “Sequent-based logical argumentation”, Argument Computation, 6:1 (2015), 73–99

[2] A. Avron, “Hypersequents, logical consequence and intermediate logics for concurrency”, Ann. Math. Artif. Intel., 4 (1991), 225–248

[3] M. Baaz, A. Leitsch, Methods of Cut-elimination, Springer Science Business Media, 34, 2011

[4] E. Beffara, Introduction to linear logic, HAL CCSD, cel-01144229, 2013

[5] Chang, Chin-Liang and Lee, Richard Char-Tung, Symbolic logic and mechanical theorem proving, Academic press, 1973

[6] A. Ciabattoni, T. Lang, R. Ramanayake, “Bounded sequent calculi for non-classical logics via hypersequents”, Automated Reasoning with Analytic Tableaux and Related Methods, 2019, 94–110

[7] A. Ciabattoni, T. Lang, R. Ramanayake, “Bounded-analytic sequent calculi and embeddings for hypersequent logics”, J. Symb. Logic, 86:2 (2021), 635–668

[8] A. Ciabattoni, L. Straßburger, K. Terui, “Expanding the realm of systematic proof theory”, International Workshop on Computer Science Logic, 2009, 163–178

[9] P. Cintula, D. Diaconescu, G. Metcalfe, “Skolemization and Herbrand theorems for lattice-valued logics”, Theor. Comput. Sci., 768 (2019), 54–75

[10] M. Fitting, “Subformula results in some propositional modal logics”, Studia Logica: An International Journal for Symbolic Logic, 37:4 (1978), 387–391

[11] A. Indrzejczak, “Simple decision procedure for S5 in standard cut-free sequent calculus”, Bulletin of the Section of Logic, 45:2 (2016), 125–140

[12] JELIA, European Conference on Logics in Artificial Intelligence (Accessed: August 1, 2023) https://www.jelia.eu/

[13] S. C. Kleene, “Permutability of inferences in Gentzens calculi LK and LJ”, Bulletin Of The American Mathematical Society, 57:6 (1951), 485–485

[14] L. Kovács, A. Voronkov, “First-order theorem proving and Vampire”, International Conference on Computer Aided Verification, 2013, 1–35

[15] T. Kowalski, H. Ono, “Analytic cut and interpolation for bi-intuitionistic logic”, The Review of Symbolic Logic, 10:2 (2017), 259–283

[16] O. Lahav, Y. Zohar, “On the construction of analytic sequent calculi for sub-classical logics”, International Workshop on Logic, Language, Information, and Computation, 2014, 206–220

[17] O. Lahav, Y. Zohar, “Pure Sequent Calculi: Analyticity and Decision Procedure”, ACM Transactions on Computational Logic (TOCL), 20:3 (2019), 1–38

[18] A. Leitsch, N. Peltier, D. Weller, “CERES for first-order schemata”, J. Logic and Computation, 27:7 (2017), 1897–1954

[19] B. Lellmann, D. Pattinson, “Cut elimination for shallow modal logics”, Automated Reasoning with Analytic Tableaux and Related Methods, 2011, 211–225

[20] C. Liang, D. Miller, “A focused approach to combining logics”, Annals of Pure and Applied Logic, 162:9 (2011), 679–697

[21] S. Marin, D. Miller, E. Pimentel, M. Volpe, “From axioms to synthetic inference rules via focusing”, Annals of Pure and Applied Logic, 173:5 (2022), 103091

[22] W. McCune, Otter 3.3 reference manual and guide, Argonne National Lab., 2003

[23] S. Negri, J. Von Plato, Structural proof theory, Cambridge University Press, 2001

[24] H. Nishimura, “A study of some tense logics by Gentzen's sequential method”, Publications of the Research Institute for Mathematical Sciences, 16:2 (1980), 343–353

[25] L. Pinto, T. Uustalu, “A proof-theoretic study of bi-intuitionistic propositional sequent calculus”, Journal of Logic and Computation, 28:1 (2018), 165–202

[26] Logics for New-Generation AI, College Publications (Accessed: August 1, 2023) https://www.collegepublications.co.uk/LNGAI/

[27] J. Rasga, “Sufficient conditions for cut elimination with complexity analysis”, Annals of Pure and Applied Logic, 149:1–3 (2007), 81–99

[28] S. Russell, P. Norvig, Artificial Intelligence: A Modern Approach, 3rd, Prentice Hall Press, 2009

[29] A. Sakharov, “A Logical Characterization of Evaluable Knowledge Bases”, 14th International Conference on Agents and Artificial Intelligence, 2022, 681–688

[30] A. Sakharov, “A Normal Form of Derivations for Quantifier-Free Sequent Calculi With Nonlogical Axioms”, Polynomial Computer Algebra, 2023, 98–103

[31] W. Sieg, B. Kauffmann, Unification for quantified formulae, Carnegie Mellon, Department of Philosophy, 1993

[32] M. E. Szabo (ed), The collected papers of Gerhard Gentzen, North-Holland, 1969

[33] M. Takano, “Subformula property as a substitute for cut-elimination in modal propositional logics”, Mathmatica Japonica, 37 (1992), 1129–1145

[34] T. Tammet, “Resolution, inverse method and the sequent calculus”, Kurt Gödel Colloquium, 1289, 1997, 65–83

[35] A. Voronkov, “Theorem proving in non-standard logics based on the inverse method”, 11th International Conference on Automated Deduction, 1992, 648–662

[36] Ch. Walther, “Many-sorted unification”, J. of the ACM (JACM), 35:1 (1988), 1–17

[37] H. Wansing, “Sequent systems for modal logics”, Handbook of Philosophical Logic, v. 8, 2002, 61–145

[38] A. Zamansky, A. Avron, “Cut-elimination and quantification in canonical systems”, Studia Logica, 82 (2006), 157–176