Geodesic
Functional Completeness in CPL via Correspondence Analysis
Bulletin of the Section of Logic, Tome 48 (2019) no. 1.

Voir la notice de l'article provenant de la source Library of Science

Kooi 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.
Keywords: correspondence analysis, invertible rules, classical propositional logic, functional completeness, sequent calculus, automated deduction, automated rules generation 
@article{BSL_2019_48_1_a2,
     author = {Leszczy\'nska-Jasion, Dorota and Petrukhin, Yaroslav and Shangin, Vasilyi and Jukiewicz, Marcin},
     title = {Functional {Completeness} in {CPL} via {Correspondence} {Analysis}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {48},
     number = {1},
     year = {2019},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2019_48_1_a2/}
}
TY  - JOUR
AU  - Leszczyńska-Jasion, Dorota
AU  - Petrukhin, Yaroslav
AU  - Shangin, Vasilyi
AU  - Jukiewicz, Marcin
TI  - Functional Completeness in CPL via Correspondence Analysis
JO  - Bulletin of the Section of Logic
PY  - 2019
VL  - 48
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2019_48_1_a2/
LA  - en
ID  - BSL_2019_48_1_a2
ER  - 
%0 Journal Article
%A Leszczyńska-Jasion, Dorota
%A Petrukhin, Yaroslav
%A Shangin, Vasilyi
%A Jukiewicz, Marcin
%T Functional Completeness in CPL via Correspondence Analysis
%J Bulletin of the Section of Logic
%D 2019
%V 48
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2019_48_1_a2/
%G en
%F BSL_2019_48_1_a2
Leszczyńska-Jasion, Dorota; Petrukhin, Yaroslav; Shangin, Vasilyi; Jukiewicz, Marcin. Functional Completeness in CPL via Correspondence Analysis. Bulletin of the Section of Logic, Tome 48 (2019) no. 1. http://geodesic.mathdoc.fr/item/BSL_2019_48_1_a2/