Tadeusz’s publications

More information about my work can be found here and especially in my research statement. For earlier papers, some comments have been inlined in this bibliography.

Here is a PDF version of the publication list.

2020
[39] , , and : Cheap CTL Compassion in NuSMV, In 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020), LNCS, vol. 11990, pp. 248–269, Springer, . Artifact evaluation: Available and Functional [bibtex] [url]
2019
[38] , , and : The High-Level Benefits of Low-Level Sandboxing, In Proc. ACM Program. Lang., 4(POPL), . 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020). Artifact evaluation: Reusable [bibtex] [url] [doi]
[37] and : Lewisian Fixed Points I: Two Incomparable Constructions, In CoRR, abs/1905.09450, . [bibtex] [url]
[36] and : Complete Additivity and Modal Incompleteness, In Review of Symbolic Logic, 12(3), pp. 487–535, . Available on arXiv: https://arxiv.org/abs/1809.07542, eScholarship: https://escholarship.org/uc/item/01p9x1hv and publisher's page: https://doi.org/10.1017/S1755020317000259 [bibtex] [url] [doi]
2018
[35] and : Lewis meets Brouwer: constructive strict implication, In Indagationes Mathematicae, 29, pp. 36–90, . A special issue "L.E.J. Brouwer, fifty years later" [bibtex] [doi]
[34] , , and : Model Theory and Proof Theory of Coalgebraic Predicate Logic, In Log. Methods Comput. Sci., 14(1), . [bibtex] [url] [doi]
[33] : Infinite Populations, Choice and Determinacy, In Studia Logica, 106, pp. 969–999, . [bibtex] [url] [doi]
[32] and : One Modal Logic to Rule Them All?, In G. Bezhanishvili, G. D'Agostino, G. Metcalfe, T. Studer, eds.: Advances in Modal Logic, vol. 12, pp. 367–386, College Publications, . Extended technical report available at https://escholarship.org/uc/item/07v9360j [bibtex] [pdf]
2017
[31] : Constructive Modalities with Provability Smack (Author's Cut), . Unabridged and extended version of a chapter in the Esakia volume of "Outstanding Contributions to Logic" [bibtex] [url]
[30] , and : A van Benthem/Rosen Theorem for Coalgebraic Predicate Logic, In Journal of Logic and Computation, 27(3), pp. 749–773, . [preprint] [bibtex] [url]
[29] and : Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion, In Fundamenta Informaticae, 150, pp. 407–449, . special issue FiCS'13 edited by David Baelde, Arnaud Carayol, Ralph Matthes and Igor Walukiewicz [bibtex] [url] [doi]
[28] , and : Negative Translations and Normal Modality, In Dale Miller, ed.: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics (LIPIcs), vol. 84, pp. 27:1–27:18, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, . [Local copy] [bibtex] [url] [doi]
[27] and : An Algebraic Glimpse at Bunched Implications and Separation Logic, In CoRR, abs/1709.07063, . To appear in the Outstanding Contributions volume "Hiroakira Ono on Residuated Lattices and Substructural Logics" [bibtex] [url]
2016
[26] , and : Relational lattices: From databases to universal algebra, In JLAMP, 85(4), pp. 540–573, . special issue with selected papers RAMiCS 2014 edited by Peter Höfner, Peter Jipsen, Wolfram Kahl and Martin E. Müller The final publication is available at Springer via http://dx.doi.org/10.1016/j.jlamp.2015.11.008 [bibtex] [url] [doi]
2014
[25] , and : Relational Lattices, In Peter Höfner, Peter Jipsen, Wolfram Kahl, Martin E. Müller, eds.: Relational and Algebraic Methods in Computer Science 2014 (RAMiCS), Lecture Notes in Computer Science, vol. 8428, pp. 327–343, Springer International Publishing, . Superseded by the journal version in the special issue of JLAMP with selected papers of RAMiCS 2014 The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-06251-8_20. [bibtex] [url] [doi]
[24] : Constructive modalities with provability smack, Chapter in Guram Bezhanishvili, ed.: Leo Esakia on duality in modal and intuitionistic logics, Outstanding Contributions to Logic, vol. 4, pp. 179–208, Springer, . [bibtex] [doi]
2013
[23] and : Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion, In David Baelde, Arnaud Carayol, eds.: FICS, EPTCS, vol. 126, pp. 72–86, . Superseded by the journal version invited to FI [bibtex] [url]
[22] , and : Coalgebraic Predicate Logic: Equipollence Results and Proof Theory, Chapter in Guram Bezhanishvili, Sebastian Löbner, Vincenzo Marra, Frank Richter, eds.: Logic, Language, and Computation. Revised Selected Papers of TbiLLC 2011, Lecture Notes in Computer Science, vol. 7758, pp. 257–276, Springer Berlin Heidelberg, . The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-36976-6_16. [bibtex] [url] [doi]
2012
[21] , , and : Coalgebraic Predicate Logic, In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, Roger Wattenhofer, eds.: Proc. 39th International Colloquium on Automata, Languages, and Programming, ICALP 2012, Lecture Notes in Computer Science, vol. 7392, pp. 299–311, Springer, . [bibtex] [pdf] [doi]
2011
[20] , and : Stone duality for nominal Boolean algebras with 'new', Chapter in Andrea Corradini, Bartek Klin, Corina Cîrstea, eds.: Algebra and Coalgebra in Computer Science, Lecture Notes in Computer Science, vol. 6859, pp. 192–207, Springer Berlin Heidelberg, . [bibtex] [doi]
2010
[19] , and : Complete axiomatizations for XPath fragments, In Journal of Applied Logic, 8(2), pp. 153–172, . Selected papers from the Logic in Databases Workshop 2008 edited by Andrea Calí, Laks V.S. Lakshmanan and Davide Martinenghi [bibtex] [url] [doi]
[18] , and : Some Modal Aspects of XPath, In Journal of Applied Non-Classical Logics, 20(3), pp. 139–171, . Invited paper to the special 20th anniversary issue
For quite a while only the early M4M version was broadly available online. Access to JANCL is rather restricted. I noticed it relatively recently. It is a shame, as the real journal version is much more substantial. You can now verify this claim:

[local copy] [bibtex] [url]
2009
[17] and : On the Termination Problem for Declarative XML Message Processing, Chapter in Sourav S. Bhowmick, Josef Küng, Roland Wagner, eds.: Database and Expert Systems Applications, Lecture Notes in Computer Science, vol. 5690, pp. 83–97, Springer Berlin Heidelberg, .
We define a formal syntax and semantics for the Rule Definition Language (RDL) of DemaqLite, which is a fragment of the declarative XML message processing system Demaq. Based on this definition, we prove that the termination problem for any practically useful sublanguage of DemaqLiteRDL is undecidable, as any such language can emulate a Single Register Machine--a Turing-complete model of computation proposed by Shepherdson and Sturgis.

 [bibtex] [url] [doi]
2008
[16] : Stability of the Blok Theorem, In Algebra Universalis, 58(4), pp. 385–411, .
The theorem generalized here - Wim Blok's classfication of degrees of incompleteness of modal logics - is one of the most beautiful and surpring ones proved in the 1970's. If you have never heard about The Blok Theorem, or heard about it but want to learn more, enjoy!

[preprint] [bibtex] [url] [doi]
[15] and : Completions of GBL-algebras: negative results, In Algebra Universalis, 58(4), pp. 373–384, .
An exercise in substructural logic,
motivated partially by my earlier results in modal logic. We show that
many varieties related to many-valued logics are not closed under any
kind of completions - not just a specific one, like canonical
completions. A significant part of the paper has been incorporated into
this book. The result turned out to be important for an emerging field of algebraic proof theory (Kazushige Terui, Nick Galatos, Agata Ciabattoni) who showed this implies non-existence of well-behaved, strongly analytical, cut-free sequent calculi for logics in question. In his invited talk at OAL2.0 in 2011, Kazushige Terui likened the significance of our result for algebraic proof theory to that of the Gödel results for the Hilbert program, but it was a hyperbole - algebraic proof theory is alive and well. Neither he nor ourselves realized at that time that the restriction of our result to MV-algebras had been carefully hidden in the 2004 Math. Scand. paper by Gehrke and Jonsson. Look for it yourself (and note that you have the advantage of this precise bibliographical reference)... I only found it by accident in 2016.

[bibtex] [url] [doi]
2007
[14] and : The importance of being discrete, Technical report PP–2007–39, Institute for Logic, Language and Computation (ILLC), University of Amsterdam, . [bibtex] [pdf]
[13] and : Topological perspective on the hybrid proof rules, In Electronic Notes in Theoretical Computer Science, 174(6), pp. 79–94, . Proceedings of the International Workshop on Hybrid Logic HyLo 2006 [bibtex] [url] [doi]
[12] : The non-reflexive counterpart of Grz, In Bulletin of the Section of Logic, 36(3–4), pp. 195–208, . A special issue In Honorem Hiroakira Ono edited by Piotr Łukowski [bibtex] [pdf]
2006
[11] and : Completions of GBL-algebras and acyclic modal algebras: negative results, vol. 1525, pp. 51–61, Technical report, Research Institute for Mathematical Sciences (RIMS), Kyoto University, .
This is included here mostly for completeness, as this is an unofficial publication and both modal and substructural results are available in other, properly published journal papers you see on this list. Still, I have to admit it is probably the only one of them which discusses both modal and substructural 'complete incompleteness' side by side.

 [bibtex] [pdf]
[10] : Algebraization of Hybrid Logic with Binders, Chapter in Renate A. Schmidt, ed.: Relations and Kleene Algebra in Computer Science, Lecture Notes in Computer Science, vol. 4136, pp. 281–295, Springer Berlin Heidelberg, .
Tarski-style algebraization of a modal formalism equivalent to the bounded fragment of predicate logic. In the local copy, cleaned some bugs and
added a few comments. Also, page layout differs from the printed version:

[local copy]

[bibtex] [url] [doi]
[9] : Isomorphism via translation, In Guido Governatori, Ian M. Hodkinson, Yde Venema, eds.: Advances in Modal Logic 6, pp. 333–351, College Publications, . Papers from the sixth conference on Advances in Modal Logic, held in Noosa, Queensland, Australia, on 25-28 September 2006 [bibtex] [ps]
2005
[8] and : All finitely axiomatizable tense logics of linear time flows are coNP-complete, In Studia Logica, 81(2), pp. 153–165, . [bibtex] [url] [doi]
[7] : An algebraic approach to incompleteness in modal logic, PhD thesis, Japan Advanced Institute of Science and Technology, .
It is not an easy reading. And I am by no means proud of this fact. If you are interested in the results of my dissertation, the Algebra Universalis solo paper, the AiML 5 paper, the Studia Logica 2004 paper, and the joint Studia Logica paper with Frank Wolter may prove better choices.

[local copy]

[bibtex]
[6] : Mathematical foundations for self-referential sentences, Technical report IS–RR–2005–005–001, JAIST, . [bibtex] [pdf]
[5] : On notions of completeness weaker than Kripke completeness, In Renate A. Schmidt, Ian Pratt-Hartmann, Mark Reynolds, Heinrich Wansing, eds.: Advances in Modal Logic 5, pp. 149–169, King's College Publications, . Papers from the fifth conference on Advances in Modal Logic, held in Manchester (UK) in September 2004 [bibtex] [ps]
2004
[4] : Modal Incompleteness Revisited, In Studia Logica, 76(3), pp. 329–342, . [bibtex] [url] [doi]
[3] : Some notes on the superintuitionistic logic of chequered subsets of ${\sf R}^\infty$, In Bulletin of the Section of Logic, 33(2), pp. 81–86, .
The paper studies superintuitionistic version of the logic of chequered subsets introduced by Johan van Benthem, Guram Bezhanishvili and Mai Gehrke. It is observed that this logic possesses
the disjunction property, contains the Scott axiom, fails to contain the
Kreisel-Putnam axiom and is not structurally complete. It is also a sublogic of the Medvedev logic
ML.
Very interesting
follow-up results have been obtained by Gaelle Fontaine and Timofei Shatrov. The latter claimed to have settled negatively the issue of finite axiomatizably of Cheq; however, to the best of my knowledge, this has never been published. The local copy is slightly extended; in particular, the
proof of main theorem is hopefully more readable:

[local copy] [bibtex] [url]
2002
[2] : A Continuum of Incomplete Intermediate Logics, In Reports on Mathematical Logic, 36, pp. 131–141, . Corrected in 2018 [bibtex] [url]
2001
[1] : Niezupełne Logiki Pośrednie (Incomplete Intermediate Logics), . Thesis submitted for the degree of Magister (Master) of Philosophy, Institute of Philosophy, Jagiellonian University (UJ) [bibtex] [pdf]