Aim of the project is to extend both the theoretical knowledge about Kleene logics and their applications in the theory of knowledge and computer science. The project is articulated in 4 main objectives.
Objective 1 (UNICA). External Kleene logics: algebraic semantics and proof-theory
Weak Kleene logics are usually understood in the internal language (that of classical logic), although they have historically been introduced in a richer language, called external [8,27]. Objective 1 aims to study external Kleene logics, with respect to both their algebraic counterparts and their proof-theory. On the one hand, we plan to develop the algebraic theory of Plonka sums also for external logics, starting from Bochvar external logic [13]. On the other hand, we will develop the unexplored field of the proof-theory of Kleene external logics, for which only Hilbert-style axiomatizations exist [22]. Finally, as internal Kleene logics are examples of the wider family of the logics of variable inclusion [11], we will explore possible generalizations of external logics.
Objective 2 (UNICA). Modal logics based on Kleene logics
Modal logics whose propositional basis is a strong Kleene logic have been introduced in the seminal works of Fitting [23,24], and by Prior and Segerberg [32,33], for weak Kleene (interestingly, these latter are defined over the external language). Objective 2 aims to expand the study of modal logics based on both strong and weak Kleene logics. It will be particularly focused on the algebraic semantics of strong Kleene logics (Kleene algebras with operators?), the algebraic semantics of modal weak Kleene (Plonka sums of algebras with operators?) and the correspondent dual relational semantics. In connection with Objective 3 (see below), Objective 2 aims also to study the algebraic counterparts and the proof-theory of epistemic modal logics based on Kleene logics.
Objective 3 (UNIURB + UNICA). Formal models of knowledge and ignorance based on modal Kleene logics
A preliminary aim consists in providing an accurate taxonomy of the forms of ignorance and their respective formal models already given. Moreover, Objective 3 intends also to provide the missing formal models (e.g. fake news ignorance; ignorance in fallible knowledge) and propose a comparison between the different logics of ignorance. Following the methodology in [3] and [10], we will explore the conditions under which various forms of ignorance are produced, the formation of second-order ignorance with respect to them, and the role of factivity in them. Finally, we will consider the role of various forms of ignorance and their formal models in the characterization of phenomena such as fake news and fallible knowledge. We expect the development of modal logics for ignorance based on Kleene logics (following the intuition in [10]).
Objective 4 (UNIURB). Development of process algebraic theories based on Kleene logic, with applications to concurrent programming and debugging theory
Weak Kleene logics appear suitable formalisms to model computer programs affected by errors [18,21]. In computer science, the combination of many-valued logics and concurrency theory is intended to characterize explicitly errors in computer programs in a formal concurrent setting. In particular, process algebras have been investigated using both strong [5] and weak Kleene logics [6]. However, these formalisms have not been systematically developed to investigate the features, origins, and effects of different kinds of errors in computer programs. The experiments above have been confined to the ACP (Algebra of Communicating Processes) process algebra, where an ad-hoc operator was used to model inaction/deadlock typical of ACP. Also, (strong) Kleene logics have been successfully applied for debugging declarative and logic programs (e.g., Prolog programs) [31]. In the setting of reversible computation recent applications of declarative debugging, also known as algorithmic debugging [14], are proposed for concurrent functional programs (Erlang) [15] and employed in generating test cases used in debugging session and cycles of software development process [16].
Objective 4 concerns the development of a process algebraic theory of fallible computations based on Kleene logics, with an application to reversible debugging of Erlang and the analysis of the implications of these computer science results on the issue of miscomputation.
Bibliography
[1] A. Abdallah. The Logic of Partial Information. Springer, 1995.
[2] A. Aldini. On the modeling and verification of the spread of fake news, algebraically. J. Logic Comput., 2022.
[3] A. Aldini, P. Graziani and M. Tagliaferri. Reasoning about Ignorance and Beliefs. In SEFM, LNCS, 2021.
[4] Jc Beall. Off-topic: A new interpretation of weak-kleene logic. Australas. J. Log., 2016.
[5] J. Bergstra and A. Ponse. Bochvar-McCarthy Logic and Process Algebra. Notre Dame J. Form. Log., 1998.
[6] J. Bergstra and A. Ponse. Kleene’s three-valued logic and process algebra. Inform. Process. Lett., 1998.
[7] J. Bergstra et al. A propositional logic with 4 values: true, false, divergent and meaningless. J. Appl. Non-Class. Log, 1995.
[8] D. Bochvar. On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus. Mat. Sb., 1938.
[9] S. Bonzio. Dualities for Płonka sums. Log. Univers., 2018.
[10] S. Bonzio, V. Fano and P. Graziani. A logical modeling of severe ignorance. J. Phil. Logic, 2023.
[11] S. Bonzio, F. Paoli and M. Pra Baldi. Logics of variable inclusion. Springer, 2022.
[12] S. Bonzio et al. On Paraconsistent Weak Kleene Logic: axiomatization and algebraic analysis. Studia Logica, 2017.
[13] S. Bonzio, M. Pra Baldi. On the structure of Bochvar algebras, ArXive pre-print, 2023.
[14] R. Caballero et al. A survey of algorithmic debugging. ACM Comput. Surv., 2017.
[15] R. Caballero et al. Declarative debugging of concurrent erlang programs. J. Log. Algebr. Methods Program., 2018.
[16] R. Caballero et al. A unified framework for declarative debugging and testing. Inf. Softw. Technol., 2021.
[17] M. Carrara and W. Zhu. Computational Errors and Suspension in a PWK Epistemic Agent. J. Logic Comput., 2021.
[18] R. Ciuni, T. M. Ferguson, and D. Szmuc. Modeling the interaction of computer errors by four-valued contaminating logics. In Logic, Language, Information, and Computation, 2019.
[19] M. Console et al. Propositional and predicate logics of incomplete information. Artif. Intell., 2022.
[20] V. Fano and P. Graziani. A working hypothesis for the logic of radical ignorance. Synthese, 2021.
[21] T. Ferguson. A computational interpretation of conceptivism. J. Appl. Non-Class. Log, 2014.
[22] V. Finn and R. Grigolia. Nonsense logics and their algebraic properties. Theoria, 1993.
[23] M. Fitting. Many-valued modal logics. Fund. Inform., 1991.
[24] M. Fitting. Many-valued modal logics II. Fund. Inform., 1992.
[25] L. Floridi, N. Fresco and G. Primiero. On malfunctioning software. Synthese, 2015.
[26] N. Fresco and G. Primiero. Miscomputation. Philos. Technol., 2013.
[27] S. Halldén. The Logic of Nonsense. Lundequista Bokhandeln, 1949.
[28] J. Hintikka. Knowledge and Belief. Cornell University Press, 1962.
[29] S. Kleene. Introduction to Metamathematics. North Holland, 1952.
[30] E. Kubyshkina and M. Petrolo. A logic for factive ignorance. Synthese, 2021.
[31] L. Naish. A three valued semantics for logic programmers. Theory Pract. Log. Program., 2006.
[32] A. Prior. Notes on a group of new modal systems. Log. Anal., 1959.
[33] K. Segerberg. Some modal logics based on a three-valued logic. Theoria, 1967.
[34] R. Turner. Logics for Artificial Intelligence. Ellis Horwood, 1984.
[35] W. van der Hoek and A. Lomuscio. A logic for ignorance. In Declarative Agent Languages and Technologies, 2004.