Seminars
Seminars, workshops and other events organised by our group
The Logic Group runs a bi-weekly Research Seminar in Logic, monthly Nordic Online Logic Seminar and the annual Lindström Lecture series, as well as other events. See below for a list of recent and upcoming events or follow the links to jump straight to a category.
The research seminar in Logic meets on alternate Fridays at 10.15. Unless otherwise stated, seminars are held at the department building (Humanisten). Details of online talks are distributed in the GU Logic mailing list. Alternatively, contact Graham E Leigh directly.
-
-
Jouko Väänänen (University of Helsinki and ILLC, University of Amsterdam)
On the Logic of Dependence
-
Opponent: TBA
Abstract Description logics are designed to reason efficiently with ontologies in knowledge bases, which are widely used in several industries. Human errors commonly cause mistakes to occur in the axioms of these ontologies, which leads to the logics deducing false conclusions. Ontology engineers spend much time on finding these false axioms to repair the ontology. This process can be facilitated by presenting a justification of the false conclusion, i.e. a set of axioms that entail the conclusion. Typically, the number of justifications for a given conclusion is very large and it is not clear which one should be presented.
It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.
A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.
To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.
Examination committee:
- TBC
-
A 2½-day workshop dedicated to current and future trends in cyclic and illfounded forms of provability and justification. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity, the Swedish Research Council through the research project Proofs with Cycles and Computation, and the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg.
-
-
-
-
In this talk I will briefly outline Krister’s biography, focusing mainly on the early nineties onwards when I became Krister’s first PhD student. By appeal (mostly) to anecdote I will try to highlight what I take to be some of the most notable features in Krister’s approach to and views on pilosophically inspired logical research and education.
-
Krister Segerberg was one of the architects of modal logic as we know it today. I will highlight a few of his major contributions and show some of their subsequent impact in various academic communities. I conclude with some thoughts on the blend of philosophical logic and formal philosophy embodied in Krister’s distinguished career.
-
On Monday, 25 August the Nordic Online Logic Seminar will host a special event in memory of Krister Segerberg, who passed away in January this year. Krister Segerberg was Professor of Theoretical Philosophy at Uppsala and, among logicians, is widely known for his pioneering work in modal logic where he initiated an influential systematic study of completeness proofs that still is standard in the field.
The seminar will feature talks by two academics that knew Krister Segerberg well:
- Johan van Benthem (UvA), Building Modern Modal Logic: Honoring Krister Segerberg
- John Cantwell (KTH), Some reflections on Krister’s philosophy of philosopy
A URL for this seminar will be distributed via the GU Logic and Nordic Online Logic mailing lists.
-
Opponent: Makoto Fujiwara, Assistant Professor, Tokyo University of Science
Abstract This dissertation concerns first-order theories of iterated positive truth and fixpoints over intuitionistic arithmetic in three respects: the strength of these theories relative to the arithmetic base theories, relationships between theories of positive fixpoints and compositional and disquotational truth for truth-positive sentences, and a comparison with the classical case.
It is known that these theories over classical Peano arithmetic (PA) are mutually interpretable and exceeds the strength of PA. Over intuitionistic Heyting arithmetic (HA), on the other hand, finite iterations of strictly positive fixpoints have been shown to be conservative.
After introducing the setting and presenting the earlier results, as well as the technical tools, the main section of the dissertation can be roughly divided into two parts. The first presents a novel proof of the conservativity result above. The proof interprets the theories into the logic of partial terms where a realizability interpretation is used to reduce the problem to fixpoints for almost negative operator forms. A diagonal argument using a hierarchy of almost negative formulae with corresponding partial satisfaction predicates yields the result.
The second part generalises the tri-interpretation result from the second paragraph to intuitionistic theories, by proposing a new generalisation of positivity called guarded positivity with the aim to better capture the behaviour of intuitionistic implications and their interplay with transfinite iterations of truth and fixpoint predicates. As a corollary, these transfinite theories are stronger than HA.
A discussion of the results and the methods used concludes the dissertation.
Examination committee:
- Vera Koponen, chair (Uppsala University)
- Takako Nemoto (Tohoku University)
- Benno van den Berg (University of Amsterdam)
-
Akama et al. [1] introduced a hierarchical classification of first-order formulas and investigated them in the context of semi-classical arithmetic. In this talk, we first give a justification for the hierarchical classification in a general context of first-order theories. In fact, we formalize the standard transformation procedure for prenex normalization, and show that the classes E_k and U_k introduced in [1] are exactly the classes induced by Sigma_k and Pi_k respectively via the transformation procedure. See [2] for the details. In addition, we restrict the prenex normalization procedures to those which are possible over intuitionistic logic with assuming the decidability of formulas of degree n. Then we introduce new classes E^n_k and U^n_k of formulas with two parameters k and n, and show that they are exactly the classes induced by Sigma_k and Pi_k respectively according to the n-th level semi-classical prenex normalization. This is a joint work with Taishi Kurahashi.
[1] Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS ’04), pp.192–201, 2004.
[2] Makoto Fujiwara and Taishi Kurahashi, Prenex normalization and the hierarchical classification of formulas, Archive for Mathematical Logic, vol. 63, pp. 391-403, 2024.
-
Logics that are obtained by constraining the available syntactic resources, such as first-order logic with a finite number of variables or with bounded quantifier rank, are central to finite model theory and descriptive complexity. In this talk, I will describe a categorical approach, which is model-theoretic in spirit, to study these logics using so-called game comonads. I will explain how these comonads capture various logic fragments (positive, existential, etc.) and combinatorial parameters of structures in a syntax-free manner. Furthermore, I will argue that this categorical perspective suggests a modal approach to various resource-bounded logics.
-
Logical inferentialists hold that the meaning of logical operators is given by their rules of inference. Arthur Prior cast doubt on this by introducing rules for his tonk operator that would allow for the derivation of any sentence whatsoever from any sentence whatsoever. The obvious inferentialist reply was to require some constraints on the defining rules, such as conservativeness (Belnap) or harmony (Dummett). In this talk, I will defend and investigate a different constraint: rules define a classical logical operator just in case they translate into an explicit definition in pure classical second-order logic. The right-hand side of this criterion will be found (i) to be philosophically principled in taking the idea of rules as definitions perfectly seriously, (ii) to explain how the semantic meaning of the operators can be determined from their rules, (iii) to be local in a similar sense as harmony, (iv) to validate the intuitionistic natural deduction rules and the intuitionistic/classical sequent calculus rules as defining the classical propositional operators while ruling out Prior’s rules for tonk, (v) to make clear why already the intuitionistic natural deduction rules define the classical meaning of logical operators so long as metavariables are interpreted as expressing classical propositions, (vi) to validate the classical natural deduction rules as analytic, (vii) to entail consistency, and, in the case of propositional operators (not quantifiers), (viii) to be decidable and (ix) to determine precisely those operators to be definable by rules that correspond to truth-functions.
-
Opponent: Jakub Szymanik, Associate professor at the Center for Brain/Mind Sciences and the Computer Science Department at the University of Trento.
Abstract Description logics are designed to reason efficiently with ontologies in knowledge bases, which are widely used in several industries. Human errors commonly cause mistakes to occur in the axioms of these ontologies, which leads to the logics deducing false conclusions. Ontology engineers spend much time on finding these false axioms to repair the ontology. This process can be facilitated by presenting a justification of the false conclusion, i.e. a set of axioms that entail the conclusion. Typically, the number of justifications for a given conclusion is very large and it is not clear which one should be presented.
It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.
A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.
To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.
-
Frame definability is a well-studied notion for a plethora of logics: a class of frames is defined by a set of formulas if and only if such formulas are validities for all and only the frames in such class.
In this talk, I will present a series of results about frame definability in a fragment of conditional logic. Conditional logic is an extension of propositional logic that includes a binary “counterfactual” conditional operator \(\leadsto\). We specifically make the following choices: (i), we consider the non-nested fragment of conditional logic (i.e., where conditionals are not allowed in the scope of other conditionals), and (ii), we consider only finite posets as the underlying structure of the models of our logic. Given these assumptions, a formula of the form \(\varphi \leadsto \psi\) is intuitively true if the consequent \(\psi\) is true in all the minimal (with respect to the partial order of the poset) worlds where the antecedent \(\varphi\) is true. Via these semantics, this fragment of conditional logic becomes relevant in several fields, such as default reasoning and belief revision.
I will present the following results: (i) a set of non-nested conditional formulas each defining a different class of finite posets; (ii) a characterization theorem identifying the classes of finite posets that can be defined by a non-nested conditional formula; and (iii), a Sahlqvist-like theorem proving that every class of finite posets definable via a non-nested conditional formula is definable also by a first-order formula.
This talk is based on the paper Frame Definability in Conditional Logic, a joint work with Damiano Fornasiere and Johannes Marti, which was published at AiML 2024.
-
Propositional dynamic logic (PDL) is a well-known modal logic which originates from the wave of so-called process logics that emerged in the 1970s. Characteristic to PDL is that its collection of modalities is given as the set of regular expressions over some set of atomic programs and (possibly) so-called test program. The main results on PDL, such as a sound and complete axiomatisation and the decidability and computational complexity of its satisfiability problem, were obtained relatively soon after its introducton. In the talk I will review some results on PDL that have been discovered (or re-discovered) in more recent years. Topics to be discussed include the relation of PDL with other fixpoint logics, expressive completeness results and cut-free proof systems. The main issue that I want to address concerns the Craig interpolation property for PDL, a long-standing problem that can finally be settled. I will finish with mentioning some open problems.
The talk is based on work with and by many co-authors.
-
This talk explores the potential of conceptual spaces as a novel layer in robot architecture to enhance the interaction and communication of children diagnosed with Autism Spectrum Disorder who use social robots’ assistance. Drawing on insights from cognitive theories and empirical observations, we propose a model that utilises conceptual spaces to better explain and thanks to this simulate the unique cognitive processes of autistic individuals. Application of our model will facilitate more effective interventions using robots, thereby enabling social engagement and reducing the communication barriers faced by autistic children. The work is in collaboration with Antonio Chella (Palermo) and Peter Gärdenfors (Lund).
-
Sun Tzu was a military strategist who lived in China about 2500 years ago. His book is still popular today, especially in business circles.
This talk presents a study of “The Art of War” from the perspectives of logic, mathematics, and computer science. We explain briefly what a mind map is and our strict text tree interpretation of it, for the purpose of analyzing Sun Tzu’s text. We show that you can improve the translation and find more meaning in the text, representing the text as mind maps. If time permits, we will illustrate that, surprisingly, the text still helps us to understand what is happening in warfare today.
The title of this talk is also the title of our book, co-authored by Kaibo Xie (Tsinghua Univ. Beijing), and Bonan Zhao (Univ. of Edinburgh), and published in 2022 by Springer. The book is the result of a joint study of the Institute of Language, Logic and Computation, Univ. of Amsterdam and the Institute for Philosophy, Tsinghua University, Beijing, China.
-
Locales and toposes are the geometric analogues of propositional and first-order logic, and in both instances the former is contained in the latter. As in the logical case, there is a non-negligible jump in complexity from locales to toposes. In this talk, I will provide a way to overcome some of the added complexity by sketching a proof that locales form a dense subcategory of toposes, meaning that toposes can be expressed in terms of locales in a canonical way. This result can be understood as a categorical justification for studying first-order logic through the lens of propositional logic, and, time permitting, we will see examples.