Theoretische Informatik

Tadeusz Litak's Publications

[33] Lewis meets Brouwer: constructive strict implication (Tadeusz Litak, Albert Visser), In Indagationes Mathematicae, vol. 29, pp. 36–90, 2018. [Elsevier version] open till Feb 10, 2018 (A special issue "L.E.J. Brouwer, fifty years later") [bib] [pdf] [doi]
[32] Infinite Populations, Choice and Determinacy (Tadeusz Litak), In Studia Logica, 2017. [Local version] (special issue on Logics for Social Behaviour edited by A. Palmigiano and M. Pivato) [bib] [pdf] [doi]
[31] A van Benthem/Rosen Theorem for Coalgebraic Predicate Logic (Lutz Schröder, Dirk Pattinson, Tadeusz Litak), In Journal of Logic and Computation, vol. 27(3), pp. 749–773, 2017. [preprint] [bib] [pdf]
[30] Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion (Stefan Milius, Tadeusz Litak), In Fundamenta Informaticae, vol. 150, pp. 407–449, 2017. (special issue FiCS'13 edited by David Baelde, Arnaud Carayol, Ralph Matthes and Igor Walukiewicz) [bib] [pdf] [doi]
[29] Model Theory and Proof Theory of CPL (Tadeusz Litak, Dirk Pattinson, Katsuhiko Sano, Lutz Schröder), In Logical Methods in Computer Science, 2017. (accepted to a special issue in honor of Jiří Adámek, to appear) [bib] [pdf]
[28] Negative Translations and Normal Modality (Tadeusz Litak, Miriam Polzer, Ulrich Rabenstein), In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (Dale Miller, ed.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 84, pp. 27:1–27:18, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2017. ( [Local copy] ) [bib] [pdf] [doi]
[27] An Algebraic Glimpse at Bunched Implications and Separation Logic (Peter Jipsen, Tadeusz Litak), In CoRR, vol. abs/1709.07063, 2017. [bib] [pdf]
[26] Complete Additivity and Modal Incompleteness (Wesley H. Holliday, Tadeusz Litak), In Review of Symbolic Logic, 2017. (to appear) [bib] [pdf]
[25] Relational lattices: From databases to universal algebra (Tadeusz Litak, Szabolcs Mikulás, Jan Hidders), In JLAMP, vol. 85(4), pp. 540–573, 2016. The final publication is available at Springer via http://dx.doi.org/10.1016/j.jlamp.2015.11.008 (special issue with selected papers RAMiCS 2014 edited by Peter Höfner, Peter Jipsen, Wolfram Kahl and Martin E. Müller) [bib] [pdf] [doi]
[24] Relational Lattices (Tadeusz Litak, Szabolcs Mikulás, Jan Hidders), In Relational and Algebraic Methods in Computer Science 2014 (RAMiCS) (Peter Höfner, Peter Jipsen, Wolfram Kahl, Martin E. Müller, eds.), Lecture Notes in Computer Science, vol. 8428, pp. 327–343, Springer International Publishing, 2014. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-06251-8_20. (Superseded by the journal version in the special issue of JLAMP with selected papers of RAMiCS 2014) [bib] [pdf] [doi]
[23] Constructive modalities with provability smack (Tadeusz Litak), Chapter in Leo Esakia on duality in modal and intuitionistic logics (Guram Bezhanishvili, ed.), Outstanding Contributions to Logic, vol. 4, pp. 179–208, Springer, 2014. The final publication is available at Springer via http://dx.doi.org/10.1007/978-94-017-8860-1_8. [bib] [pdf] [doi]
[22] Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion (Stefan Milius, Tadeusz Litak), In FICS (David Baelde, Arnaud Carayol, eds.), EPTCS, vol. 126, pp. 72–86, 2013. (Superseded by the journal version invited to FI) [bib] [pdf]
[21] Coalgebraic Predicate Logic: Equipollence Results and Proof Theory (Tadeusz Litak, Dirk Pattinson, Katsuhiko Sano), Chapter in Logic, Language, and Computation. Revised Selected Papers of TbiLLC 2011 (Guram Bezhanishvili, Sebastian Löbner, Vincenzo Marra, Frank Richter, eds.), Lecture Notes in Computer Science, vol. 7758, pp. 257–276, Springer Berlin Heidelberg, 2013. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-36976-6_16. [bib] [pdf] [doi]
[20] Coalgebraic Predicate Logic (Tadeusz Litak, Dirk Pattinson, Katsuhiko Sano, Lutz Schröder), In Proc. 39th International Colloquium on Automata, Languages, and Programming, ICALP 2012 (Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, Roger Wattenhofer, eds.), Lecture Notes in Computer Science, vol. 7392, pp. 299–311, Springer, 2012. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-31585-5_29. [bib] [pdf] [doi]
[19] Stone duality for nominal Boolean algebras with 'new' (Murdoch Gabbay, Tadeusz Litak, Daniela Petri\csan), Chapter in Algebra and Coalgebra in Computer Science (Andrea Corradini, Bartek Klin, Corina Cîrstea, eds.), Lecture Notes in Computer Science, vol. 6859, pp. 192–207, Springer Berlin Heidelberg, 2011. [bib] [doi]
[18] Complete axiomatizations for XPath fragments (Balder ten Cate, Tadeusz Litak, Maarten Marx), In Journal of Applied Logic, vol. 8(2), pp. 153–172, 2010. (Selected papers from the Logic in Databases Workshop 2008 edited by Andrea Calí, Laks V.S. Lakshmanan and Davide Martinenghi) [bib] [pdf] [doi]
[17] Some Modal Aspects of XPath (Balder ten Cate, Gaëlle Fontaine, Tadeusz Litak), In Journal of Applied Non-Classical Logics, vol. 20(3), pp. 139–171, Taylor & Francis, 2010.
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] (Invited paper to the special 20th anniversary issue) [bib] [pdf]
[16] On the Termination Problem for Declarative XML Message Processing (Tadeusz Litak, Sven Helmer), Chapter in Database and Expert Systems Applications (Sourav S. Bhowmick, Josef Küng, Roland Wagner, eds.), Lecture Notes in Computer Science, vol. 5690, pp. 83–97, Springer Berlin Heidelberg, 2009.
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.
[bib] [pdf] [doi]
[15] Stability of the Blok Theorem (Tadeusz Litak), In Algebra Universalis, vol. 58(4), pp. 385–411, Birkhäuser Verlag Basel, 2008.
The last and most advanced one in the series of papers based on or related to my PhD Thesis. It is also the one which attempts to put the whole research in a broader mathematical context. 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] [bib] [pdf] [doi]
[14] Completions of GBL-algebras: negative results (Tomasz Kowalski, Tadeusz Litak), In Algebra Universalis, vol. 58(4), pp. 373–384, Birkhäuser Verlag Basel, 2008.
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.
[bib] [pdf] [doi]
[13] The importance of being discrete (Balder Ten Cate, Tadeusz Litak), Technical report, Institute for Logic, Language and Computation (ILLC), University of Amsterdam, 2007. [bib] [pdf]
[12] Topological perspective on the hybrid proof rules (Balder ten Cate, Tadeusz Litak), In Electronic Notes in Theoretical Computer Science, vol. 174(6), pp. 79–94, Elsevier, 2007. (Proceedings of the International Workshop on Hybrid Logic HyLo 2006) [bib] [pdf] [doi]
[11] The non-reflexive counterpart of Grz (Tadeusz Litak), In Bulletin of the Section of Logic, vol. 36(3--4), pp. 195–208, 2007. (A special issue In Honorem Hiroakira Ono edited by Piotr Łukowski) [bib] [pdf]
[10] Completions of GBL-algebras and acyclic modal algebras: negative results (Tadeusz Litak, Tomasz Kowalski), vol. 1525, pp. 51–61, Technical report, Research Institute for Mathematical Sciences (RIMS), Kyoto University, 2006.
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.
[bib] [pdf]
[9] Algebraization of Hybrid Logic with Binders (Tadeusz Litak), Chapter in Relations and Kleene Algebra in Computer Science (Renate A. Schmidt, ed.), Lecture Notes in Computer Science, vol. 4136, pp. 281–295, Springer Berlin Heidelberg, 2006.
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] [bib] [pdf] [doi]
Powered by bibtexbrowser