|Prof. Katalin Bimbo|
|Teaching||Research||Contact and other info|
I taught the following philosophy courses (some of them many times) in the last several years. (These are all “PHIL” courses, listed by number, in decreasing order.)
My main research area is logic. I am especially interested in nonclassical logics, including relevance and substructural logics, modal logics, combinatory logic and λ-calculi. Nonclassical logics were first introduced as a solution to philosophical problems such as the problem of implication and entailment. Later on, new logics emerged in other disciplines too — from mathematics and computer science to linguistics. Some of my research interests — beyond logic and the philosophy of logic — are connected to the latter areas. I have a keen interest in the philosophy of mathematics, in particular, in the foundations of mathematics. I also try to follow the latest developments in the philosophy of computer science and informatics, especially, those that concern questions related to theoretical computer science — such as algorithmics, programming language design, information theory, complexity theory and cyber security. Earlier, I worked on some questions in the semantics of natural languages, primarily, using modal (specifically, temporal/tense) logics and discourse representation theory.
Some of my research results concern semantics for various nonclassical logics (e.g., calculi for combinatory logic). J. Michael Dunn and I wrote a book on the relational semantics of nonclassical logical calculi. These kinds of semantics generalize Kripke's possible-world semantics for normal modal logics, and have been the preferred sort of semantics for decades. Some years ago, we worked out representations for Kleene logic and action logic, which are closely related to dynamic logic. We also collaborated on defining a “four-valued” semantics for minimal substructural logic. We continue to work — within a SSHRC IG — on problems related to the semantics of non-classical logics, primarily, on questions connected to the three-termed relational semantics. A paper I wrote about the semantics of implicational relevance logics appeared this year in the proceedings of the IsraLog 2014 workshop. The (first) Third Workshop, which is thematically connected to this project, took place on May 16–17, 2016, at the University of Alberta. (The poster.)
A more precise characterization of classes of structures for various nonclassical logics leads straightforwardly to topological frames. I proved topological duality theorems for ortho- and De Morgan lattices and for the algebra of the logic of entailment. These duality theorems provide plenty of insights into the logics themselves, because interpretations are maps in a category.
Combinatory logic and λ-calculi are connected to other nonclassical logics in various ways, one of which is the Curry–Howard correspondence (CHC). J. Michael Dunn and I wrote a paper about extracting combinatory inhabitants from proofs in a sequent calculus for implicational ticket entailment. This is the first step to extend CHC into new directions. Certain combinatory terms are equivalent to proofs in various nonclassical logics; therefore, the question of decidability turns into the question of inhabitation. Combinatory logic in itself is an elegant and powerful formalism that can represent computable functions — just as Turing or register machines and Markov algorithms can. A book on combinatory logic that I wrote appeared a couple of years ago.
The proof theory of nonclassical logics sometimes gets really tricky. The original classical sequent calculus is a seemingly simple proof system, but in reality, the proofs are tightly controlled — as evidenced by the cut theorem. Some well-known relevance logics cannot be formalized as extensions of the associative Lambek calculus, which causes various “technical complications.” I succeeded in defining sequent calculi for some of these relevance logics together with proving the cut theorem for them. A major research project that I and J. Michael Dunn worked on (as a SSHRC SRG), was the problem of the decidability of the implicational fragment of ticket entailment, which remained open for over 50 years. Our proof was made possible by our new conceptualization of a sequent calculus for implicational R. I wrote a book on proof theory with a focus on sequent calculi (including some tableaux and resolution systems). In the summer of 2014, I closed another long-open problem: I proved that MELL, the multiplicative–exponential fragment of linear logic is decidable. J. Michael Dunn and I extended this result, and proved that full propositional linear logic (LL) is also decidable. This past summer, I constructed another proof of the decidability of LL.
I am certain that logic — together with its many connections and offsprings — is an exciting and thriving field of research.
I received a Faculty of Arts Research Excellence Award in 2012.
University of Alberta
Page updated on:
October 19th, 2016
My Erdös number:
Three (i.e., 3)
Some U of A links:
|Publications selected from the 21st century|