Programme
Venue and Registration
- Venue: ARQNL 2026 is part of the Federated Logic Conference (FLoC) in Lisbon. The workshop will take place in Edifício II (Building II) at ISCTE (Instituto Universitário de Lisboa), a university located in Lisbon, Portugal. See the information about the venue on the FLoC website for more details.
- Registration: See the FLoC website for more information on how to register for the ARQNL workshop. The early registration deadline is June 1st.
Invited Speakers
-
David Fernández-Duque,
University of Barcelona
"Decidable non-classical analogues of linear temporal logic"
Schedule
The ARQNL 2026 programme schedule as a PDF document:Friday, 24 July 2026
| 08:55-09:00 |
Opening of the ARQNL Workshop Christoph Benzmüller, Jens Otten and Revantha Ramanayake | |
| 09:00-09:50 | Invited Talk Decidable Non-Classical Analogues of Linear Temporal Logic David Fernández-Duque | |
| 09:50-10:30 | Session 1: Modal Logics (Session Chair: Christoph Benzmüller) | |
| 09:50-10:10 |
Algorithmic Properties of First-Order Modal Logics of Some Classes of Trees Dmitry Shkatov and Mikhail Rybakov |
|
| 10:10-10:30 |
Interpolation Calculi for Modal Logics Jonte Deakin, Dirk Pattinson and Cláudia Nalon | PO |
| 10:30-11:00 | Coffee Break | |
| 11:00-12:00 | Session 2: Proof Theory and Substructural Logics (Session Chair: Revantha Ramanayake) | |
| 11:00-11:20 |
The Logic of Bunched Implications is Undecidable, Mechanized in Rocq Dominique Larchey-Wendling |
|
| 11:20-11:40 |
Beth Semantics and Tableaux for Bi-Intuitionistic Bunched Implications Didier Galmiche, Benjamin Izart and Daniel Mery |
|
| 11:40-12:00 |
Number Systems and Hilbert Calculi for Atomic Logics Guillaume Aucher | PO |
| 12:00-13:30 | Lunch Break | |
| 13:30-14:45 | Session 3: Definite Descriptions and Free Logics (Session Chair: Torben Braüner) | |
| 13:30-13:50 |
Second-order Positive Free Logic with Second-order Definite Descriptions Yaroslav Petrukhin |
|
| 13:50-14:10 |
Sequent Calculus for Negative Free Logic of Classes Andrzej Indrzejczak |
|
| 14:10-14:30 |
A Paradefinite Version of Russellian Theory of Definite Descriptions Yaroslav Petrukhin |
|
| 14:30-14:45 |
Python-Based Reasoner for Description Logic with Definite Descriptions Michał Sochański, Przemysław Wałęga and Michał Zawidzki |
|
| 14:45-15:10 | Coffee Break | |
| 15:10-16:10 | Session 4: Tableaux (Session Chair: Jens Otten) | |
| 15:10-15:30 |
A Sound and Weakly Complete Tableau System for Social Announcement Logic Rui Zhu |
|
| 15:30-15:50 |
A Tableau System for First-Order Epistemic Logic with Standard Names Jens Classen and Torben Braüner |
|
| 15:50-16:10 |
Towards Quantified Dependent Assertion Logic Lukas Grätz |
|
| 16:10-16:40 | Coffee Break | |
| 16:40-17:30 | Session 5: Embeddings and Benchmarks (Session Chair: Dmitry Shkatov) | |
| 16:40-16:55 |
Embedding Deontic Logic Operators from a Large Ontology in Higher-order Logic Christopher Feener, Adam Pease and Richard Thompson | PO |
| 16:55-17:15 |
First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness Christoph Benzmüller and Daniel Kirchner |
|
| 17:15-17:30 |
Generating Random Benchmark Problems for the First-Order Logic of Here-and-There Jens Otten |
|
| 17:30 | Closing |
PO: Presentation Only