Pokaż uproszczony rekord

dc.contributor.authorLeszczyńska-Jasion, Dorota
dc.contributor.authorPetrukhin, Yaroslav
dc.contributor.authorShangin, Vasilyi
dc.contributor.authorJukiewicz, Marcin
dc.date.accessioned2019-10-13T10:39:50Z
dc.date.available2019-10-13T10:39:50Z
dc.date.issued2019
dc.identifier.issn0138-0680
dc.identifier.urihttp://hdl.handle.net/11089/30606
dc.description.abstractKooi and Tamminga's correspondence analysis is a technique for designing proof systems, mostly, natural deduction and sequent systems. In this paper it is used to generate sequent calculi with invertible rules, whose only branching rule is the rule of cut. The calculi pertain to classical propositional logic and any of its fragments that may be obtained from adding a set (sets) of rules characterizing a two-argument Boolean function(s) to the negation fragment of classical propositional logic. The properties of soundness and completeness of the calculi are demonstrated. The proof of completeness is conducted by Kalmár's method. Most of the presented sequent-calculus rules have been obtained automatically, by a rule-generating algorithm implemented in Python. Correctness of the algorithm is demonstrated. This automated approach allowed us to analyse thousands of possible rules' schemes, hundreds of rules corresponding to Boolean functions, and to nd dozens of those invertible. Interestingly, the analysis revealed that the presented proof-theoretic framework provides a syntactic characteristics of such an important semantic property as functional completeness.en_GB
dc.description.sponsorshipPolish National Science Centre, grant no. 2017/26/E/HS1/00127en_GB
dc.description.sponsorshipPolish National Science Centre, grant no. 2017/25/B/HS1/01268en_GB
dc.language.isoenen_GB
dc.publisherWydawnictwo Uniwersytetu Łódzkiegoen_GB
dc.relation.ispartofseriesBulletin of the Section of Logic; 1
dc.rightsThis work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.en_GB
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0en_GB
dc.subjectcorrespondence analysisen_GB
dc.subjectinvertible rulesen_GB
dc.subjectclassical propositional logicen_GB
dc.subjectfunctional completenessen_GB
dc.subjectsequent calculusen_GB
dc.subjectautomated deductionen_GB
dc.subjectautomated rules generationen_GB
dc.titleFunctional Completeness in CPL via Correspondence Analysisen_GB
dc.typeArticleen_GB
dc.page.number45–76
dc.contributor.authorAffiliationDepartment of Logic and Cognitive Science, Adam Mickiewicz University, Poznań, Poland
dc.contributor.authorAffiliationDepartment of Logic, Faculty of Philosophy, Lomonosov Moscow State University, Moscow, Russia
dc.contributor.authorAffiliationDepartment of Logic, Faculty of Philosophy, Lomonosov Moscow State University, Moscow, Russia
dc.contributor.authorAffiliationDepartment of Logic and Cognitive Science, Adam Mickiewicz University, Poznan, Poland
dc.identifier.eissn2449-836X
dc.referencesF. G. Asenjo, A calculus of antinomies, Notre Dame Journal of Formal Logic, vol. 7, no. 1 (1966), pp. 103–105.
dc.referencesN. D. Belnap, A useful four-valued logic, Modern Uses of MultipleValued Logic, ed. by J.M. Dunn, G. Epstein. Boston: Reidel Publishing Company (1977), pp. 7–37.
dc.referencesN. D. Belnap, How a computer should think, Contemporary Aspects of Philosophy, ed. by G. Rule. Stocksfield: Oriel Press (1977), pp. 30–56.
dc.referencesS. Bonzio, J. Gil-F´erez, F. Paoli, L. Peruzzi, On Paraconsistent Weak Kleene Logic: Axiomatisation and Algebraic Analysis, Studia Logica, vol. 105, no. 2 (2017), pp. 253–297.
dc.referencesK. Doˇsen, Logical constants as punctuation marks, Notre Dame Journal of Formal Logic, vol. 30, no. 3 (1989), pp. 362–381.
dc.referencesJ. M. Dunn, Intuitive semantics for first-degree entailment and coupled trees, Philosophical Studies, vol. 29, no. 3 (1976), pp. 149–168.
dc.referencesM. Fitting, First-Order Logic and Automated Theorem Proving, New York: Springer-Verlag, 1990.
dc.referencesS. Halld´en, The Logic of Nonsense. Lundequista Bokhandeln, Uppsala, 1949.
dc.referencesA. Indrzejczak, Rule-Generation Theorem and Its Applications, Bulletin of the Section of Logic, vol. 47, no. 4 (2018), pp. 265–281.
dc.referencesA. Karpenko, N. Tomova, Bochvar’s three-valued logic and literal paralogics: Their lattice and functional equivalence, Logic and Logical Philosophy, vol. 26, no. 2 (2017), pp. 207–235.
dc.referencesS. C. Kleene, On a notation for ordinal numbers, The Journal of Symbolic Logic, vol. 3, no. 1 (1938), pp. 150–155.
dc.referencesS. C. Kleene, Introduction to metamathematics, Sixth Reprint, Wolters-Noordhoff Publishing and North-Holland Publishing Company, 1971.
dc.referencesB. Kooi, A. Tamminga, Completeness via correspondence for extensions of the logic of paradox, The Review of Symbolic Logic, vol. 5, no. 4 (2012), pp. 720–730.
dc.referencesE. Kubyshkina, D. V. Zaitsev, Rational agency from a truth-functional perspective, Logic and Logical Philosophy, vol. 25, no. 4 (2016), pp. 499– 520.
dc.referencesS. Negri, J. von Plato, Structural Proof Theory, Cambridge: Cambridge University Press, 2001.
dc.referencesY. Petrukhin, V. Shangin, Automated correspondence analysis for the binary extensions of the logic of paradox, The Review of Symbolic Logic, vol. 10, no. 4 (2017), pp. 756–781.
dc.referencesY. Petrukhin, V. Shangin, Automated proof searching for strong Kleene logic and its binary extensions via correspondence analysis, Logic and Logical Philosophy, vol. 28, no. 2 (2019), pp. 223–257.
dc.referencesY. Petrukhin, V. Shangin, Natural three-valued logics characterised by natural deduction, Logique et Analyse, vol. 244 (2018), pp. 407–427.
dc.referencesY. Petrukhin, V. Shangin, Completeness via correspondence for extensions of paraconsistent weak Kleene logic, The Proceedings of the 10th Smirnov Readings in Logic (2017), pp. 114–115.
dc.referencesY. Petrukhin, V. Shangin, Correspondence Analysis and Automated Proofsearching for First Degree Entailment, European Journal of Mathematics, online first article, DOI: 10.1007/s40879-019-00344-5.
dc.referencesY. I. Petrukhin, Correspondence analysis for first degree entailment, Logical Investigations, vol. 22, no. 1 (2016), pp. 108–124.
dc.referencesY. Petrukhin, Generalized Correspondence Analysis for Three-Valued Logics, Logica Universalis, vol. 12, no. 3–4 (2018), pp. 423–460.
dc.referencesY. I. Petrukhin, Correspondence analysis for logic of rational agent, Chelyabinsk Physical and Mathematical Journal, vol. 2, no. 3 (2017), pp. 329–337.
dc.referencesG. Priest, The logic of paradox, Journal of Philosophical Logic, vol. 8, no. 1 (1979), pp. 219–241.
dc.referencesK. Segerberg, Arbitrary truth-value functions and natural deduction, Mathematical Logic Quarterly, vol. 29, no. 11 (1983), pp. 557–564.
dc.referencesA. Tamminga, Correspondence analysis for strong three-valued logic, Logical Investigations, vol. 20 (2014), pp. 255–268.
dc.referencesN. E. Tomova, A lattice of implicative extensions of regular Kleene’s logics, Reports on Mathematical Logic, vol. 47 (2012), pp. 173–182.
dc.referencesA. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, second edition, Cambridge: Cambridge University Press, 2000.
dc.referencesW. Wernick, Complete sets of logical functions, Transactions of the American Mathematical Society, vol. 51 (1942), pp. 117–132.
dc.contributor.authorEmailDorota.Leszczynska@amu.edu.pl
dc.contributor.authorEmailpetrukhin@philos.msu.ru
dc.contributor.authorEmailshangin@philos.msu.ru
dc.contributor.authorEmailMarcin.Jukiewicz@amu.edu.pl
dc.identifier.doi10.18778/0138-0680.48.1.04
dc.relation.volume48en_GB


Pliki tej pozycji

Thumbnail

Pozycja umieszczona jest w następujących kolekcjach

Pokaż uproszczony rekord

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.
Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.