Publications

The list of publications is also available as PDF document.

2022, 2021,
2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012

2022

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann, and Julián Méndez: Evonne: Interactive Proof Visualization for Description Logics (System Description). In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Lecture Notes in Computer Science. Springer, 2022. (to appear)
BibTeX entry Abstract Paper (PDF)

Manfred Droste, Sven Dziadek, and Werner Kuich: Logic for omega-Pushdown Automata. Information and Computation, 282, 2022. Special issue on WATA 2018
BibTeX entry Abstract DOI

Manfred Droste, Sven Dziadek, and Werner Kuich: Greibach Normal Form for omega-Algebraic Systems and Weighted Simple omega-Pushdown Automata. Information and Computation, 285, 2022.
BibTeX entry Abstract DOI

Marco Kuhlmann, Andreas Maletti, and Lena Katharina Schiffer: The tree-generative capacity of combinatory categorial grammars. Journal of Computer and System Sciences, 124:214–233, 2022.
BibTeX entry Abstract DOI ©Elsevier

2021

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures. In André Platzer and Geoff Sutcliffe, editors, Proceedings of the 28th International Conference on Automated Deduction (CADE-28), July 11–16, 2021, Virtual Event, United States, volume 12699 of Lecture Notes in Computer Science, pages 291–308, 2021.
BibTeX entry Abstract Paper (PDF) DOI

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Abstract). In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, Proceedings of the 34th International Workshop on Description Logics (DL 2021) part of Bratislava Knowledge September (BAKS 2021), Bratislava, Slovakia, September 19th to 22nd, 2021, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021.
BibTeX entry Paper (PDF)

Christian Alrabbaa, Stefan Borgwardt, Nina Knieriemen, Alisa Kovtunova, Anna Milena Rothermel, and Frederik Wiehr: In the Hand of the Beholder: Comparing Interactive Proof Visualizations. In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, Proceedings of the 34th International Workshop on Description Logics (DL 2021) part of Bratislava Knowledge September (BAKS 2021), Bratislava, Slovakia, September 19th to 22nd, 2021, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021.
BibTeX entry Abstract Paper (PDF)

Christian Alrabbaa, Stefan Borgwardt, Nina Knieriemen, Alisa Kovtunova, Anna Milena Rothermel, and Frederik Wiehr: In the Hand of the Beholder: Comparing Interactive Proof Visualizations (Extended Abstract). In Informal Proceedings of the Explainable Logic-Based Knowledge Representation (XLoKR 2021) workshop co-located with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), Online Event [Hanoi, Vietnam], November 3rd to 5th, 2021, 2021.
BibTeX entry Paper (PDF)

Christian Alrabbaa, Willi Hieke, and Anni-Yasmin Turhan: Counter Model Transformation For Explaining Non-Subsumption in EL. In Christoph Beierle, Marco Ragni, Frieder Stolzenburg, and Matthias Thimm, editors, Proceedings of the 7th Workshop on Formal and Cognitive Reasoning (FCR-2021) co-located with the 44th German Conference on Artificial Intelligence (KI-2021), volume 2961 of CEUR Workshop Proceedings, pages 9–22. CEUR-WS.org, 2021.
BibTeX entry Abstract Paper (PDF)

Christian Alrabbaa, Willi Hieke, and Anni-Yasmin Turhan: Relevant Parts of Counter Models as Explanations for EL Non-Subsumptions (Extended Abstract). In Informal Proceedings of the 2nd Workshop on Explainable Logic-Based Knowledge Representation (XLoKR-2021) co-located with the 18th international Conference on Principles of Knowledge Representation and Reasoning (KR-2021), 2021.
BibTeX entry Abstract Paper (PDF)

Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch, and Julian Siber: Causality-Based Game Solving. In Computer Aided Verification - 33rd International Conference, CAV 2021, pages 894–917. Springer, 2021.
BibTeX entry Abstract DOI

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell: The Orbit Problem for Parametric Linear Dynamical Systems. In 32nd International Conference on Concurrency Theory, CONCUR 2021, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
BibTeX entry Abstract DOI

Christel Baier, Florian Funke, Simon Jantsch, Jakob Piribauer, and Robin Ziemek: Probabilistic Causes in Markov Chains. In Automated Technology for Verification and Analysis, LNCS. Springer, 2021.
BibTeX entry Abstract DOI

Manuel Bodirsky, Thomas Feller, Simon Knäuer, and Sebastian Rudolph: On Logics and Homomorphism Closure. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.
BibTeX entry DOI

Manuel Bodirsky and Johannes Greiner: Tractable Combinations of Theories via Sampling. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, editors, Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, pages 133–146. Springer International Publishing, 2021.
BibTeX entry Abstract DOI (The final publication is available at link.springer.com)

Manuel Bodirsky and Simon Knäuer: Network Satisfaction for Symmetric Relation Algebras with a Flexible Atom. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 6218–6226. AAAI Press, 2021.
BibTeX entry

Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph: Datalog-Expressibility for Monadic and Guarded Second-Order Logic. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 120:1–120:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
BibTeX entry DOI

Frederic Dörband: Kleene and Büchi Theorems for Weighted Forest Languages over M-Monoids. Special issue of Information and Computation devoted to WATA 2020, 2021. In print
BibTeX entry Abstract DOI

Frederic Dörband, Thomas Feller, and Kevin Stier: Approximated Determinisation of Weighted Tree Automata. In Language and Automata Theory and Applications, pages 255–266. Springer International Publishing, 2021.
BibTeX entry Abstract DOI

Frederic Dörband, Thomas Feller, and Kevin Stier: Sequentiality of Group-Weighted Tree Automata. In Language and Automata Theory and Applications, pages 267–278. Springer International Publishing, 2021.
BibTeX entry Abstract DOI

Willi Hieke, Francesco Kriegel, and Adrian Nuradiansyah: Repairing EL TBoxes by Means of Countermodels Obtained by Model Transformation. In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, Proceedings of the 34th International Workshop on Description Logics (DL 2021), Hybrid Event, Bratislava, Slovakia, September 19–22, 2021, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021.
BibTeX entry Abstract Paper (PDF)

Simon Jantsch, Jakob Piribauer, and Christel Baier: Witnessing Subsystems for Probabilistic Systems with Low Tree Width. In Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF), EPTCS, 2021.
BibTeX entry Abstract DOI

Tobias John, Simon Jantsch, Christel Baier, and Sascha Klüppelholz: Determinization and Limit-Determinization of Emerson-Lei Automata. In Automated Technology for Verification and Analysis, LNCS. Springer, 2021.
BibTeX entry Abstract DOI

Corto Mascle, Christel Baier, Florian Funke, Simon Jantsch, and Stefan Kiefer: Responsibility and verification: Importance value in temporal logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. IEEE, 2021.
BibTeX entry Abstract DOI

Lena Katharina Schiffer and Andreas Maletti: Strong Equivalence of TAG and CCG. Transactions of the Association for Computational Linguistics, 9:707–720, 2021.
BibTeX entry Abstract DOI ©MIT Press

2020

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: Finding Small Proofs for Description Logic Entailments: Theory and Practice. In Elvira Albert and Laura Kovacs, editors, LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 73 of EPiC Series in Computing, pages 32–67. EasyChair, 2020.
BibTeX entry Abstract Paper (PDF) DOI

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: On the Complexity of Finding Good Proofs for Description Logic Entailments. In DL 2020: International Workshop on Description Logics, CEUR-WS. CEUR-WS.org, 2020.
BibTeX entry Abstract Paper (PDF)

Christian Alrabbaa, Franz Baader, Raimund Dachselt, Tamara Flemisch, and Patrick Koopmann: Visualising Proofs and the Modular Structure of Ontologies to Support Ontology Repair. In DL 2020: International Workshop on Description Logics, CEUR-WS. CEUR-WS.org, 2020.
BibTeX entry Abstract Paper (PDF)

Christian Alrabbaa, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: Finding Proofs for Description Logic Entailments in Practice. In Explainable Logic-Based Knowledge Representation (XLoKR 2020), 2020.
BibTeX entry Abstract Paper (PDF)

Franz Baader and Filippo De Bortoli: Description Logics That Count, and What They Can and Cannot Count. In Laura Kovacs, Konstantin Korovin, and Giles Reger, editors, ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia, volume 68 of EPiC Series in Computing, pages 1–25. EasyChair, 2020.
BibTeX entry Abstract DOI

Franz Baader and Filippo De Bortoli: Description Logics that Count, and What They Can and Cannot Count (Extended Abstract). In Stefan Borgwardt and Thomas Meyer, editors, Proceedings of the 33rd International Workshop on Description Logics (DL'20), volume 2663 of CEUR Workshop Proceedings. Online, CEUR-WS, 2020.
BibTeX entry Abstract Paper (PDF)

Franz Baader and Jakub Rydval: Description Logics with Concrete Domains and General Concept Inclusions Revisited. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 413–431. Cham, Springer International Publishing, 2020.
BibTeX entry Abstract Paper (PDF) ©Springer-Verlag

Franz Baader and Jakub Rydval: Description Logics with Concrete Domains and General Concept Inclusions Revisited (Extended Abstract). In Stefan Borgwardt and Thomas Meyer, editors, Proceedings of the 33rd International Workshop on Description Logics (DL'20), volume 2663 of CEUR Workshop Proceedings. Online, CEUR-WS, 2020.
BibTeX entry Abstract Paper (PDF)

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland: Reachability in Dynamical Systems with Rounding. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 36:1–36:17, 2020.
BibTeX entry Abstract DOI

Manuel Bodirsky and Johannes Greiner: The Complexity of Combinations of Qualitative Constraint Satisfaction Problems. Logical Methods in Computer Science, Volume 16, Issue 1, 2020.
BibTeX entry Abstract DOI

Manuel Bodirsky and Simon Knäuer: Hardness of Network Satisfaction for Relation Algebras with Normal Representations. In Relational and Algebraic Methods in Computer Science, pages 31–46. Springer International Publishing, 2020.
BibTeX entry DOI

Manuel Bodirsky, Simon Knäuer, and Florian Starke: ASNP: A Tame Fragment of Existential Second-Order Logic. In Lecture Notes in Computer Science, pages 149–162. Springer International Publishing, 2020.
BibTeX entry Paper (PDF) DOI

Manuel Bodirsky, Wied Pakusa, and Jakub Rydval: Temporal Constraint Satisfaction Problems in Fixed-Point Logic. In Proceedings of the Symposium on Logic in Computer Science (LICS 2020), pages 237–251. New York, NY, USA, Association for Computing Machinery, 2020.
BibTeX entry Abstract Paper (PDF) DOI

Manfred Droste, Sven Dziadek, and Werner Kuich: Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), volume 182 of LIPIcs, pages 44:1–44:14, 2020.
BibTeX entry Abstract DOI

Tamara Flemisch, Ricardo Langner, Christian Alrabbaa, and Raimund Dachselt: Towards Designing a Tool For Understanding Proofs in Ontologies through Combined Node-Link Diagrams. In Valentina Ivanova, Patrick Lambrix, Catia Pesquita, and Vitalis Wiens, editors, Proceedings of the Fifth International Workshop on Visualization and Interaction for Ontologies and Linked Data co-located with the 19th International Semantic Web Conference (ISWC 2020), Virtual Conference (originally planned in Athens, Greece), November 02, 2020, volume 2778 of CEUR Workshop Proceedings, pages 28–40. CEUR-WS.org, 2020.
BibTeX entry Abstract Paper (PDF)

Florian Funke, Simon Jantsch, and Christel Baier: Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, pages 324–345. Cham, Springer International Publishing, 2020.
BibTeX entry Abstract DOI

Willi Hieke and Anni-Yasmin Turhan: Towards Model Transformation in Description Logics — Investigating the Case of Transductions. In Christoph Beierle, Marco Ragni, Frieder Stolzenburg, and Matthias Thimm, editors, Proceedings of the 6th Workshop on Formal and Cognitive Reasoning (FCR-2020) co-located with 43rd German Conference on Artificial Intelligence (KI-2020), volume 2680 of CEUR Workshop Proceedings, pages 69–82. CEUR-WS.org, 2020.
BibTeX entry Abstract Paper (PDF)

Simon Jantsch, Florian Funke, and Christel Baier: Minimal Witnesses for Probabilistic Timed Automata. In Automated Technology for Verification and Analysis (ATVA), 2020.
BibTeX entry Abstract DOI

Simon Jantsch, Hans Harder, Florian Funke, and Christel Baier: SWITSS: Computing Small Witnessing Subsystems. In 20th Conference on Formal Methods in Computer-Aided Design - FMCAD 2020, pages 236–244. TU Wien Academic Press, 2020.
BibTeX entry Paper (PDF) DOI

Erik Paul: Finite Sequentiality of Finitely Ambiguous Max-Plus Tree Automata. In 47th International Colloquium on Automata, Languages, and Programming (ICALP), pages 137:1–137:15, 2020. Track B Best Student Paper Award
BibTeX entry

Jakob Piribauer and Christel Baier: On Skolem-Hardness and Saturation Points in Markov Decision Processes. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of Leibniz International Proceedings in Informatics (LIPIcs), pages 138:1–138:17. Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2020.
BibTeX entry Abstract DOI

2019

Christian Alrabbaa, Patrick Koopmann, and Anni-Yasmin Turhan: Practical Query Rewriting for DL-Lite with Numerical Predicates. In Diego Calvanese and Luca Iocchi, editors, GCAI 2019. Proceedings of the 5th Global Conference on Artificial Intelligence, volume 65 of EPiC Series in Computing, pages 15–27. EasyChair, 2019.
BibTeX entry Abstract Paper (PDF) Extended technical report (PDF) DOI

Shima Asaadi, Saif M. Mohammad, and Svetlana Kiritchenko: Big BiRD: A Large, Fine-Grained, Bigram Relatedness Dataset for Examining Semantic Composition. In In Proceedings of the North American Chapter of the Association for Computational Linguistics (NAACL-2019), 2019.
BibTeX entry

Franz Baader and Filippo De Bortoli: On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets. In Andreas Herzig and Andrei Popescu, editors, Proc. of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019), volume 11715 of Lecture Notes in Computer Science, pages 203–219. Springer, 2019.
BibTeX entry Abstract Paper (PDF) DOI (The final publication is available at link.springer.com) ©Springer Nature Switzerland AG 2019

Franz Baader, Oliver Fernández Gil, and Pavlos Marantidis: Matching in the Description Logic FL0 with respect to General TBoxes (Extended abstract). In Mantas Simkus and Grant Weddell, editors, Proceedings of the 32nd International Workshop on Description Logics (DL'19), volume 2373 of CEUR Workshop Proceedings. CEUR-WS, 2019.
BibTeX entry Abstract Paper (PDF)

Christel Baier, Nathalie Bertrand, Jakob Piribauer, and Ocan Sankur: Long-run Satisfaction of Path Properties. In Proceedings of the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'19), pages 1–14. IEEE, 2019.
BibTeX entry Abstract DOI

Frederic Dörband, Zoltán Fülöp, and Heiko Vogler: Kleene and Büchi Theorems for Weighted Forest Languages over M-Monoids. Special issue of Information and Computation devoted to CAI 2019, 2019. Accepted
BibTeX entry Abstract

Manfred Droste, Sven Dziadek, and Werner Kuich: Greibach Normal Form for omega-Algebraic Systems and Weighted Simple omega-Pushdown Automata. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), volume 150 of LIPIcs, pages 38:1–38:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019.
BibTeX entry Abstract Paper (PDF) DOI

Manfred Droste, Sven Dziadek, and Werner Kuich: Weighted simple reset pushdown automata. Theoretical Computer Science, 777:252–259, 2019.
BibTeX entry Abstract DOI

Simon Jantsch, David Müller, Christel Baier, and Joachim Klein: From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods The Next 30 Years, Lecture Notes in Computer Science, pages 262–279. Cham, Springer International Publishing, 2019.
BibTeX entry Abstract Paper (PDF) Extended technical report (PDF) DOI

Marco Kuhlmann, Andreas Maletti, and Lena Katharina Schiffer: The Tree-Generative Capacity of Combinatory Categorial Grammars. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), volume 150 of Leibniz International Proceedings in Informatics (LIPIcs), pages 44:1–44:14. Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2019.
BibTeX entry Abstract Paper (PDF) DOI

Rolf Niedermeier and Christophe Paul, editors: 36th International Symposium on Theoretical Aspects of Computer Science (STACS), volume 126 of in Leibniz International Proceedings in Informatics (LIPIcs), 2019.
BibTeX entry

Erik Paul: Finite Sequentiality of Unambiguous Max-Plus Tree Automata. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 55:1–55:17, 2019.
BibTeX entry

Jakob Piribauer and Christel Baier: Partial and conditional expectations in Markov decision processes with integer weights. In Mikolaj Bojanczyk and Alex Simpson, editors, Proceedings of the 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'19), volume 11425 of LNCS, pages 436–452. Springer, 2019.
BibTeX entry Abstract

Markus Ulbricht: Repairing Non-monotonic Knowledge Bases. In Francesco Calimeri, Nicola Leone, and Marco Manna, editors, Logics in Artificial Intelligence, pages 151–167. Cham, Springer International Publishing, 2019.
BibTeX entry Abstract

2018

Christian Alrabbaa, Sebastian Rudolph, and Lukas Schweizer: Faceted Answer-Set Navigation. In Christoph Benzmüller and Francesco Ricca and Xavier Parent and Dumitru Roman, editors, Proceedings of Rules and Reasoning - Second International Joint Conference, RuleML+RR 2018, volume 11092 of Lecture Notes in Computer Science, pages 211–225. Springer, 2018.
BibTeX entry Abstract Paper (PDF)

Franz Baader, Oliver Fernández Gil, and Pavlos Marantidis: Matching in the Description Logic FL0 with respect to General TBoxes. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, pages 76–94. EasyChair, 2018.
BibTeX entry Abstract Paper (PDF) DOI

Franz Baader, Oliver Fernández Gil, and Maximilian Pensel: Standard and Non-Standard Inferences in the Description Logic FL₀ Using Tree Automata. In Daniel Lee, Alexander Steen, and Toby Walsh, editors, GCAI 2018, 4th Global Conference on Artificial Intelligence, Luxembourg, September 2018., volume 55 of EPiC Series in Computing, pages 1–14. EasyChair, 2018.
BibTeX entry Abstract Paper (PDF) DOI

Franz Baader, Pavlos Marantidis, and Antoine Mottet: ACUI Unification modulo Ground Theories. In Mauricio Ayala-Rincón and Philippe Balbiani, editors, Proceedings of the 32th International Workshop on Unification (UNIF 2018), 2018.
BibTeX entry Abstract Paper (PDF)

Franz Baader, Pavlos Marantidis, and Maximilian Pensel: The Data Complexity of Answering Instance Queries in FL₀. In Proc. of the Reasoning on Data Workshop (RoD'18), Companion of the The Web Conference 2018, pages 1603–1607. ACM, 2018.
BibTeX entry Abstract Paper (PDF) DOI

Parvaneh Babari, Manfred Droste, and Vitaly Perevoshchikov: Weighted register automata and weighted logic on data words. Theoretical Computer Science, 744:3–21, 2018.
BibTeX entry Abstract DOI

Ringo Baumann and Markus Ulbricht: If Nothing Is Accepted - Repairing Argumentation Frameworks. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018., pages 108–117, 2018.
BibTeX entry Abstract

Manuel Bodirsky and Johannes Greiner: Complexity of Combinations of Qualitative Constraint Satisfaction Problems. In Didier, Galmiche, Stephan, Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning (IJCAR), volume 10900 of Lecture Notes in Computer Science, pages 263–278. Springer International Publishing, 2018.
BibTeX entry Abstract DOI (The final publication is available at link.springer.com)

Manuel Bodirsky, Peter Jonsson, Barnaby Martin, and Antoine Mottet: Classification Transfer for Qualitative Reasoning Problems. In Proceedings of IJCAI'18, 2018.
BibTeX entry

Manuel Bodirsky, Florent Madelaine, and Antoine Mottet: A universal-algebraic proof of the dichotomy for Monotone Monadic SNP. In Proceedings of LICS'18, pages 105–114, 2018.
BibTeX entry DOI

Manuel Bodirsky, Marcello Mamino, Barnaby Martin, and Antoine Mottet: The complexity of disjunctive linear Diophantine constraints. In Proceedings of MFCS'18, 2018.
BibTeX entry

Manuel Bodirsky, Marcello Mamino, and Caterina Viola: Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:22. Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.
BibTeX entry Paper (PDF) DOI

Manuel Bodirsky and Antoine Mottet: A Dichotomy for First-Order Reducts of Unary Structures. Logical Methods in Computer Science, Volume 14, Issue 2, 2018.
BibTeX entry DOI

Gerhard Brewka, Matthias Thimm, and Markus Ulbricht: Strong inconsistency. Artificial Intelligence, 267:78–117, 2018.
BibTeX entry Abstract DOI

Manfred Droste and Erik Paul: A Feferman-Vaught decomposition theorem for weighted MSO logic. In Proceedings of MFCS'18, 2018.
BibTeX entry

Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, and David Müller: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer (STTT), 20(2):179–194, 2018.
BibTeX entry Abstract

Maximilian Pensel and Anni-Yasmin Turhan: Reasoning in the Defeasible Description Logic EL—Computing Standard Inferences under Rational and Relevant Semantics. International Journal of Approximate Reasoning (IJAR), 103:28–70, 2018.
BibTeX entry Abstract DOI

Markus Ulbricht, Matthias Thimm, and Gerhard Brewka: Measuring Strong Inconsistency. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI'18), pages 1989–1996. AAAI Press, February 2018.
BibTeX entry Abstract

2017

Shima Asaadi and Sebastian Rudolph: Gradual Learning of Matrix-Space Models of Language for Sentiment Analysis. In Proceedings of the 2nd Workshop on Representation Learning for NLP, pages 178–185, 2017.
BibTeX entry Paper (PDF)

Franz Baader and Oliver Fernández Gil: Decidability and Complexity of Threshold Description Logics Induced by Concept Similarity Measures. In Proceedings of the 32nd Annual ACM Symposium on Applied Computing, Marrakech, Morocco, April 4-6, 2017, pages 983–988. ACM, 2017.
BibTeX entry Abstract

Franz Baader, Oliver Fernández Gil, and Pavlos Marantidis: Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in FL₀. In Frank Drewes, Carlos Martín-Vide, and Bianca Truthe, editors, Proceedings of the 11th International Conference on Language and Automata Theory and Applications (LATA 2017), volume 10168 of Lecture Notes in Computer Science, pages 3–26. Springer, 2017.
BibTeX entry Abstract Paper (PDF) DOI

Franz Baader and Pavlos Marantidis: Language equations for approximate matching in the Description Logic FL0. In Adrià Gascón and Christopher Lynch, editors, Proceedings of the 31st International Workshop on Unification (UNIF'17), 2017.
BibTeX entry Abstract Paper (PDF)

Manuel Bodirsky, Barnaby Martin, and Antoine Mottet: Discrete Temporal Constraint Satisfaction Problems. Journal of the ACM, 2017. Accepted for publication in the Journal of the ACM.
BibTeX entry

Gerhard Brewka, Matthias Thimm, and Markus Ulbricht: Strong Inconsistency in Nonmonotonic Reasoning. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pages 901–907, 2017.
BibTeX entry Abstract Paper (PDF) DOI

Manfred Droste and Stefan Dück: Weighted Automata and Logics for Infinite Nested Words. Inf. Comp., 253, Part 3:448–466, 2017.
BibTeX entry DOI

Manfred Droste, Stefan Dück, Dino Mandrioli, and Matteo Pradella: Weighted Operator Precedence Languages. In Proceedings of MFCS'17, pages 31:1–31:15, 2017.
BibTeX entry

Andreas Ecke: Quantitative Methods for Similarity in Description Logics. Künstliche Intelligenz, 2017. To appear
BibTeX entry

Luisa Herrmann: A Medvedev Characterization of Recognizable Tree Series. In Émilie Charlier, Julien Leroy, and Michel Rigo, editors, Proc. 21th Int. Conf. on Developments in Language Theorie (DLT 2017), pages 210–221. Cham, Springer International Publishing, 2017.
BibTeX entry DOI

David Müller and Salomon Sickert: LTL to Deterministic Emerson-Lei Automata. In 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), volume 256 of Electronic Proceedings of Theoretical Computer Science, pages 180–194. Open Publishing Association, 2017.
BibTeX entry Abstract Paper (PDF)

Erik Paul: Monitor logics for quantitative monitor automata. In Proceedings of MFCS'17, 2017.
BibTeX entry

Erik Paul: The equivalence, unambiguity and sequentiality problems of finitely ambiguous max-plus tree automata are decidable. In Proceedings of MFCS'17, 2017.
BibTeX entry

Maximilian Pensel and Anni-Yasmin Turhan: Including Quantification in Defeasible Reasoning for the Description Logic EL_bot. In Marcello Balduccini and Tomi Janhunen, editors, Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning - LPNMR, pages 78–84. Springer, 2017.
BibTeX entry Abstract Paper (PDF) DOI

Maximilian Pensel and Anni-Yasmin Turhan: Making Quantification Relevant again—the case of Defeasible EL_bot. In Richard Booth, Giovanni Casini, and Ivan Varzinczak, editors, Proceedings of the 4th International Workshop on Defeasible and Ampliative Reasoning - DARe. CEUR-WS.org, 2017.
BibTeX entry Abstract Paper (PDF)

2016

Shima Asaadi and Sebastian Rudolph: On the Correspondence between Compositional Matrix-Space Models of Language and Weighted Automata. In Proceedings of the SIGFSM Workshop on Statistical NLP and Weighted Automata, pages 70–74, 2016.
BibTeX entry Paper (PDF)

Franz Baader and Andreas Ecke: Reasoning with Prototypes in the Description Logic ALC using Weighted Tree Automata. In Proceedings of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016), Lecture Notes in Computer Science, pages 63–75. Springer-Verlag, 2016.
BibTeX entry Abstract Paper (PDF)

Franz Baader and Oliver Fernández Gil: Extending the Description Logic tel(deg) with Acyclic TBoxes. In ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), volume 285 of Frontiers in Artificial Intelligence and Applications, pages 1096–1104. IOS Press, 2016.
BibTeX entry Abstract Paper (PDF)

Franz Baader, Pavlos Marantidis, and Alexander Okhotin: Approximate Unification in the Description Logic FL₀. In Loizos Michael and Antonis C. Kakas, editors, Proc. of the 15th Eur. Conf. on Logics in Artificial Intelligence (JELIA 2016), volume 10021 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2016.
BibTeX entry

P. Babari and N. Schweikardt: +Omega-Picture Languages Recognizable by Büchi-Tiling Systems. In Proc. of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016), Lecture Notes in Computer Science, pages 76–88. Springer, 2016.
BibTeX entry

Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klueppelholz, David Müller, and James Worrell: Markov Chains and Unambiguous Büchi Automata. In 28th International Conference on Computer Aided Verification, Lecture Notes in Computer Science. Springer, 2016. to appear
BibTeX entry

Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier, and Sascha Wunderlich: Greener Bits: Formal Analysis of Demand Response. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Proc. of the 14th Int. Symp. on Automated Technology for Verification and Analysis (ATVA 2016), volume 9938 of Lecture Notes in Computer Science, pages 323–339. Springer-Verlag, 2016.
BibTeX entry

Manuel Bodirsky, Victor Dalmau, Barnaby Martin, Antoine Mottet, and Michael Pinsker: Distance Constraint Satisfaction Problems. Information and Computation, 247:87–105, 2016.
BibTeX entry DOI

Manuel Bodirsky and Antoine Mottet: Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction. In Proceedings of the Thirty-First Annual Symposium on Logic in Computer Science (LICS), pages 623–632, 2016.
BibTeX entry DOI

Claudia Carapelle, Shiguang Feng, Alexander Kartzow, and Markus Lohrey: Satisfiability of ECTL^* with local tree constraints. Theory of Computing Systems, 2016. Zur VerÃ¶ffentlichung angenommen.
BibTeX entry

Claudia Carapelle and Anni-Yasmin Turhan: Description Logics Reasoning w.r.t. general TBoxes is decidable for Concrete Domains with the EHD-property. In Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke Hüllermeier, Virginia Dignum, Frank Dignum, and Frank van Harmelen, editors, Proceedings of the 22nd European Conference on Artificial Intelligence, pages 1440–1448. Dresden, Germany, IOS Press, 2016.
BibTeX entry Abstract Paper (PDF) DOI

M. Droste and V. Perevoshchikov: Multi-weighted automata and MSO logic. Theory of Computing Systems, 2016. DOI: 10.1007/s00224-015-9658-9. Accepted for publication.
BibTeX entry

Manfred Droste, Zoltán Fülöp, and Doreen Götze: A Kleene Theorem for Weighted Tree Automata over Tree Valuation Monoids. In Proc. of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016), Lecture Notes in Computer Science, pages 452–463, 2016.
BibTeX entry

Stefan Dück: Weighted Automata and Logics on Infinite Graphs. In Proceedings of the 20th International Conference on Developments in Language Theory (DLT 2016), volume 9840 of LNCS, pages 151–163. Springer, 2016.
BibTeX entry

Daniel Gburek, Christel Baier, and Sascha Klüppelholz: Composition of Stochastic Transition Systems Based on Spans and Couplings. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, Proc. of the 43rd Int. Coll. on Automata, Languages and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics, pages 102:1–102:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016.
BibTeX entry

Luisa Herrmann and Heiko Vogler: Weighted Symbolic Automata with Data Storage. In Srecko Brlek and Christophe Reutenauer, editors, Proc. of the 20th Int. Conf. on Developments in Language Theory (DLT 2016), volume 9840 of Lecture Notes in Computer Science, pages 203–215. Springer-Verlag, 2016.
BibTeX entry

Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, and David Müller: Advances in Symbolic Probabilistic Model Checking with PRISM. In Proc. of the 22th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 9636 of Lecture Notes in Computer Science, pages 349–366. Springer, 2016.
BibTeX entry Abstract

Mark-Jan Nederhof, Markus Teichmann, and Heiko Vogler: Non-Self-Embedding Linear Context-Free Tree Grammars Generate Regular Tree Languages. Journal of Automata, Languages and Combinatorics, 2016. To appear
BibTeX entry

Johannes Osterholzer, Toni Dietze, and Luisa Herrmann: Linear Context-Free Tree Languages and Inverse Homomorphisms. In Proc. of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016), Lecture Notes in Computer Science, pages 478–489. Springer-Verlag, 2016.
BibTeX entry

Erik Paul: On Finite and Polynomial Ambiguity of Weighted Tree Automata. In Proceedings of the 20th International Conference on Developments in Language Theory (DLT 2016), volume 9840 of LNCS, pages 368–379. Springer, 2016.
BibTeX entry DOI

Markus Teichmann: Regular Approximation of Weighted Linear Nondeleting Context-Free Tree Languages. In Proceedings of the 21st International Conference on Implementation and Application of Automata (CIAA), volume 9705 of Lecture Notes in Computer Science, pages 1–12, 2016.
BibTeX entry DOI

Markus Ulbricht, Matthias Thimm, and Gerhard Brewka: Measuring Inconsistency in Answer Set Programs. In Loizos Michael and Antonis Kakas, editors, Logics in Artificial Intelligence: 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings, pages 577–583. Cham, Springer International Publishing, 2016.
BibTeX entry DOI

Heiko Vogler, Manfred Droste, and Luisa Herrmann: A Weighted MSO Logic with Storage Behaviour and its Büchi-Elgot-Trakhtenbrot Theorem. In Proc. of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016), Lecture Notes in Computer Science, pages 127–139. Springer-Verlag, 2016.
BibTeX entry Abstract

2015

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporal Query Entailment in the Description Logic SHQ. Journal of Web Semantics, 33:71–93, 2015.
BibTeX entry Abstract DOI

Franz Baader, Gerhard Brewka, and Oliver Fernández Gil: Adding Threshold Concepts to the Description Logic EL. In Carsten Lutz and Silvio Ranise, editors, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), volume 9322 of Lectures Notes in Artificial Intelligence, pages 33–48. Wroclaw, Poland, Springer-Verlag, 2015.
BibTeX entry Abstract Paper (PDF) Extended technical report (PDF)

P. Babari and M. Droste: A Nivat theorem for weighted picture automata and weighted MSO logics. In Language and Automata Theory and Applications (LATA 2015), volume 8977 of LNCS, pages 703–715. Springer, 2015.
BibTeX entry

Tomas Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretinsky, David Müller, David Parker, and Jan Strejcek: The Hanoi Omega-Automata Format. In 27th International Conference on Computer Aided Verification (CAV), volume 9206 of Lecture Notes in Computer Science, pages 479–486, 2015.
BibTeX entry Abstract ©Springer-Verlag

Manuel Bodirsky, Barnaby Martin, and Antoine Mottet: Constraint Satisfaction Problems over the Integers with Successor. In Magnús M. Halldórsson, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming (ICALP 2015), volume 9134 of LNCS, pages 256–267. Springer-Verlag Berlin Heidelberg, 2015.
BibTeX entry (The final publication is available at link.springer.com)

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporalizing Rewritable Query Languages over Knowledge Bases. Journal of Web Semantics, 33:50–70, 2015.
BibTeX entry Abstract DOI

C. Carapelle, S. Feng, A. Kartzow, and M. Lohrey: Satisfiability of ECTL* with tree constraints. In 10th International Computer Science Symposium in Russia (CSR 2015), volume 9139 of LNCS, pages 94–108. Springer, 2015.
BibTeX entry

Claudia Carapelle and Markus Lohrey: Temporal Logics with Local Constraints (Invited Contribution). In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2–13. Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.
BibTeX entry DOI

M. Droste and S. Dück: Weighted automata and logics on graphs. In Proceedings of the 40th Conference on Mathematical Foundations of Computer Science (MFCS 2015), Part I, volume 9234 of LNCS, pages 192–204. Springer, 2015.
BibTeX entry

M. Droste and D. Heusel: The supports of weighted unranked tree automata. Fundamenta Informaticae, 136:37–58, 2015.
BibTeX entry

M. Droste and V. Perevoshchikov: A logical characterization of timed pushdown languages. In 10th International Computer Science Symposium in Russia (CSR 2015), volume 9139 of LNCS, pages 189–203. Springer, 2015.
BibTeX entry

M. Droste and V. Perevoshchikov: Logics for weighted timed pushdown automata. In A Symposium on Logic in Computer Science celebrating Yuri Gurevich's 75th birthday (YURIFEST 2015), LNCS, pages 153–173. Springer, 2015.
BibTeX entry

Manfred Droste, Doreen Heusel, and Heiko Vogler: Weighted Unranked Tree Automata over Tree Valuation Monoids and Their Characterization by Weighted Logics. In Andreas Maletti, editor, Algebraic Informatics, volume 9270 of Lecture Notes in Computer Science, pages 90–102. Springer International Publishing, 2015.
BibTeX entry Abstract DOI

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Similarity-based Relaxed Instance Queries. Journal of Applied Logic, 13(4, Part 1):480–508, 2015. Special Issue for the Workshop on Weighted Logics for AI 2013
BibTeX entry Abstract Paper (PDF) DOI

Andreas Ecke, Maximilian Pensel, and Anni-Yasmin Turhan: ELASTIQ: Answering Similarity-threshold Instance Queries in EL. In Diego Calvanese and Boris Konev, editors, Proceedings of the 28th International Workshop on Description Logics (DL-2015), volume 1350 of CEUR Workshop Proceedings. CEUR-WS.org, June 2015.
BibTeX entry Abstract Paper (PDF)

S. Feng, M. Lohrey, and K. Quaas: Path checking for MTL and TPTL over data words. In 19th International Conference on Developments in Language Theory (DLT 2015), volume 9168 of LNCS, pages 326–339. Springer, 2015.
BibTeX entry

Zoltán Fülöp and Heiko Vogler: Characterizations of recognizable weighted tree languages by logic and bimorphisms. Soft Computing1–12, 2015.
BibTeX entry Abstract DOI

Zoltán Fülöp and Heiko Vogler: Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics.. Theoretical Computer Science, 594:82–105, 2015.
BibTeX entry Abstract DOI

Kilian Gebhardt and Johannes Osterholzer: A direct link between Tree-Adjoining and Context-Free Tree Grammars. In Thomas Hanneforth and Christian Wurm, editors, Proceedings of the 12th International Conference on Finite-State Methods and Natural Language Processing (FSMNLP), 2015.
BibTeX entry Abstract

Oliver Fernandez Gil, Franz Baader, and Gerhard Brewka: Adding Threshold Concepts to the Description Logic EL. In Proceedings of the 28th International Workshop on Description Logics, Athens,Greece, June 7-10, 2015., 2015.
BibTeX entry Abstract

Luisa Herrmann and Heiko Vogler: A Chomsky-Schützenberger Theorem for Weighted Automata with Storage. In Andreas Maletti, editor, Proceedings of the 6th International Conference on Algebraic Informatics (CAI 2015), pages 115–127. Springer International Publishing Switzerland, 2015.
BibTeX entry Abstract

Daniel Krähmann, Jana Schubert, Christel Baier, and Clemens Dubslaff: Ratio and Weight Quantiles. In 40th International Symposium on Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science, pages 344–356. Springer Berlin Heidelberg, 2015.
BibTeX entry DOI

Johannes Osterholzer: Complexity of Uniform Membership of Context-Free Tree Grammars. In Andreas Maletti, editor, Proceedings of the 6th International Conference on Algebraic Informatics (CAI 2015), pages 176–188, 2015.
BibTeX entry

V. Perevoshchikov: Weight assignment logic. In 19th International Conference on Developments in Language Theory (DLT 2015), volume 9168 of LNCS, pages 413–425. Springer, 2015.
BibTeX entry

Markus Teichmann and Johannes Osterholzer: A link between multioperator and tree valuation automata and logics. Theoretical Computer Science, 594:106–119, 2015.
BibTeX entry Abstract DOI

Thomas Weidner: Probabilistic Regular Expressions and MSO Logic on Finite Trees. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), volume 45 of Leibniz International Proceedings in Informatics (LIPIcs), pages 503–516. Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.
BibTeX entry DOI

2014

Franz Baader and Marcel Lippmann: Runtime Verification Using the Temporal Description Logic ALC-LTL Revisited. Journal of Applied Logic, 12(4):584–613, 2014.
BibTeX entry Abstract DOI

Christel Baier, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich: Probabilistic Model Checking for Energy-Utility Analysis. In Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, pages 96–123. Springer, 2014.
BibTeX entry

Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, Marcus Daum, Joachim Klein, Steffen Märcker, and Sascha Wunderlich: Probabilistic Model Checking and Non-standard Multi-objective Reasoning. In Proc. of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE), volume 8411 of Lecture Notes in Computer Science, pages 1–16. Springer, 2014.
BibTeX entry Abstract

Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, and Linda Leuschner: Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking. In Proc. of the 35th Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS), volume 8489 of Lecture Notes in Computer Science, pages 20–39. Springer, 2014.
BibTeX entry Abstract

Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich: Weight Monitoring with Linear Temporal Logic: Complexity and Decidability. In Proc. of the 23rd Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS), pages 11:1–11:10. ACM, 2014.
BibTeX entry Abstract

Stefan Borgwardt, Felix Distel, and Rafael Peñaloza: Decidable Gödel description logics without the finitely-valued model property. In Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR'14), pages 228–237. Vienna, Austria, AAAI Press, 2014.
BibTeX entry Abstract Paper (PDF)

Stefan Borgwardt and Rafael Peñaloza: Consistency Reasoning in Lattice-Based Fuzzy Description Logics. International Journal of Approximate Reasoning, 2014.
BibTeX entry Abstract Paper (PDF) DOI

Claudia Carapelle, Shiguang Feng, Oliver Fernández Gil, and Karin Quaas: Satisfiability for MTL and TPTL over Non-monotonic Data Words. In Adrian-Horia Dediu, Carlos Martin-Víde, José-Luis Sierra-Rodríguez, and Bianca Truthe, editors, Language and Automata Theory and Applications, volume 8370 of Lecture Notes in Computer Science, pages 248–259. Springer International Publishing, 2014.
BibTeX entry Paper (PDF) DOI

Claudia Carapelle, Shiguang Feng, Oliver Fernandez Gil, and Karin Quaas: On the Expressiveness of TPTL and MTL over omega-Data Words. In Zoltán É and Zoltán Fülöp, editors, Proceedings 14th International Conference on Automata and Formal Languages, AFL 2014, Szeged, Hungary, May 27-29, 2014, volume 151 of EPTCS, pages 174–187, 2014.
BibTeX entry Paper (PDF)

M. Droste and V. Perevoshchikov: A Nivat theorem for weighted timed automata and weighted relative distance logic. In 35th Int. Colloq. on Automata, Languages, and Programming (ICALP 2014), volume 8573 of LNCS, pages 171–182. Springer, 2014.
BibTeX entry

Manfred Droste and Stefan Dück: Weighted Automata and Logics for Infinite Nested Words. In Adrian Horia Dediu, Carlos Martín-Vide, José Luis Sierra-Rodríguez, and Bianca Truthe, editors, 8th International Conference on Language and Automata Theory and Application (LATA), volume 8370 of Lecture Notes in Computer Science, pages 323–334. Madrid, Spain, Springer, 2014.
BibTeX entry

Manfred Droste and Heiko Vogler: The Chomsky-Schützenberger Theorem for Quantitative Context-Free Languages. International Journal of Foundations of Computer Science, 25(8):955–969, 2014.
BibTeX entry Abstract DOI

Andreas Ecke: Similarity-based Relaxed Instance Queries in EL⁺⁺. In Thomas Lukasiewicz, Rafael Peñaloza, and Anni-Yasmin Turhan, editors, Proceedings of the First Workshop on Logics for Reasoning about Preferences, Uncertainty, and Vagueness, volume 1205 of CEUR Workshop Proceedings, pages 101–113. CEUR-WS.org, 2014.
BibTeX entry Abstract Paper (PDF)

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Answering Instance Queries Relaxed by Concept Similarity. In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR'14), pages 248–257. Vienna, Austria, AAAI Press, 2014.
BibTeX entry Abstract Paper (PDF)

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Completion-based Generalization Inferences for the Description Logic ELOR with Subjective Probabilities. International Journal of Approximate Reasoning, 55(9):1939–1970, 2014.
BibTeX entry Abstract Paper (PDF) DOI

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Mary, What's Like All Cats?. In Proceedings of the 27th International Workshop on Description Logics (DL-2014), July 2014. Extended Abstract
BibTeX entry Paper (PDF)

Oliver Fernández Gil: On the Non-Monotonic Description Logic ALC+Tmin. In Proceedings of the 15th International Workshop on Non-Monotonic Reasoning (NMR'14), pages 114–122, 2014.
BibTeX entry Abstract Paper (PDF)

Joachim Klein, David Müller, Christel Baier, and Sascha Klüppelholz: Are Good-for-Games Automata Good for Probabilistic Model Checking?. In Adrian Horia Dediu, Carlos Mart\'ın-Vide, José Luis Sierra-Rodr\'ıguez, and Bianca Truthe, editors, Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, volume 8370 of Lecture Notes in Computer Science, pages 453–465. Springer, 2014.
BibTeX entry

Johannes Osterholzer: Pushdown Machines for Weighted Context-Free Tree Translation. In Proceedings of 19th International Conference on Implementation and Application of Automata (CIAA 2014), pages 290–303, 2014.
BibTeX entry Abstract DOI

Thomas Weidner: Probabilistic Omega-Regular Expressions. In Adrian-Horia Dediu, Carlos Martín-Vide, José-Luis Sierra-Rodríguez, and Bianca Truthe, editors, Language and Automata Theory and Applications, volume 8370 of Lecture Notes in Computer Science, pages 588–600. Springer International Publishing, 2014.
BibTeX entry DOI ©Springer-Verlag

2013

Ignasi Ab\'ıo, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodr\'ıguez-Carbonell: A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. In 19th International Conference on Principles and Practice of Constraint Programming, CP'13, 2013.
BibTeX entry

Ignasi Ab\'ıo, Robert Nieuwenhuis, Albert Oliveras, Enric Rodr\'ıguez-Carbonell, and Peter J. Stuckey: To Encode or to Propagate? The Best Choice for Each Constraint in SAT. In 19th International Conference on Principles and Practice of Constraint Programming, CP'13, 2013.
BibTeX entry

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporalizing Ontology-Based Data Access. In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), Lecture Notes in Artificial Intelligence. Lake Placid, NY, USA, Springer-Verlag, 2013.
BibTeX entry Abstract Paper (PDF) Extended technical report (PDF) (The final publication is available at link.springer.com)

Daniel Borchmann: Axiomatizing EL_gfp-General Concept Inclusions in the Presence of Untrusted Individuals. In Thomas Eiter, Birte Glimm, Yevgeny Kazakov, and Markus Krötzsch, editors, Proceedings of the 26th International Workshop on Description Logics (DL-2013), volume 1014 of CEUR Workshop Proceedings. Ulm, Germany, CEUR-WS.org, July 2013.
BibTeX entry Abstract

Daniel Borchmann: Axiomatizing EL-Expressible Terminological Knowledge from Erroneous Data. In Proceedings of the seventh international conference on Knowledge capture, K-CAP '13, pages 1–8. New York, NY, USA, ACM, 2013.
BibTeX entry Abstract DOI

Daniel Borchmann: Towards an Error-Tolerant Construction of EL -Ontologies from Data Using Formal Concept Analysis. In Peggy Cellier, Felix Distel, and Bernhard Ganter, editors, Formal Concept Analysis, 11th International Conference, ICFCA 2013, Dresden, Germany, May 21-24, 2013. Proceedings, volume 7880 of Lecture Notes in Computer Science, pages 60–75. Springer, 2013.
BibTeX entry Abstract Paper (PDF)

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporal Query Answering in the Description Logic DL-Lite. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), volume 8152 of Lecture Notes in Computer Science, pages 165–180. Nancy, France, Springer-Verlag, 2013.
BibTeX entry Abstract Paper (PDF) Extended technical report (PDF) (The final publication is available at link.springer.com)

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporal Query Answering in DL-Lite. In Thomas Eiter, Birte Glimm, Yevgeny Kazakov, and Markus Krötzsch, editors, Proceedings of the 26th International Workshop on Description Logics (DL-2013), volume 1014 of CEUR Workshop Proceedings. Ulm, Germany, CEUR-WS.org, July 2013.
BibTeX entry Paper (PDF) Extended technical report (PDF)

Stefan Borgwardt and Rafael Peñaloza: About Subsumption in Fuzzy EL. In Thomas Eiter, Birte Glimm, Yevgeny Kazakov, and Markus Krötzsch, editors, Proceedings of the 2013 International Workshop on Description Logics (DL'13), volume 1014 of CEUR Workshop Proceedings, pages 526–538, 2013.
BibTeX entry Abstract Paper (PDF)

Stefan Borgwardt and Rafael Peñaloza: Positive Subsumption in Fuzzy EL with General t-norms. In Francesca Rossi, editor, Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI'13), pages 789–795. Beijing, China, AAAI Press, 2013.
BibTeX entry Abstract Paper (PDF) ©IJCAI

Claudia Carapelle, Alexander Kartzow, and Markus Lohrey: Satisfiability of CTL* with Constraints. In Pedro R. D'Argenio and Hernán Melgratti, editors, CONCUR 2013 - Concurrency Theory, volume 8052 of Lecture Notes in Computer Science, pages 455–469. Springer Berlin Heidelberg, 2013.
BibTeX entry Paper (PDF) DOI (The final publication is available at link.springer.com)

Manfred Droste and Doreen Götze: The Support of Nested Weighted Automata. In Suna Bensch, Frank Drewes, Rudolf Freund, and Friedrich Otto, editors, Non-Classical Models of Automata and Applications (NCMA), This email address is being protected from spambots. You need JavaScript enabled to view it., pages 101–116. Ume, Sweden, Österreichische Computer Gesellschaft, 2013.
BibTeX entry

Manfred Droste and Vitaly Perevoshchikov: Multi-weighted Automata and MSO Logic. In Andrei A. Bulatov and Arseny M. Shur, editors, Proceedings of the 8th International Computer Science Symposium in Russia, volume 7913 of Lecture Notes in Artificial Intelligence, pages 418–430. Springer, 2013.
BibTeX entry (The final publication is available at link.springer.com)

Manfred Droste and Heiko Vogler: The Chomsky-Schützenberger Theorem for Quantitative Context-Free Languages. In Proceedings of the 17th International Conference on Developments in Language Theory (DLT 2013), 2013.
BibTeX entry Abstract

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Computing Role-depth Bounded Generalizations in the Description Logic ELOR. In Proceedings of the 36th German Conference on Artificial Intelligence (KI 2013), volume 8077 of Lecture Notes in Artificial Intelligence. Koblenz, Germany, Springer-Verlag, 2013.
BibTeX entry Abstract Paper (PDF) Extended technical report (PDF)

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Role-depth bounded Least Common Subsumer in Prob-EL with Nominals. In Proceedings of the 26th International Workshop on Description Logics (DL-2013), CEUR Workshop Proceedings. Ulm, Germany, CEUR-WS.org, July 2013.
BibTeX entry Abstract Paper (PDF)

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Towards Instance Query Answering for Concepts Relaxed by Similarity Measures. In Workshop on Weighted Logics for AI (in conjunction with IJCAI'13), 2013.
BibTeX entry Abstract Paper (PDF)

Uwe Ryssel, Felix Distel, and Daniel Borchmann: Fast algorithms for implication bases and attribute exploration using proper premises. Annals of Mathematics and Artificial Intelligence, Special Issue 65:1–29, 2013.
BibTeX entry Abstract Paper (PDF) (The final publication is available at link.springer.com)

2012

Thomas Weidner: Probabilistic Automata and Probabilistic Logic. In Branislav Rovan, Vladimiro Sassone, and Peter Widmayer, editors, Mathematical Foundations of Computer Science 2012, volume 7464 of Lecture Notes in Computer Science, pages 813–824. Springer Berlin Heidelberg, 2012.
BibTeX entry DOI ©Springer-Verlag

BibTeX entries

The list of publications is also available as PDF document.

2022, 2021,
2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012

2022

BibTeX entry:

@inproceedings{ ALBABODAKOME-IJCAR22,
  author = {Christian {Alrabbaa} and Franz {Baader} and Stefan {Borgwardt} and Raimund {Dachselt} and Patrick {Koopmann} and Juli\'an {M\'endez}},
  booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022},
  note = {(to appear)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {\textsc{Evonne}: Interactive Proof Visualization for Description Logics (System Description)},
  year = {2022},
}

Manfred Droste, Sven Dziadek, and Werner Kuich: Logic for omega-Pushdown Automata. Information and Computation, 282, 2022. Special issue on WATA 2018
Abstract DOI

BibTeX entry:

@article{ DrDzKu-InfCompWATA18-22,
  author = {Manfred {Droste} and Sven {Dziadek} and Werner {Kuich}},
  doi = {https://dx.doi.org/10.1016/j.ic.2020.104659},
  journal = {Information and Computation},
  note = {Special issue on WATA 2018},
  title = {Logic for omega-Pushdown Automata},
  volume = {282},
  year = {2022},
}

BibTeX entry:

@article{ DrDzKu-InfComp-22,
  author = {Manfred {Droste} and Sven {Dziadek} and Werner {Kuich}},
  doi = {https://dx.doi.org/10.1016/j.ic.2022.104871},
  journal = {Information and Computation},
  title = {{Greibach} Normal Form for omega-Algebraic Systems and Weighted Simple omega-Pushdown Automata},
  volume = {285},
  year = {2022},
}

BibTeX entry:

@article{ KMS-JCSS-2022,
  author = {Marco {Kuhlmann} and Andreas {Maletti} and Lena Katharina {Schiffer}},
  doi = {https://doi.org/10.1016/j.jcss.2021.10.005},
  journal = {Journal of Computer and System Sciences},
  pages = {214--233},
  publisher = {Elsevier},
  title = {The tree-generative capacity of combinatory categorial grammars},
  volume = {124},
  year = {2022},
}

2021

BibTeX entry:

@inproceedings{ AlBaBoKoKo-CADE2021,
  author = {Christian {Alrabbaa} and Franz {Baader} and Stefan {Borgwardt} and Patrick {Koopmann} and Alisa {Kovtunova}},
  booktitle = {Proceedings of the 28th International Conference on Automated Deduction (CADE-28), July 11--16, 2021, Virtual Event, United States},
  doi = {https://doi.org/10.1007/978-3-030-79876-5_17},
  editor = {Andr{\'e} {Platzer} and Geoff {Sutcliffe}},
  pages = {291--308},
  series = {Lecture Notes in Computer Science},
  title = {Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures},
  volume = {12699},
  year = {2021},
}

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Abstract). In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, Proceedings of the 34th International Workshop on Description Logics (DL 2021) part of Bratislava Knowledge September (BAKS 2021), Bratislava, Slovakia, September 19th to 22nd, 2021, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021.
Paper (PDF)

BibTeX entry:

@inproceedings{ AlrabbaaBBKK21,
  author = {Christian {Alrabbaa} and Franz {Baader} and Stefan {Borgwardt} and Patrick {Koopmann} and Alisa {Kovtunova}},
  booktitle = {Proceedings of the 34th International Workshop on Description Logics {(DL} 2021) part of Bratislava Knowledge September {(BAKS} 2021), Bratislava, Slovakia, September 19th to 22nd, 2021},
  editor = {Martin {Homola} and Vladislav {Ryzhikov} and Renate A. {Schmidt}},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  title = {Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Abstract)},
  volume = {2954},
  year = {2021},
}

BibTeX entry:

@inproceedings{ AlrabbaaBKKRW21,
  author = {Christian {Alrabbaa} and Stefan {Borgwardt} and Nina {Knieriemen} and Alisa {Kovtunova} and Anna Milena {Rothermel} and Frederik {Wiehr}},
  booktitle = {Proceedings of the 34th International Workshop on Description Logics {(DL} 2021) part of Bratislava Knowledge September {(BAKS} 2021), Bratislava, Slovakia, September 19th to 22nd, 2021},
  editor = {Martin {Homola} and Vladislav {Ryzhikov} and Renate A. {Schmidt}},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  title = {In the Hand of the Beholder: Comparing Interactive Proof Visualizations},
  volume = {2954},
  year = {2021},
}

Christian Alrabbaa, Stefan Borgwardt, Nina Knieriemen, Alisa Kovtunova, Anna Milena Rothermel, and Frederik Wiehr: In the Hand of the Beholder: Comparing Interactive Proof Visualizations (Extended Abstract). In Informal Proceedings of the Explainable Logic-Based Knowledge Representation (XLoKR 2021) workshop co-located with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), Online Event [Hanoi, Vietnam], November 3rd to 5th, 2021, 2021.
Paper (PDF)

BibTeX entry:

@inproceedings{ AlBoKnKoRoWi-XLoKR21,
  author = {Christian {Alrabbaa} and Stefan {Borgwardt} and Nina {Knieriemen} and Alisa {Kovtunova} and Anna Milena {Rothermel} and Frederik {Wiehr}},
  booktitle = {Informal Proceedings of the Explainable Logic-Based Knowledge Representation (XLoKR 2021) workshop co-located with the 18th International Conference on Principles of Knowledge Representation and Reasoning {(KR} 2021), Online Event [Hanoi, Vietnam], November 3rd to 5th, 2021},
  title = {In the Hand of the Beholder: Comparing Interactive Proof Visualizations (Extended Abstract)},
  year = {2021},
}

BibTeX entry:

@inproceedings{ AlHiTu-FCR-2021,
  author = {Christian {Alrabbaa} and Willi {Hieke} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 7th Workshop on Formal and Cognitive Reasoning (FCR-2021) co-located with the 44th German Conference on Artificial Intelligence (KI-2021)},
  editor = {Christoph {Beierle} and Marco {Ragni} and Frieder {Stolzenburg} and Matthias {Thimm}},
  pages = {9--22},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  title = {Counter Model Transformation For Explaining Non-Subsumption in $\mathcal{EL}$},
  volume = {2961},
  year = {2021},
}

BibTeX entry:

@inproceedings{ AlHiTu-XLoKR-2021,
  author = {Christian {Alrabbaa} and Willi {Hieke} and Anni-Yasmin {Turhan}},
  booktitle = {Informal Proceedings of the 2nd Workshop on Explainable Logic-Based Knowledge Representation (XLoKR-2021) co-located with the 18th international Conference on Principles of Knowledge Representation and Reasoning (KR-2021)},
  title = {Relevant Parts of Counter Models as Explanations for {$\mathcal{EL}$} Non-Subsumptions (Extended Abstract)},
  year = {2021},
}

BibTeX entry:

@inproceedings{ BaEtAl-CAV-21,
  author = {Christel {Baier} and Norine {Coenen} and Bernd {Finkbeiner} and Florian {Funke} and Simon {Jantsch} and Julian {Siber}},
  booktitle = {Computer Aided Verification - 33rd International Conference, {CAV} 2021},
  doi = {10.1007/978-3-030-81685-8\_42},
  pages = {894--917},
  publisher = {Springer},
  title = {Causality-Based Game Solving},
  year = {2021},
}

BibTeX entry:

@inproceedings{ BaEtAl-CONCUR-21,
  author = {Christel {Baier} and Florian {Funke} and Simon {Jantsch} and Toghrul {Karimov} and Engel {Lefaucheux} and Florian {Luca} and Jo{\"{e}}l {Ouaknine} and David {Purser} and Markus A. {Whiteland} and James {Worrell}},
  booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021},
  doi = {10.4230/LIPIcs.CONCUR.2021.28},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  series = {LIPIcs},
  title = {The Orbit Problem for Parametric Linear Dynamical Systems},
  year = {2021},
}

BibTeX entry:

@inproceedings{ BaEtAl-ATVA-21,
  author = {Christel {Baier} and Florian {Funke} and Simon {Jantsch} and Jakob {Piribauer} and Robin {Ziemek}},
  booktitle = {Automated {{Technology}} for {{Verification}} and {{Analysis}}},
  doi = {10.1007/978-3-030-88885-5\_14},
  publisher = {{Springer}},
  series = {{LNCS}},
  title = {Probabilistic {{Causes}} in {{Markov Chains}}},
  year = {2021},
}

BibTeX entry:

@inproceedings{ DBLP:conf/lics/BodirskyFKR21,
  author = {Manuel {Bodirsky} and Thomas {Feller} and Simon {Kn{\"{a}}uer} and Sebastian {Rudolph}},
  booktitle = {36th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2021, Rome, Italy, June 29 - July 2, 2021},
  doi = {10.1109/LICS52264.2021.9470511},
  pages = {1--13},
  publisher = {{IEEE}},
  title = {On Logics and Homomorphism Closure},
  year = {2021},
}

Manuel Bodirsky and Johannes Greiner: Tractable Combinations of Theories via Sampling. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, editors, Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, pages 133–146. Springer International Publishing, 2021.
Abstract DOI (The final publication is available at link.springer.com)

BibTeX entry:

@inproceedings{ BG_JELIA_2021,
  author = {Manuel {Bodirsky} and Johannes {Greiner}},
  booktitle = {Logics in Artificial Intelligence - 17th European Conference, {JELIA} 2021, Virtual Event, May 17-20, 2021, Proceedings},
  doi = {10.1007/978-3-030-75775-5_10},
  editor = {Wolfgang {Faber} and Gerhard {Friedrich} and Martin {Gebser} and Michael {Morak}},
  pages = {133--146},
  publisher = {Springer International Publishing},
  title = {Tractable Combinations of Theories via Sampling},
  year = {2021},
}

BibTeX entry:

@inproceedings{ DBLP:conf/aaai/BodirskyK21,
  author = {Manuel {Bodirsky} and Simon {Kn{\"{a}}uer}},
  booktitle = {Thirty-Fifth {AAAI} Conference on Artificial Intelligence, {AAAI} 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, {IAAI} 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, {EAAI} 2021, Virtual Event, February 2-9, 2021},
  pages = {6218--6226},
  publisher = {{AAAI} Press},
  title = {Network Satisfaction for Symmetric Relation Algebras with a Flexible Atom},
  year = {2021},
}

BibTeX entry:

@inproceedings{ DBLP:conf/icalp/BodirskyKR21,
  author = {Manuel {Bodirsky} and Simon {Kn{\"{a}}uer} and Sebastian {Rudolph}},
  booktitle = {48th International Colloquium on Automata, Languages, and Programming, {ICALP} 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference)},
  doi = {10.4230/LIPIcs.ICALP.2021.120},
  editor = {Nikhil {Bansal} and Emanuela {Merelli} and James {Worrell}},
  pages = {120:1--120:17},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  series = {LIPIcs},
  title = {Datalog-Expressibility for Monadic and Guarded Second-Order Logic},
  volume = {198},
  year = {2021},
}

Frederic Dörband: Kleene and Büchi Theorems for Weighted Forest Languages over M-Monoids. Special issue of Information and Computation devoted to WATA 2020, 2021. In print
Abstract DOI

BibTeX entry:

@article{ dor20,
  author = {Frederic {D\"{o}rband}},
  doi = {https://doi.org/10.1016/j.ic.2021.104765},
  journal = {Special issue of Information and Computation devoted to WATA 2020},
  month = {March},
  note = {In print},
  title = {Kleene and B\"{u}chi Theorems for Weighted Forest Languages over M-Monoids},
  year = {2021},
}

BibTeX entry:

@incollection{ D_rband_2021b,
  author = {Frederic {D\"{o}rband} and Thomas {Feller} and Kevin {Stier}},
  booktitle = {Language and Automata Theory and Applications},
  doi = {10.1007/978-3-030-68195-1_20},
  pages = {255--266},
  publisher = {Springer International Publishing},
  title = {Approximated Determinisation of Weighted Tree Automata},
  year = {2021},
}

BibTeX entry:

@incollection{ D_rband_2021,
  author = {Frederic {D\"{o}rband} and Thomas {Feller} and Kevin {Stier}},
  booktitle = {Language and Automata Theory and Applications},
  doi = {10.1007/978-3-030-68195-1_21},
  pages = {267--278},
  publisher = {Springer International Publishing},
  title = {Sequentiality of Group-Weighted Tree Automata},
  year = {2021},
}

BibTeX entry:

@inproceedings{ HiKrNu-DL-2021,
  author = {Willi {Hieke} and Francesco {Kriegel} and Adrian {Nuradiansyah}},
  booktitle = {Proceedings of the 34th International Workshop on Description Logics ({DL} 2021), Hybrid Event, Bratislava, Slovakia, September 19--22, 2021},
  editor = {Martin {Homola} and Vladislav {Ryzhikov} and Renate A. {Schmidt}},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  title = {{Repairing $\mathcal{EL}$ TBoxes by Means of Countermodels Obtained by Model Transformation}},
  volume = {2954},
  year = {2021},
}

BibTeX entry:

@inproceedings{ JaEtAl-GANDALF-21,
  author = {Simon {Jantsch} and Jakob {Piribauer} and Christel {Baier}},
  booktitle = {Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification ({GandALF})},
  doi = {10.4204/EPTCS.346.3},
  series = {{EPTCS}},
  title = {Witnessing Subsystems for Probabilistic Systems with Low Tree Width},
  year = {2021},
}

BibTeX entry:

@inproceedings{ JoEtAl-ATVA-21,
  author = {Tobias {John} and Simon {Jantsch} and Christel {Baier} and Sascha {Kl{\"u}ppelholz}},
  booktitle = {Automated {{Technology}} for {{Verification}} and {{Analysis}}},
  doi = {10.1007/978-3-030-88885-5\_2},
  publisher = {Springer},
  series = {{LNCS}},
  title = {Determinization and Limit-Determinization of Emerson-Lei Automata},
  year = {2021},
}

BibTeX entry:

@inproceedings{ MaEtAl-LICS-21,
  author = {Corto {Mascle} and Christel {Baier} and Florian {Funke} and Simon {Jantsch} and Stefan {Kiefer}},
  booktitle = {36th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2021},
  doi = {10.1109/LICS52264.2021.9470597},
  publisher = {{IEEE}},
  title = {Responsibility and verification: Importance value in temporal logics},
  year = {2021},
}

Lena Katharina Schiffer and Andreas Maletti: Strong Equivalence of TAG and CCG. Transactions of the Association for Computational Linguistics, 9:707–720, 2021.
Abstract DOI ©MIT Press

BibTeX entry:

@article{ SM-TACL-2021,
  author = {Lena Katharina {Schiffer} and Andreas {Maletti}},
  doi = {https://doi.org/10.1162/tacl_a_00393},
  journal = {Transactions of the Association for Computational Linguistics},
  month = {08},
  pages = {707--720},
  publisher = {MIT Press},
  title = {{Strong Equivalence of TAG and CCG}},
  volume = {9},
  year = {2021},
}

2020

BibTeX entry:

@inproceedings{ AlBaBoKoKo-20,
  author = {Christian {Alrabbaa} and Franz {Baader} and Stefan {Borgwardt} and Patrick {Koopmann} and Alisa {Kovtunova}},
  booktitle = {LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  doi = {https://doi.org/10.29007/nhpp},
  editor = {Elvira {Albert} and Laura {Kovacs}},
  pages = {32--67},
  publisher = {EasyChair},
  series = {EPiC Series in Computing},
  title = {Finding Small Proofs for Description Logic Entailments: Theory and Practice},
  volume = {73},
  year = {2020},
}

BibTeX entry:

@inproceedings{ AlBaBoKoKo-DL-20,
  author = {Christian {Alrabbaa} and Franz {Baader} and Stefan {Borgwardt} and Patrick {Koopmann} and Alisa {Kovtunova}},
  booktitle = {{DL 2020:} International Workshop on Description Logics},
  publisher = {CEUR-WS.org},
  series = {CEUR-WS},
  title = {On the Complexity of Finding Good Proofs for Description Logic Entailments},
  year = {2020},
}

BibTeX entry:

@inproceedings{ AlBaDaFlKo-DL-20,
  author = {Christian {Alrabbaa} and Franz {Baader} and Raimund {Dachselt} and Tamara {Flemisch} and Patrick {Koopmann}},
  booktitle = {{DL 2020:} International Workshop on Description Logics},
  publisher = {CEUR-WS.org},
  series = {CEUR-WS},
  title = {Visualising Proofs and the Modular Structure of Ontologies to Support Ontology Repair},
  year = {2020},
}

BibTeX entry:

@inproceedings{ AlBoKoKo-XLoKR-20,
  author = {Christian {Alrabbaa} and Stefan {Borgwardt} and Patrick {Koopmann} and Alisa {Kovtunova}},
  booktitle = {Explainable Logic-Based Knowledge Representation (XLoKR 2020)},
  title = {Finding Proofs for Description Logic Entailments in Practice},
  year = {2020},
}

BibTeX entry:

@inproceedings{ BaBo-ANDREI60-20,
  author = {Franz {Baader} and Filippo {De Bortoli}},
  booktitle = {ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia},
  doi = {10.29007/ltzn},
  editor = {Laura {Kovacs} and Konstantin {Korovin} and Giles {Reger}},
  pages = {1--25},
  publisher = {EasyChair},
  series = {EPiC Series in Computing},
  title = {Description Logics That Count, and What They Can and Cannot Count},
  volume = {68},
  year = {2020},
}

BibTeX entry:

@inproceedings{ BaDeBo-DL-20,
  address = {Online},
  author = {Franz {Baader} and Filippo {De Bortoli}},
  booktitle = {Proceedings of the 33rd International Workshop on Description Logics (DL'20)},
  editor = {Stefan {Borgwardt} and Thomas {Meyer}},
  publisher = {CEUR-WS},
  series = {CEUR Workshop Proceedings},
  title = {Description Logics that Count, and What They Can and Cannot Count (Extended Abstract)},
  volume = {2663},
  year = {2020},
}

BibTeX entry:

@inproceedings{ BaRy-IJCAR-20,
  address = {Cham},
  author = {Franz {Baader} and Jakub {Rydval}},
  booktitle = {Automated Reasoning},
  editor = {Nicolas {Peltier} and Viorica {Sofronie-Stokkermans}},
  pages = {413--431},
  publisher = {Springer International Publishing},
  title = {Description Logics with Concrete Domains and General Concept Inclusions Revisited},
  year = {2020},
}

BibTeX entry:

@inproceedings{ BaRy-DL-20,
  address = {Online},
  author = {Franz {Baader} and Jakub {Rydval}},
  booktitle = {Proceedings of the 33rd International Workshop on Description Logics (DL'20)},
  editor = {Stefan {Borgwardt} and Thomas {Meyer}},
  publisher = {CEUR-WS},
  series = {CEUR Workshop Proceedings},
  title = {Description Logics with Concrete Domains and General Concept Inclusions Revisited (Extended Abstract)},
  volume = {2663},
  year = {2020},
}

BibTeX entry:

@inproceedings{ BaEtAl-FSTTCS-20,
  author = {Christel {Baier} and Florian {Funke} and Simon {Jantsch} and Toghrul {Karimov} and Engel {Lefaucheux} and Jo{\"e}l {Ouaknine} and Amaury {Pouly} and David {Purser} and Markus A. {Whiteland}},
  booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)},
  doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.36},
  pages = {36:1--36:17},
  title = {{Reachability in Dynamical Systems with Rounding}},
  year = {2020},
}

Manuel Bodirsky and Johannes Greiner: The Complexity of Combinations of Qualitative Constraint Satisfaction Problems. Logical Methods in Computer Science, Volume 16, Issue 1, 2020.
Abstract DOI

BibTeX entry:

@article{ BG_LMCS_2020,
  author = {Manuel {Bodirsky} and Johannes {Greiner}},
  doi = {10.23638/LMCS-16(1:21)2020},
  journal = {{Logical Methods in Computer Science}},
  month = {February},
  title = {{The Complexity of Combinations of Qualitative Constraint Satisfaction Problems}},
  volume = {{Volume 16, Issue 1}},
  year = {2020},
}

BibTeX entry:

@incollection{ Bodirsky2020,
  author = {Manuel {Bodirsky} and Simon {Kn\"{a}uer}},
  booktitle = {Relational and Algebraic Methods in Computer Science},
  doi = {10.1007/978-3-030-43520-2_3},
  pages = {31--46},
  publisher = {Springer International Publishing},
  title = {Hardness of Network Satisfaction for Relation Algebras with Normal Representations},
  year = {2020},
}

BibTeX entry:

@incollection{ Bodirsky2020,
  author = {Manuel {Bodirsky} and Simon {Kn\"{a}uer}},
  booktitle = {Relational and Algebraic Methods in Computer Science},
  doi = {10.1007/978-3-030-43520-2_3},
  pages = {31--46},
  publisher = {Springer International Publishing},
  title = {Hardness of Network Satisfaction for Relation Algebras with Normal Representations},
  year = {2020},
}

BibTeX entry:

@incollection{ Bodirsky2020,
  author = {Manuel {Bodirsky} and Simon {Kn\"{a}uer} and Florian {Starke}},
  booktitle = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-51466-2_13},
  pages = {149--162},
  publisher = {Springer International Publishing},
  title = {{ASNP}: A Tame Fragment of Existential Second-Order Logic},
  year = {2020},
}

BibTeX entry:

@inproceedings{ BoRy-LICS20,
  address = {New York, NY, USA},
  author = {Manuel {Bodirsky} and Wied {Pakusa} and Jakub {Rydval}},
  booktitle = {Proceedings of the Symposium on Logic in Computer Science ({LICS} 2020)},
  doi = {https://dx.doi.org/10.1145/3373718.3394750},
  pages = {237--251},
  publisher = {Association for Computing Machinery},
  title = {Temporal Constraint Satisfaction Problems in Fixed-Point Logic},
  year = {2020},
}

BibTeX entry:

@inproceedings{ DrDzKu-FSTTCS-20,
  author = {Manfred {Droste} and Sven {Dziadek} and Werner {Kuich}},
  booktitle = {Foundations of Software Technology and Theoretical Computer Science ({FSTTCS} 2020)},
  doi = {https://dx.doi.org/10.4230/LIPIcs.FSTTCS.2020.44},
  pages = {44:1--44:14},
  series = {LIPIcs},
  title = {{Nivat}-Theorem and Logic for Weighted Pushdown Automata on Infinite Words},
  volume = {182},
  year = {2020},
}

BibTeX entry:

@inproceedings{ FlLaAlDa-VOILA-20,
  author = {Tamara {Flemisch} and Ricardo {Langner} and Christian {Alrabbaa} and Raimund {Dachselt}},
  booktitle = {Proceedings of the Fifth International Workshop on Visualization and Interaction for Ontologies and Linked Data co-located with the 19th International Semantic Web Conference {(ISWC} 2020), Virtual Conference (originally planned in Athens, Greece), November 02, 2020},
  editor = {Valentina {Ivanova} and Patrick {Lambrix} and Catia {Pesquita} and Vitalis {Wiens}},
  pages = {28--40},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  title = {Towards Designing a Tool For Understanding Proofs in Ontologies through Combined Node-Link Diagrams},
  volume = {2778},
  year = {2020},
}

BibTeX entry:

@inproceedings{ tacas20,
  address = {{Cham}},
  author = {Florian {Funke} and Simon {Jantsch} and Christel {Baier}},
  booktitle = {Tools and {{Algorithms}} for the {{Construction}} and {{Analysis}} of {{Systems}} (TACAS)},
  doi = {https://doi.org/10.1007/978-3-030-45190-5_18},
  editor = {Armin {Biere} and David {Parker}},
  pages = {324--345},
  publisher = {{Springer International Publishing}},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  title = {Farkas {{Certificates}} and {{Minimal Witnesses}} for {{Probabilistic Reachability Constraints}}},
  year = {2020},
}

BibTeX entry:

@inproceedings{ HiTu-FCR20,
  author = {Willi {Hieke} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 6th Workshop on Formal and Cognitive Reasoning (FCR-2020) co-located with 43rd German Conference on Artificial Intelligence (KI-2020)},
  editor = {Christoph {Beierle} and Marco {Ragni} and Frieder {Stolzenburg} and Matthias {Thimm}},
  pages = {69--82},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  title = {Towards Model Transformation in Description Logics --- Investigating the Case of Transductions},
  volume = {2680},
  year = {2020},
}

Simon Jantsch, Florian Funke, and Christel Baier: Minimal Witnesses for Probabilistic Timed Automata. In Automated Technology for Verification and Analysis (ATVA), 2020.
Abstract DOI

BibTeX entry:

@inproceedings{ JaFuBa-ATVA-20,
  author = {Simon {Jantsch} and Florian {Funke} and Christel {Baier}},
  booktitle = {Automated Technology for Verification and Analysis (ATVA)},
  doi = {https://doi.org/10.1007/978-3-030-59152-6_28},
  title = {Minimal Witnesses for Probabilistic Timed Automata},
  year = {2020},
}

BibTeX entry:

@inproceedings{ JaHaFuBa-FMCAD-20,
  author = {Simon {Jantsch} and Hans {Harder} and Florian {Funke} and Christel {Baier}},
  booktitle = {20th Conference on Formal Methods in Computer-Aided Design - FMCAD 2020},
  doi = {http://dx.doi.org/10.34727/2020/isbn.978-3-85448-042-6_31},
  pages = {236--244},
  publisher = {{TU Wien Academic Press}},
  title = {{{SWITSS}}: {{Computing Small Witnessing Subsystems}}},
  volume = {1},
  year = {2020},
}

BibTeX entry:

@inproceedings{ DBLP:conf/icalp/Paul20,
  author = {Erik {Paul}},
  booktitle = {47th International Colloquium on Automata, Languages, and Programming ({ICALP})},
  note = {Track B Best Student Paper Award},
  pages = {137:1--137:15},
  title = {Finite Sequentiality of Finitely Ambiguous Max-Plus Tree Automata},
  year = {2020},
}

BibTeX entry:

@inproceedings{ piribauer_et_al:LIPIcs:2020:12545,
  address = {Dagstuhl, Germany},
  author = {Jakob {Piribauer} and Christel {Baier}},
  booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  doi = {10.4230/LIPIcs.ICALP.2020.138},
  editor = {Artur {Czumaj} and Anuj {Dawar} and Emanuela {Merelli}},
  pages = {138:1--138:17},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{On {S}kolem-Hardness and Saturation Points in {M}arkov Decision Processes}},
  volume = {168},
  year = {2020},
}

2019

Christian Alrabbaa, Patrick Koopmann, and Anni-Yasmin Turhan: Practical Query Rewriting for DL-Lite with Numerical Predicates. In Diego Calvanese and Luca Iocchi, editors, GCAI 2019. Proceedings of the 5th Global Conference on Artificial Intelligence, volume 65 of EPiC Series in Computing, pages 15–27. EasyChair, 2019.
Abstract Paper (PDF) Extended technical report (PDF) DOI

BibTeX entry:

@inproceedings{ AlKoTu-GCAI-19,
  author = {Christian {Alrabbaa} and Patrick {Koopmann} and Anni-Yasmin {Turhan}},
  booktitle = {GCAI 2019. Proceedings of the 5th Global Conference on Artificial Intelligence},
  doi = {10.29007/gqll},
  editor = {Diego {Calvanese} and Luca {Iocchi}},
  pages = {15--27},
  publisher = {EasyChair},
  series = {EPiC Series in Computing},
  title = {Practical Query Rewriting for DL-Lite with Numerical Predicates},
  volume = {65},
  year = {2019},
}

BibTeX entry:

@inproceedings{ AMK-NAACL-2019,
  author = {Shima {Asaadi} and Saif {M. Mohammad} and Svetlana {Kiritchenko}},
  booktitle = {In Proceedings of the North American Chapter of the Association for Computational Linguistics (NAACL-2019)},
  title = {Big BiRD: A Large, Fine-Grained, Bigram Relatedness Dataset for Examining Semantic Composition},
  year = {2019},
}

Franz Baader and Filippo De Bortoli: On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets. In Andreas Herzig and Andrei Popescu, editors, Proc. of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019), volume 11715 of Lecture Notes in Computer Science, pages 203–219. Springer, 2019.
Abstract Paper (PDF) DOI (The final publication is available at link.springer.com) ©Springer Nature Switzerland AG 2019

BibTeX entry:

@inproceedings{ BaDeBo-FroCoS19,
  author = {Franz {Baader} and Filippo {De Bortoli}},
  booktitle = {Proc. of the 12th International Symposium on Frontiers of Combining Systems ({FroCoS} 2019)},
  doi = {https://doi.org/10.1007/978-3-030-29007-8_12},
  editor = {Andreas {Herzig} and Andrei {Popescu}},
  pages = {203--219},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets},
  volume = {11715},
  year = {2019},
}

BibTeX entry:

@inproceedings{ BaFeMa-DL19,
  author = {Franz {Baader} and Oliver {Fern\'andez Gil} and Pavlos {Marantidis}},
  booktitle = {Proceedings of the 32nd International Workshop on Description Logics (DL'19)},
  editor = {Mantas {Simkus} and Grant {Weddell}},
  publisher = {CEUR-WS},
  series = {CEUR Workshop Proceedings},
  title = {Matching in the Description Logic {FL0} with respect to General TBoxes (Extended abstract)},
  volume = {2373},
  year = {2019},
}

BibTeX entry:

@inproceedings{ BBPS19,
  author = {Christel {Baier} and Nathalie {Bertrand} and Jakob {Piribauer} and Ocan {Sankur}},
  booktitle = {Proceedings of the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'19)},
  doi = {10.1109/LICS.2019.8785672},
  pages = {1--14},
  publisher = {IEEE},
  title = {Long-run Satisfaction of Path Properties},
  year = {2019},
}

BibTeX entry:

@article{ dor20,
  author = {Frederic {D\"{o}rband} and Zolt\'{a}n {F\"{u}l\"{o}p} and Heiko {Vogler}},
  journal = {Special issue of Information and Computation devoted to CAI 2019},
  month = {October},
  note = {Accepted},
  title = {Kleene and B\"{u}chi Theorems for Weighted Forest Languages over M-Monoids},
  year = {2019},
}

BibTeX entry:

@inproceedings{ fsttcs2019,
  author = {Manfred {Droste} and Sven {Dziadek} and Werner {Kuich}},
  booktitle = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2019.38},
  pages = {38:1--38:14},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  title = {Greibach Normal Form for omega-Algebraic Systems and Weighted Simple omega-Pushdown Automata},
  volume = {150},
  year = {2019},
}

Manfred Droste, Sven Dziadek, and Werner Kuich: Weighted simple reset pushdown automata. Theoretical Computer Science, 777:252–259, 2019.
Abstract DOI

BibTeX entry:

@article{ droste_dziadek_kuich,
  author = {Manfred {Droste} and Sven {Dziadek} and Werner {Kuich}},
  doi = {https://doi.org/10.1016/j.tcs.2019.01.016},
  journal = {Theoretical Computer Science},
  pages = {252--259},
  title = {Weighted simple reset pushdown automata},
  volume = {777},
  year = {2019},
}

Simon Jantsch, David Müller, Christel Baier, and Joachim Klein: From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods The Next 30 Years, Lecture Notes in Computer Science, pages 262–279. Cham, Springer International Publishing, 2019.
Abstract Paper (PDF) Extended technical report (PDF) DOI

BibTeX entry:

@inproceedings{ JaMuBaKl-FM-19,
  address = {Cham},
  author = {Simon {Jantsch} and David {M{\"u}ller} and Christel {Baier} and Joachim {Klein}},
  booktitle = {Formal {Methods} \textendash{} {The Next} 30 {Years}},
  doi = {10.1007/978-3-030-30942-8_17},
  editor = {Maurice H. {ter Beek} and Annabelle {McIver} and Jos{\'e} N. {Oliveira}},
  pages = {262--279},
  publisher = {Springer International Publishing},
  series = {Lecture {Notes} in {Computer Science}},
  title = {From {LTL} to {Unambiguous B{\"u}chi Automata} via {Disambiguation} of {Alternating Automata}},
  year = {2019},
}

BibTeX entry:

@inproceedings{ KMS-FSTTCS-2019,
  address = {Dagstuhl, Germany},
  author = {Marco {Kuhlmann} and Andreas {Maletti} and Lena Katharina {Schiffer}},
  booktitle = {39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2019.44},
  editor = {Arkadev {Chattopadhyay} and Paul {Gastin}},
  pages = {44:1--44:14},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{The Tree-Generative Capacity of Combinatory Categorial Grammars}},
  volume = {150},
  year = {2019},
}

BibTeX entry:

@proceedings{ DBLP:conf/stacs/2019,
  editor = {Rolf {Niedermeier} and Christophe {Paul}},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"{u}}r Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {36th International Symposium on Theoretical Aspects of Computer Science ({STACS})},
  volume = {126},
  year = {2019},
}

Erik Paul: Finite Sequentiality of Unambiguous Max-Plus Tree Automata. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 55:1–55:17, 2019.

BibTeX entry:

@inproceedings{ DBLP:conf/stacs/Paul19,
  author = {Erik {Paul}},
  booktitle = {36th International Symposium on Theoretical Aspects of Computer Science ({STACS})},
  pages = {55:1--55:17},
  title = {Finite Sequentiality of Unambiguous Max-Plus Tree Automata},
  year = {2019},
}

BibTeX entry:

@inproceedings{ PirBai-FOSSACS-2019,
  author = {Jakob {Piribauer} and Christel {Baier}},
  booktitle = {Proceedings of the 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'19)},
  editor = {Mikolaj {Bojanczyk} and Alex {Simpson}},
  pages = {436--452},
  publisher = {Springer},
  series = {LNCS},
  title = {Partial and conditional expectations in {M}arkov decision processes with integer weights},
  volume = {11425},
  year = {2019},
}

BibTeX entry:

@inproceedings{ 10.1007/978-3-030-19570-0_10,
  address = {Cham},
  author = {Markus {Ulbricht}},
  booktitle = {Logics in Artificial Intelligence},
  editor = {Francesco {Calimeri} and Nicola {Leone} and Marco {Manna}},
  pages = {151--167},
  publisher = {Springer International Publishing},
  title = {Repairing Non-monotonic Knowledge Bases},
  year = {2019},
}

2018

BibTeX entry:

@inproceedings{ AlRuSc-RR18,
  author = {Christian {Alrabbaa} and Sebastian {Rudolph} and Lukas {Schweizer}},
  booktitle = {Proceedings of Rules and Reasoning - Second International Joint Conference, RuleML+RR 2018},
  editor = {Christoph Benzm{\"{u}}ller and	Francesco Ricca and	Xavier {Parent} and Dumitru {Roman}},
  pages = {211--225},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Faceted Answer-Set Navigation},
  volume = {11092},
  year = {2018},
}

BibTeX entry:

@inproceedings{ BaFeMa18-LPAR,
  author = {Franz {Baader} and Oliver {Fern\'andez Gil} and Pavlos {Marantidis}},
  booktitle = {LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  doi = {10.29007/q74p},
  editor = {Gilles {Barthe} and Geoff {Sutcliffe} and Margus {Veanes}},
  pages = {76--94},
  publisher = {EasyChair},
  series = {EPiC Series in Computing},
  title = {Matching in the Description Logic FL0 with respect to General TBoxes},
  volume = {57},
  year = {2018},
}

BibTeX entry:

@inproceedings{ BaFePe-GCAI-18,
  author = {Franz {Baader} and Oliver {Fern\'andez Gil} and Maximilian {Pensel}},
  booktitle = {{GCAI} 2018, 4th Global Conference on Artificial Intelligence, Luxembourg, September 2018.},
  doi = {10.29007/scbw},
  editor = {Daniel {Lee} and Alexander {Steen} and Toby {Walsh}},
  pages = {1--14},
  publisher = {EasyChair},
  series = {EPiC Series in Computing},
  title = {Standard and Non-Standard Inferences in the Description Logic {$\mathcal{FL}_0$} Using Tree Automata},
  volume = {55},
  year = {2018},
}

BibTeX entry:

@inproceedings{ BaMaMo-UNIF2018,
  address = {Oxford, UK},
  author = {Franz {Baader} and Pavlos {Marantidis} and Antoine {Mottet}},
  booktitle = {Proceedings of the 32th International Workshop on Unification ({UNIF 2018})},
  editor = {Mauricio {Ayala-Rinc{\'o}n} and Philippe {Balbiani}},
  title = {ACUI Unification modulo Ground Theories},
  year = {2018},
}

BibTeX entry:

@inproceedings{ BaMaPe-RoD-18,
  author = {Franz {Baader} and Pavlos {Marantidis} and Maximilian {Pensel}},
  booktitle = {Proc.\ of the Reasoning on Data Workshop (RoD'18), Companion of the The Web Conference 2018},
  doi = {https://dx.doi.org/10.1145/3184558.3191618},
  pages = {1603--1607},
  publisher = {ACM},
  title = {The Data Complexity of Answering Instance Queries in $\mathcal{FL}_0$},
  year = {2018},
}

Parvaneh Babari, Manfred Droste, and Vitaly Perevoshchikov: Weighted register automata and weighted logic on data words. Theoretical Computer Science, 744:3–21, 2018.
Abstract DOI

BibTeX entry:

@article{ babari_droste_perevoshchikov,
  author = {Parvaneh {Babari} and Manfred {Droste} and Vitaly {Perevoshchikov}},
  doi = {https://doi.org/10.1016/j.tcs.2018.01.004},
  journal = {Theoretical Computer Science},
  pages = {3--21},
  title = {Weighted register automata and weighted logic on data words},
  volume = {744},
  year = {2018},
}

BibTeX entry:

@inproceedings{ Baumann2018if,
  author = {Ringo {Baumann} and Markus {Ulbricht}},
  booktitle = {Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, {KR} 2018, Tempe, Arizona, 30 October - 2 November 2018.},
  pages = {108--117},
  title = {If Nothing Is Accepted - Repairing Argumentation Frameworks},
  year = {2018},
}

Manuel Bodirsky and Johannes Greiner: Complexity of Combinations of Qualitative Constraint Satisfaction Problems. In Didier, Galmiche, Stephan, Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning (IJCAR), volume 10900 of Lecture Notes in Computer Science, pages 263–278. Springer International Publishing, 2018.
Abstract DOI (The final publication is available at link.springer.com)

BibTeX entry:

@inproceedings{ BG_IJCAR_2018,
  author = {Manuel {Bodirsky} and Johannes {Greiner}},
  booktitle = {9th International Joint Conference on Automated Reasoning ({IJCAR})},
  doi = {10.1007/978-3-319-94205-6_18},
  editor = {Didier, {Galmiche} and Stephan, {Schulz} and Roberto {Sebastiani}},
  pages = {263--278},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  title = {Complexity of Combinations of Qualitative Constraint Satisfaction Problems},
  volume = {10900},
  year = {2018},
}

Manuel Bodirsky, Peter Jonsson, Barnaby Martin, and Antoine Mottet: Classification Transfer for Qualitative Reasoning Problems. In Proceedings of IJCAI'18, 2018.

BibTeX entry:

@inproceedings{ BodJonMarMot-IJCAI,
  author = {Manuel {Bodirsky} and Peter {Jonsson} and Barnaby {Martin} and Antoine {Mottet}},
  booktitle = {Proceedings of IJCAI'18},
  title = {Classification Transfer for Qualitative Reasoning Problems},
  year = {2018},
}

Manuel Bodirsky, Florent Madelaine, and Antoine Mottet: A universal-algebraic proof of the dichotomy for Monotone Monadic SNP. In Proceedings of LICS'18, pages 105–114, 2018.
DOI

BibTeX entry:

@inproceedings{ BodMadMot-LICS,
  author = {Manuel {Bodirsky} and Florent {Madelaine} and Antoine {Mottet}},
  booktitle = {Proceedings of LICS'18},
  doi = {http://dx.doi.org/10.1145/3209108.3209156},
  pages = {105--114},
  title = {A universal-algebraic proof of the dichotomy for Monotone Monadic SNP},
  year = {2018},
}

Manuel Bodirsky, Marcello Mamino, Barnaby Martin, and Antoine Mottet: The complexity of disjunctive linear Diophantine constraints. In Proceedings of MFCS'18, 2018.

BibTeX entry:

@inproceedings{ BodMamMarMot-MFCS,
  author = {Manuel {Bodirsky} and Marcello {Mamino} and Barnaby {Martin} and Antoine {Mottet}},
  booktitle = {Proceedings of MFCS'18},
  title = {The complexity of disjunctive linear Diophantine constraints},
  year = {2018},
}

BibTeX entry:

@inproceedings{ bodirsky_et_al:LIPIcs:2018:9679,
  address = {Dagstuhl, Germany},
  author = {Manuel {Bodirsky} and Marcello {Mamino} and Caterina {Viola}},
  booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  doi = {10.4230/LIPIcs.CSL.2018.12},
  editor = {Dan {Ghica} and Achim {Jung}},
  pages = {12:1--12:22},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains}},
  volume = {119},
  year = {2018},
}

Manuel Bodirsky and Antoine Mottet: A Dichotomy for First-Order Reducts of Unary Structures. Logical Methods in Computer Science, Volume 14, Issue 2, 2018.
DOI

BibTeX entry:

@article{ BodMot-LMCS,
  author = {Manuel {Bodirsky} and Antoine {Mottet}},
  doi = {http://dx.doi.org/10.23638/LMCS-14(2:13)2018},
  journal = {{Logical Methods in Computer Science}},
  title = {{A Dichotomy for First-Order Reducts of Unary Structures}},
  volume = {{Volume 14, Issue 2}},
  year = {2018},
}

Gerhard Brewka, Matthias Thimm, and Markus Ulbricht: Strong inconsistency. Artificial Intelligence, 267:78–117, 2018.
Abstract DOI

BibTeX entry:

@article{ BREWKA201978,
  author = {Gerhard {Brewka} and Matthias {Thimm} and Markus {Ulbricht}},
  doi = {https://doi.org/10.1016/j.artint.2018.11.002},
  journal = {Artificial Intelligence},
  pages = {78--117},
  title = {Strong inconsistency},
  volume = {267},
  year = {2018},
}

Manfred Droste and Erik Paul: A Feferman-Vaught decomposition theorem for weighted MSO logic. In Proceedings of MFCS'18, 2018.

BibTeX entry:

@inproceedings{ DroPau-MFCS18,
  author = {Manfred {Droste} and Erik {Paul}},
  booktitle = {Proceedings of MFCS'18},
  title = {A {F}eferman-{V}aught decomposition theorem for weighted {MSO} logic},
  year = {2018},
}

BibTeX entry:

@article{ KBCDDKMM-STTT-18,
  author = {Joachim {Klein} and Christel {Baier} and Philipp {Chrszon} and Marcus {Daum} and Clemens {Dubslaff} and Sascha {Kl\"uppelholz} and Steffen {M\"arcker} and David {M\"uller}},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  number = {2},
  pages = {179--194},
  title = {Advances in probabilistic model checking with {PRISM}: variable reordering, quantiles and weak deterministic B\"uchi automata},
  volume = {20},
  year = {2018},
}

BibTeX entry:

@article{ PeTu-IJAR-18,
  author = {Maximilian {Pensel} and Anni-Yasmin {Turhan}},
  doi = {https://doi.org/10.1016/j.ijar.2018.08.005},
  journal = {International Journal of Approximate Reasoning ({IJAR})},
  pages = {28--70},
  title = {Reasoning in the Defeasible Description Logic $\mathcal{EL}_{\bot}$---Computing Standard Inferences under Rational and Relevant Semantics},
  volume = {103},
  year = {2018},
}

BibTeX entry:

@inproceedings{ Ulbricht:2018,
  author = {Markus {Ulbricht} and Matthias {Thimm} and Gerhard {Brewka}},
  booktitle = {Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI'18)},
  month = {February},
  pages = {1989--1996},
  publisher = {AAAI Press},
  title = {Measuring Strong Inconsistency},
  year = {2018},
}

2017

BibTeX entry:

@inproceedings{ AR-RepL4NLP-2017,
  author = {Shima {Asaadi} and Sebastian {Rudolph}},
  booktitle = {Proceedings of the 2nd Workshop on Representation Learning for NLP},
  pages = {178--185},
  title = {Gradual Learning of Matrix-Space Models of Language for Sentiment Analysis},
  year = {2017},
}

BibTeX entry:

@inproceedings{ sacBaFe17,
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}},
  booktitle = {Proceedings of the 32nd Annual {ACM} Symposium on Applied Computing, Marrakech, Morocco, April 4-6, 2017},
  pages = {983--988},
  publisher = {{ACM}},
  title = {Decidability and Complexity of Threshold Description Logics Induced by Concept Similarity Measures},
  year = {2017},
}

BibTeX entry:

@inproceedings{ BaFM-LATA17,
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil} and Pavlos {Marantidis}},
  booktitle = {Proceedings of the 11th International Conference on Language and Automata Theory and Applications ({LATA 2017})},
  doi = {10.1007/978-3-319-53733-7_1},
  editor = {Frank {Drewes} and Carlos {Mart{\'i}n{-}Vide} and Bianca {Truthe}},
  pages = {3--26},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in $\mathcal{FL}_0$},
  venue = {Ume{\aa}, Sweden},
  volume = {10168},
  year = {2017},
}

BibTeX entry:

@inproceedings{ BaMa-UNIF2017,
  address = {Oxford, UK},
  author = {Franz {Baader} and Pavlos {Marantidis}},
  booktitle = {Proceedings of the 31st International Workshop on Unification ({UNIF'17})},
  editor = {Adri\`{a} {Gasc\'{o}n} and Christopher {Lynch}},
  title = {Language equations for approximate matching in the Description Logic FL0},
  year = {2017},
}

Manuel Bodirsky, Barnaby Martin, and Antoine Mottet: Discrete Temporal Constraint Satisfaction Problems. Journal of the ACM, 2017. Accepted for publication in the Journal of the ACM.

BibTeX entry:

@article{ BodMarMot-DiscreteTemporal,
  author = {Manuel {Bodirsky} and Barnaby {Martin} and Antoine {Mottet}},
  journal = {Journal of the ACM},
  note = {Accepted for publication in the Journal of the ACM.},
  title = {Discrete {T}emporal {C}onstraint {S}atisfaction {P}roblems},
  year = {2017},
}

BibTeX entry:

@inproceedings{ brewka2017strong,
  author = {Gerhard {Brewka} and Matthias {Thimm} and Markus {Ulbricht}},
  booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, {IJCAI-17}},
  doi = {10.24963/ijcai.2017/125},
  pages = {901--907},
  title = {Strong Inconsistency in Nonmonotonic Reasoning},
  year = {2017},
}

Manfred Droste and Stefan Dück: Weighted Automata and Logics for Infinite Nested Words. Inf. Comp., 253, Part 3:448–466, 2017.
DOI

BibTeX entry:

@article{ DrDue-InfComp-2016,
  author = {Manfred {Droste} and Stefan {D{\"u}ck}},
  doi = {http://dx.doi.org/10.1016/j.ic.2016.06.010},
  journal = {Inf. Comp.},
  pages = {448--466},
  title = {Weighted Automata and Logics for Infinite Nested Words},
  volume = {253, Part 3},
  year = {2017},
}

Manfred Droste, Stefan Dück, Dino Mandrioli, and Matteo Pradella: Weighted Operator Precedence Languages. In Proceedings of MFCS'17, pages 31:1–31:15, 2017.

BibTeX entry:

@inproceedings{ DDMP-MFCS-2017,
  author = {Manfred {Droste} and Stefan {D{\"{u}}ck} and Dino {Mandrioli} and Matteo {Pradella}},
  booktitle = {Proceedings of MFCS'17},
  pages = {31:1--31:15},
  title = {Weighted Operator Precedence Languages},
  year = {2017},
}

Andreas Ecke: Quantitative Methods for Similarity in Description Logics. Künstliche Intelligenz, 2017. To appear

BibTeX entry:

@article{ Ecke-KIJ-17,
  author = {Andreas {Ecke}},
  journal = {K\"unstliche Intelligenz},
  note = {To appear},
  title = {Quantitative Methods for Similarity in Description Logics},
  year = {2017},
}

BibTeX entry:

@inproceedings{ her17,
  address = {Cham},
  author = {Luisa {Herrmann}},
  booktitle = {Proc. 21th Int. Conf. on Developments in Language Theorie (DLT 2017)},
  doi = {10.1007/978-3-319-62809-7_15},
  editor = {{\'E}milie {Charlier} and Julien {Leroy} and Michel {Rigo}},
  pages = {210--221},
  publisher = {Springer International Publishing},
  title = {A Medvedev Characterization of Recognizable Tree Series},
  year = {2017},
}

BibTeX entry:

@inproceedings{ MS-GandALF-17,
  author = {David {M\"uller} and Salomon {Sickert}},
  booktitle = {8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF)},
  pages = {180--194},
  publisher = {Open Publishing Association},
  series = {Electronic Proceedings of Theoretical Computer Science},
  title = {{LTL} to Deterministic {Emerson-Lei} Automata},
  volume = {256},
  year = {2017},
}

Erik Paul: Monitor logics for quantitative monitor automata. In Proceedings of MFCS'17, 2017.

BibTeX entry:

@inproceedings{ Pau-MFCS172,
  author = {Erik {Paul}},
  booktitle = {Proceedings of MFCS'17},
  title = {Monitor logics for quantitative monitor automata},
  year = {2017},
}

Erik Paul: The equivalence, unambiguity and sequentiality problems of finitely ambiguous max-plus tree automata are decidable. In Proceedings of MFCS'17, 2017.

BibTeX entry:

@inproceedings{ Pau-MFCS171,
  author = {Erik {Paul}},
  booktitle = {Proceedings of MFCS'17},
  title = {The equivalence, unambiguity and sequentiality problems of finitely ambiguous max-plus tree automata are decidable},
  year = {2017},
}

BibTeX entry:

@inproceedings{ PeTu-LPNMR-17,
  author = {Maximilian {Pensel} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning - {LPNMR}},
  doi = {10.1007/978-3-319-61660-5_9},
  editor = {Marcello {Balduccini} and Tomi {Janhunen}},
  pages = {78--84},
  publisher = {Springer},
  title = {Including Quantification in Defeasible Reasoning for the Description Logic $\mathcal{EL}_{bot}$},
  year = {2017},
}

BibTeX entry:

@inproceedings{ PeTu-DARE-17,
  author = {Maximilian {Pensel} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 4th International Workshop on Defeasible and Ampliative Reasoning - {DARe}},
  editor = {Richard {Booth} and Giovanni {Casini} and Ivan {Varzinczak}},
  publisher = {CEUR-WS.org},
  title = {Making Quantification Relevant again---the case of Defeasible $\mathcal{EL}_{bot}$},
  year = {2017},
}

2016

BibTeX entry:

@inproceedings{ AR-SIGFSM-2016,
  author = {Shima {Asaadi} and Sebastian {Rudolph}},
  booktitle = {Proceedings of the SIGFSM Workshop on Statistical NLP and Weighted Automata},
  pages = {70--74},
  title = {On the Correspondence between Compositional Matrix-Space Models of Language and Weighted Automata},
  year = {2016},
}

BibTeX entry:

@inproceedings{ BaEc-LATA16,
  author = {Franz {Baader} and Andreas {Ecke}},
  booktitle = {Proceedings of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016)},
  pages = {63--75},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Reasoning with Prototypes in the Description Logic ALC using Weighted Tree Automata},
  venue = {Prague, Czeck},
  year = {2016},
}

BibTeX entry:

@inproceedings{ DBLP:conf/ecai/BaaderG16,
  author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}},
  booktitle = {{ECAI} 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence {(PAIS} 2016)},
  pages = {1096--1104},
  publisher = {{IOS} Press},
  series = {Frontiers in Artificial Intelligence and Applications},
  title = {Extending the Description Logic tel(deg) with Acyclic TBoxes},
  volume = {285},
  year = {2016},
}

BibTeX entry:

@inproceedings{ BM16,
  author = {Franz {Baader} and Pavlos {Marantidis} and Alexander {Okhotin}},
  booktitle = {Proc.\ of the 15th Eur.\ Conf.\ on Logics in Artificial Intelligence ({JELIA 2016})},
  editor = {Loizos {Michael} and Antonis C. {Kakas}},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Approximate Unification in the Description Logic {$\mathcal{FL}_0$}},
  volume = {10021},
  year = {2016},
}

BibTeX entry:

@inproceedings{ BaSch,
  author = {P. {Babari} and N. {Schweikardt}},
  booktitle = {Proc.\ of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016)},
  pages = {76--88},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {+Omega-Picture Languages Recognizable by B{\"u}chi-Tiling Systems},
  year = {2016},
}

BibTeX entry:

@inproceedings{ BKKKMW16,
  author = {Christel {Baier} and Stefan {Kiefer} and Joachim {Klein} and Sascha {Klueppelholz} and David {M\"uller} and James {Worrell}},
  booktitle = {28th International Conference on Computer Aided Verification},
  note = {to appear},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Markov Chains and Unambiguous B{\"u}chi Automata},
  year = {2016},
}

BibTeX entry:

@inproceedings{ BKMNW16,
  author = {Christel {Baier} and Sascha {Kl\"uppelholz} and Hermann {de Meer} and Florian {Niedermeier} and Sascha {Wunderlich}},
  booktitle = {Proc.\ of the 14th Int.\ Symp.\ on Automated Technology for Verification and Analysis ({ATVA 2016})},
  editor = {Cyrille {Artho} and Axel {Legay} and Doron {Peled}},
  pages = {323--339},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Greener Bits: Formal Analysis of Demand Response},
  volume = {9938},
  year = {2016},
}

Manuel Bodirsky, Victor Dalmau, Barnaby Martin, Antoine Mottet, and Michael Pinsker: Distance Constraint Satisfaction Problems. Information and Computation, 247:87–105, 2016.
DOI

BibTeX entry:

@article{ BodDalMarMotPin-InfComp-2015,
  author = {Manuel {Bodirsky} and Victor {Dalmau} and Barnaby {Martin} and Antoine {Mottet} and Michael {Pinsker}},
  doi = {http://dx.doi.org/10.1016/j.ic.2015.11.010},
  journal = {Information and Computation},
  month = {April},
  pages = {87--105},
  publisher = {Elsevier},
  title = {Distance Constraint Satisfaction Problems},
  volume = {247},
  year = {2016},
}

BibTeX entry:

@inproceedings{ BodMot-LICS-2016,
  author = {Manuel {Bodirsky} and Antoine {Mottet}},
  booktitle = {Proceedings of the Thirty-First Annual Symposium on Logic in Computer Science (LICS)},
  doi = {http://dx.doi.org/10.1145/2933575.2934515},
  pages = {623--632},
  title = {Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction},
  year = {2016},
}

BibTeX entry:

@article{ CFKL2016stip,
  author = {Claudia {Carapelle} and Shiguang {Feng} and Alexander {Kartzow} and Markus {Lohrey}},
  journal = {Theory of Computing Systems},
  note = {Zur VerÃ¶ffentlichung angenommen.},
  title = {Satisfiability of {ECTL$^*$} with local tree constraints},
  year = {2016},
}

BibTeX entry:

@inproceedings{ CaTu-ECAI-16,
  address = {Dresden, Germany},
  author = {Claudia {Carapelle} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 22nd European Conference on Artificial Intelligence},
  doi = {10.3233/978-1-61499-672-9-1440},
  editor = {Gal A. {Kaminka} and Maria {Fox} and Paolo {Bouquet} and Eyke {H{\"{u}}llermeier} and Virginia {Dignum} and Frank {Dignum} and Frank van {Harmelen}},
  pages = {1440--1448},
  publisher = {{IOS} Press},
  title = {Description Logics Reasoning w.r.t. general TBoxes is decidable for Concrete Domains with the EHD-property},
  year = {2016},
}

M. Droste and V. Perevoshchikov: Multi-weighted automata and MSO logic. Theory of Computing Systems, 2016. DOI: 10.1007/s00224-015-9658-9. Accepted for publication.

BibTeX entry:

@article{ DrostePerev-TOCS-16,
  author = {M. {Droste} and V. {Perevoshchikov}},
  journal = {Theory of Computing Systems},
  note = {DOI: 10.1007/s00224-015-9658-9. Accepted for publication.},
  title = {Multi-weighted automata and MSO logic},
  year = {2016},
}

BibTeX entry:

@inproceedings{ DFG-LATA-2016,
  author = {Manfred {Droste} and Zolt\'an {F\"ul\"op} and Doreen {G\"otze}},
  booktitle = {Proc.\ of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016)},
  pages = {452--463},
  series = {Lecture Notes in Computer Science},
  title = {A Kleene Theorem for Weighted Tree Automata over Tree Valuation Monoids},
  year = {2016},
}

BibTeX entry:

@inproceedings{ Due16,
  author = {Stefan {D{\"{u}}ck}},
  booktitle = {Proceedings of the 20th International Conference on Developments in Language Theory (DLT 2016)},
  pages = {151--163},
  publisher = {Springer},
  series = {LNCS},
  title = {Weighted Automata and Logics on Infinite Graphs},
  volume = {9840},
  year = {2016},
}

BibTeX entry:

@inproceedings{ icalpGburek16,
  author = {Daniel {Gburek} and Christel {Baier} and Sascha {Kl\"uppelholz}},
  booktitle = {Proc.\ of the 43rd Int.\ Coll.\ on Automata, Languages and Programming ({ICALP 2016})},
  editor = {Ioannis {Chatzigiannakis} and Michael {Mitzenmacher} and Yuval {Rabani} and Davide {Sangiorgi}},
  pages = {102:1--102:15},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f\"ur Informatik},
  series = {Leibniz International Proceedings in Informatics},
  title = {Composition of Stochastic Transition Systems Based on Spans and Couplings},
  volume = {55},
  year = {2016},
}

BibTeX entry:

@inproceedings{ Herrmann2016,
  author = {Luisa {Herrmann} and Heiko {Vogler}},
  booktitle = {Proc.\ of the 20th Int.\ Conf.\ on Developments in Language Theory ({DLT 2016})},
  editor = {Sre{\v{c}}ko {Brlek} and Christophe {Reutenauer}},
  pages = {203--215},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Weighted Symbolic Automata with Data Storage},
  volume = {9840},
  year = {2016},
}

BibTeX entry:

@inproceedings{ KBCDDKMM16,
  author = {Joachim {Klein} and Christel {Baier} and Philipp {Chrszon} and Marcus {Daum} and Clemens {Dubslaff} and Sascha {Kl{\"u}ppelholz} and Steffen {M{\"a}rcker} and David {M{\"u}ller}},
  booktitle = {Proc. of the 22th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  pages = {349--366},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Advances in Symbolic Probabilistic Model Checking with {PRISM}},
  volume = {9636},
  year = {2016},
}

BibTeX entry:

@article{ nedteivog16,
  author = {Mark-Jan {Nederhof} and Markus {Teichmann} and Heiko {Vogler}},
  journal = {Journal of Automata, Languages and Combinatorics},
  note = {To appear},
  title = {Non-Self-Embedding Linear Context-Free Tree Grammars Generate Regular Tree Languages},
  year = {2016},
}

BibTeX entry:

@inproceedings{ ODH-LATA-2016,
  author = {Johannes {Osterholzer} and Toni {Dietze} and Luisa {Herrmann}},
  booktitle = {Proc.\ of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016)},
  pages = {478--489},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Linear Context-Free Tree Languages and Inverse Homomorphisms},
  year = {2016},
}

BibTeX entry:

@inproceedings{ Pau16,
  author = {Erik {Paul}},
  booktitle = {Proceedings of the 20th International Conference on Developments in Language Theory ({DLT} 2016)},
  doi = {10.1007/978-3-662-53132-7_30},
  pages = {368--379},
  publisher = {Springer},
  series = {LNCS},
  title = {On Finite and Polynomial Ambiguity of Weighted Tree Automata},
  volume = {9840},
  year = {2016},
}

BibTeX entry:

@inproceedings{ tei16,
  author = {Markus {Teichmann}},
  booktitle = {Proceedings of the 21st International Conference on Implementation and Application of Automata (CIAA)},
  doi = {10.1007/978-3-319-40946-7_23},
  pages = {1--12},
  series = {Lecture Notes in Computer Science},
  title = {Regular Approximation of Weighted Linear Nondeleting Context-Free Tree Languages},
  volume = {9705},
  year = {2016},
}

BibTeX entry:

@inproceedings{ Ulbricht2016,
  address = {Cham},
  author = {Markus {Ulbricht} and Matthias {Thimm} and Gerhard {Brewka}},
  booktitle = {Logics in Artificial Intelligence: 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings},
  doi = {http://dx.doi.org/10.1007/978-3-319-48758-8_42},
  editor = {Loizos {Michael} and Antonis {Kakas}},
  pages = {577--583},
  publisher = {Springer International Publishing},
  title = {Measuring Inconsistency in Answer Set Programs},
  year = {2016},
}

BibTeX entry:

@inproceedings{ VDH-LATA-2016,
  author = {Heiko {Vogler} and Manfred {Droste} and Luisa {Herrmann}},
  booktitle = {Proc.\ of the 10th International Conference on Language and Automata Theory and Applications (LATA 2016)},
  pages = {127--139},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {A Weighted MSO Logic with Storage Behaviour and its B\"uchi-Elgot-Trakhtenbrot Theorem},
  year = {2016},
}

2015

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporal Query Entailment in the Description Logic SHQ. Journal of Web Semantics, 33:71–93, 2015.
Abstract DOI

BibTeX entry:

@article{ BaBL-JWS15,
  author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}},
  doi = {http://dx.doi.org/10.1016/j.websem.2014.11.008},
  journal = {Journal of Web Semantics},
  pages = {71--93},
  title = {Temporal Query Entailment in the Description Logic {$\mathcal{SHQ}$}},
  volume = {33},
  year = {2015},
}

Franz Baader, Gerhard Brewka, and Oliver Fernández Gil: Adding Threshold Concepts to the Description Logic EL. In Carsten Lutz and Silvio Ranise, editors, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), volume 9322 of Lectures Notes in Artificial Intelligence, pages 33–48. Wroclaw, Poland, Springer-Verlag, 2015.
Abstract Paper (PDF) Extended technical report (PDF)

BibTeX entry:

@inproceedings{ BBG-FROCOS-15,
  address = {Wroclaw, Poland},
  author = {Franz {Baader} and Gerhard {Brewka} and Oliver {Fern\'andez Gil}},
  booktitle = {Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15)},
  editor = {Carsten {Lutz} and Silvio {Ranise}},
  pages = {33--48},
  publisher = {Springer-Verlag},
  series = {Lectures Notes in Artificial Intelligence},
  title = {Adding Threshold Concepts to the Description Logic {$\mathcal{EL}$}},
  volume = {9322},
  year = {2015},
}

BibTeX entry:

@inproceedings{ BD15,
  author = {P. {Babari} and M. {Droste}},
  booktitle = {Language and Automata Theory and Applications (LATA 2015)},
  pages = {703--715},
  publisher = {Springer},
  series = {LNCS},
  title = {A Nivat theorem for weighted picture automata and weighted MSO logics},
  volume = {8977},
  year = {2015},
}

BibTeX entry:

@inproceedings{ BBDKKMPS-CAV15,
  author = {Tomas {Babiak} and Frantisek {Blahoudek} and Alexandre {Duret-Lutz} and Joachim {Klein} and Jan {Kretinsky} and David {M\"uller} and David {Parker} and Jan {Strejcek}},
  booktitle = {27th International Conference on Computer Aided Verification (CAV)},
  pages = {479--486},
  series = {Lecture Notes in Computer Science},
  title = {The {Hanoi} Omega-Automata Format},
  volume = {9206},
  year = {2015},
}

Manuel Bodirsky, Barnaby Martin, and Antoine Mottet: Constraint Satisfaction Problems over the Integers with Successor. In Magnús M. Halldórsson, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming (ICALP 2015), volume 9134 of LNCS, pages 256–267. Springer-Verlag Berlin Heidelberg, 2015.
(The final publication is available at link.springer.com)

BibTeX entry:

@inproceedings{ BodMarMot-ICALP-2015,
  author = {Manuel {Bodirsky} and Barnaby {Martin} and Antoine {Mottet}},
  booktitle = {Automata, Languages, and Programming (ICALP 2015)},
  editor = {Magn\'us M. {Halld\'orsson} and Naoki {Kobayashi} and Bettina {Speckmann}},
  pages = {256--267},
  publisher = {Springer-Verlag Berlin Heidelberg},
  series = {LNCS},
  title = {Constraint {S}atisfaction {P}roblems over the {I}ntegers with {S}uccessor},
  volume = {9134},
  year = {2015},
}

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporalizing Rewritable Query Languages over Knowledge Bases. Journal of Web Semantics, 33:50–70, 2015.
Abstract DOI

BibTeX entry:

@article{ BoLT-JWS15,
  author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}},
  doi = {10.1016/j.websem.2014.11.007},
  journal = {Journal of Web Semantics},
  pages = {50--70},
  title = {Temporalizing Rewritable Query Languages over Knowledge Bases},
  volume = {33},
  year = {2015},
}

BibTeX entry:

@inproceedings{ CFKL15,
  author = {C. {Carapelle} and S. {Feng} and A. {Kartzow} and M. {Lohrey}},
  booktitle = {10th International Computer Science Symposium in Russia (CSR 2015)},
  pages = {94--108},
  publisher = {Springer},
  series = {LNCS},
  title = {Satisfiability of ECTL* with tree constraints},
  volume = {9139},
  year = {2015},
}

BibTeX entry:

@inproceedings{ carapelle_et_al:LIPIcs:2015:5446,
  address = {Dagstuhl, Germany},
  author = {Claudia {Carapelle} and Markus {Lohrey}},
  booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2015.2},
  editor = {Stephan {Kreutzer}},
  pages = {2--13},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Temporal Logics with Local Constraints (Invited Contribution)}},
  volume = {41},
  year = {2015},
}

BibTeX entry:

@inproceedings{ DD15,
  author = {M. {Droste} and S. {D\"uck}},
  booktitle = {Proceedings of the 40th Conference on Mathematical Foundations of Computer Science (MFCS 2015), Part {I}},
  pages = {192--204},
  publisher = {Springer},
  series = {LNCS},
  title = {Weighted automata and logics on graphs},
  volume = {9234},
  year = {2015},
}

M. Droste and D. Heusel: The supports of weighted unranked tree automata. Fundamenta Informaticae, 136:37–58, 2015.

BibTeX entry:

@article{ DH15,
  author = {M. {Droste} and D. {Heusel}},
  journal = {Fundamenta Informaticae},
  pages = {37--58},
  title = {The supports of weighted unranked tree automata},
  volume = {136},
  year = {2015},
}

BibTeX entry:

@inproceedings{ DP151,
  author = {M. {Droste} and V. {Perevoshchikov}},
  booktitle = {10th International Computer Science Symposium in Russia (CSR 2015)},
  pages = {189--203},
  publisher = {Springer},
  series = {LNCS},
  title = {A logical characterization of timed pushdown languages},
  volume = {9139},
  year = {2015},
}

BibTeX entry:

@inproceedings{ DP152,
  author = {M. {Droste} and V. {Perevoshchikov}},
  booktitle = {A Symposium on Logic in Computer Science celebrating Yuri Gurevich's 75th birthday (YURIFEST 2015)},
  pages = {153--173},
  publisher = {Springer},
  series = {LNCS},
  title = {Logics for weighted timed pushdown automata},
  year = {2015},
}

BibTeX entry:

@incollection{ DHV15,
  author = {Manfred {Droste} and Doreen {Heusel} and Heiko {Vogler}},
  booktitle = {Algebraic Informatics},
  doi = {10.1007/978-3-319-23021-4_9},
  editor = {Andreas {Maletti}},
  pages = {90--102},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  title = {Weighted Unranked Tree Automata over Tree Valuation Monoids and Their Characterization by Weighted Logics},
  volume = {9270},
  year = {2015},
}

BibTeX entry:

@article{ EcPeTu-JAL15,
  author = {Andreas {Ecke} and Rafael {Pe\~naloza} and Anni-Yasmin {Turhan}},
  doi = {http://dx.doi.org/10.1016/j.jal.2015.01.002},
  journal = {Journal of Applied Logic},
  note = {Special Issue for the Workshop on Weighted Logics for {AI} 2013},
  number = {4, Part 1},
  pages = {480--508},
  title = {Similarity-based Relaxed Instance Queries},
  volume = {13},
  year = {2015},
}

BibTeX entry:

@inproceedings{ EcPeTu-DL15,
  author = {Andreas {Ecke} and Maximilian {Pensel} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 28th International Workshop on Description Logics ({DL-2015})},
  editor = {Diego {Calvanese} and Boris {Konev}},
  month = {June},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  title = {ELASTIQ: Answering Similarity-threshold Instance Queries in {$\mathcal{EL}$}},
  venue = {Athens, Greece},
  volume = {1350},
  year = {2015},
}

BibTeX entry:

@inproceedings{ FLQ15,
  author = {S. {Feng} and M. {Lohrey} and K. {Quaas}},
  booktitle = {19th International Conference on Developments in Language Theory (DLT 2015)},
  pages = {326--339},
  publisher = {Springer},
  series = {LNCS},
  title = {Path checking for MTL and TPTL over data words},
  volume = {9168},
  year = {2015},
}

Zoltán Fülöp and Heiko Vogler: Characterizations of recognizable weighted tree languages by logic and bimorphisms. Soft Computing1–12, 2015.
Abstract DOI

BibTeX entry:

@article{ fuelvog15a,
  author = {Zolt{\'a}n {F{\"u}l{\"o}p} and Heiko {Vogler}},
  doi = {10.1007/s00500-015-1717-2},
  journal = {Soft Computing},
  pages = {1--12},
  title = {Characterizations of recognizable weighted tree languages by logic and bimorphisms},
  year = {2015},
}

Zoltán Fülöp and Heiko Vogler: Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics.. Theoretical Computer Science, 594:82–105, 2015.
Abstract DOI

BibTeX entry:

@article{ fuelvog15,
  author = {Zolt\'{a}n {F\"{u}l\"{o}p} and Heiko {Vogler}},
  doi = {10.1016/j.tcs.2015.04.024},
  journal = {Theoretical Computer Science},
  pages = {82--105},
  publisher = {Elsevier},
  title = {Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics.},
  volume = {594},
  year = {2015},
}

BibTeX entry:

@inproceedings{ gebost15,
  author = {Kilian {Gebhardt} and Johannes {Osterholzer}},
  booktitle = {Proceedings of the 12th International Conference on Finite-State Methods and Natural Language Processing (FSMNLP)},
  editor = {Thomas {Hanneforth} and Christian {Wurm}},
  title = {A direct link between Tree-Adjoining and Context-Free Tree Grammars},
  year = {2015},
}

BibTeX entry:

@inproceedings{ DBLP:conf/dlog/GilBB15,
  author = {Oliver Fernandez {Gil} and Franz {Baader} and Gerhard {Brewka}},
  booktitle = {Proceedings of the 28th International Workshop on Description Logics, Athens,Greece, June 7-10, 2015.},
  title = {Adding Threshold Concepts to the Description Logic {EL}},
  year = {2015},
}

BibTeX entry:

@inproceedings{ hervog15,
  author = {Luisa {Herrmann} and Heiko {Vogler}},
  booktitle = {Proceedings of the 6th International Conference on Algebraic Informatics (CAI 2015)},
  editor = {Andreas {Maletti}},
  pages = {115--127},
  publisher = {Springer International Publishing Switzerland},
  title = {A Chomsky-Sch\"{u}tzenberger Theorem for Weighted Automata with Storage},
  year = {2015},
}

BibTeX entry:

@inproceedings{ mfcsKraehmann15,
  author = {Daniel {Kr\"ahmann} and Jana {Schubert} and Christel {Baier} and Clemens {Dubslaff}},
  booktitle = {40th International Symposium on Mathematical Foundations of Computer Science ({MFCS})},
  doi = {10.1007/978-3-662-48057-1_27},
  pages = {344--356},
  publisher = {Springer Berlin Heidelberg},
  series = {Lecture Notes in Computer Science},
  title = {Ratio and Weight Quantiles},
  year = {2015},
}

BibTeX entry:

@inproceedings{ ost15,
  author = {Johannes {Osterholzer}},
  booktitle = {Proceedings of the 6th International Conference on Algebraic Informatics (CAI 2015)},
  editor = {Andreas {Maletti}},
  pages = {176--188},
  title = {Complexity of Uniform Membership of Context-Free Tree Grammars},
  year = {2015},
}

V. Perevoshchikov: Weight assignment logic. In 19th International Conference on Developments in Language Theory (DLT 2015), volume 9168 of LNCS, pages 413–425. Springer, 2015.

BibTeX entry:

@inproceedings{ Pe15,
  author = {V. {Perevoshchikov}},
  booktitle = {19th International Conference on Developments in Language Theory (DLT 2015)},
  pages = {413--425},
  publisher = {Springer},
  series = {LNCS},
  title = {Weight assignment logic},
  volume = {9168},
  year = {2015},
}

Markus Teichmann and Johannes Osterholzer: A link between multioperator and tree valuation automata and logics. Theoretical Computer Science, 594:106–119, 2015.
Abstract DOI

BibTeX entry:

@article{ teiost15,
  author = {Markus {Teichmann} and Johannes {Osterholzer}},
  doi = {10.1016/j.tcs.2015.04.033},
  journal = {Theoretical Computer Science},
  pages = {106--119},
  publisher = {Elsevier},
  title = {A link between multioperator and tree valuation automata and logics},
  volume = {594},
  year = {2015},
}

BibTeX entry:

@inproceedings{ Weidner-FSTTCS-2015,
  address = {Dagstuhl, Germany},
  author = {Thomas {Weidner}},
  booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  doi = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.503},
  editor = {Prahladh {Harsha} and G. {Ramalingam}},
  pages = {503--516},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{ Probabilistic Regular Expressions and MSO Logic on Finite Trees}},
  volume = {45},
  year = {2015},
}

2014

Franz Baader and Marcel Lippmann: Runtime Verification Using the Temporal Description Logic ALC-LTL Revisited. Journal of Applied Logic, 12(4):584–613, 2014.
Abstract DOI

BibTeX entry:

@article{ BaLi-JAL14,
  author = {Franz {Baader} and Marcel {Lippmann}},
  doi = {http://dx.doi.org/10.1016/j.jal.2014.09.001},
  journal = {Journal of Applied Logic},
  number = {4},
  pages = {584--613},
  title = {Runtime Verification Using the Temporal Description Logic $\mathcal{ALC}$-LTL Revisited},
  volume = {12},
  year = {2014},
}

BibTeX entry:

@incollection{ BaDuKlKlWu-PP14,
  author = {Christel {Baier} and Clemens {Dubslaff} and Joachim {Klein} and Sascha {Kl{\"u}ppelholz} and Sascha {Wunderlich}},
  booktitle = {Horizons of the Mind. A Tribute to Prakash Panangaden},
  pages = {96--123},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Probabilistic Model Checking for Energy-Utility Analysis},
  volume = {8464},
  year = {2014},
}

BibTeX entry:

@inproceedings{ BaDuKlDaKlMaWu-FASE14,
  author = {Christel {Baier} and Clemens {Dubslaff} and Sascha {Kl{\"u}ppelholz} and Marcus {Daum} and Joachim {Klein} and Steffen {M{\"a}rcker} and Sascha {Wunderlich}},
  booktitle = {Proc. of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE)},
  pages = {1--16},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Probabilistic Model Checking and Non-standard Multi-objective Reasoning},
  volume = {8411},
  year = {2014},
}

BibTeX entry:

@inproceedings{ BDKL14,
  author = {Christel {Baier} and Clemens {Dubslaff} and Sascha {Kl{\"u}ppelholz} and Linda {Leuschner}},
  booktitle = {Proc. of the 35th Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS)},
  pages = {20--39},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking},
  volume = {8489},
  year = {2014},
}

BibTeX entry:

@inproceedings{ BaKlKlWu-CSLLICS14,
  author = {Christel {Baier} and Joachim {Klein} and Sascha {Kl{\"u}ppelholz} and Sascha {Wunderlich}},
  booktitle = {Proc. of the 23rd Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS)},
  pages = {11:1--11:10},
  publisher = {ACM},
  title = {Weight Monitoring with Linear Temporal Logic: Complexity and Decidability},
  year = {2014},
}

BibTeX entry:

@inproceedings{ BoDP-KR14,
  address = {Vienna, Austria},
  author = {Stefan {Borgwardt} and Felix {Distel} and Rafael {Pe{\~n}aloza}},
  booktitle = {Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR'14)},
  pages = {228--237},
  publisher = {AAAI Press},
  title = {Decidable {G}{\"o}del description logics without the finitely-valued model property},
  year = {2014},
}

Stefan Borgwardt and Rafael Peñaloza: Consistency Reasoning in Lattice-Based Fuzzy Description Logics. International Journal of Approximate Reasoning, 2014.
Abstract Paper (PDF) DOI

BibTeX entry:

@article{ BoPe-IJAR14,
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  doi = {http://dx.doi.org/10.1016/j.ijar.2013.07.006},
  journal = {International Journal of Approximate Reasoning},
  title = {Consistency Reasoning in Lattice-Based Fuzzy Description Logics},
  year = {2014},
}

BibTeX entry:

@incollection{ Carapelle_Feng_Fernandez_Quaas_LATA2014.bib,
  author = {Claudia {Carapelle} and Shiguang {Feng} and Oliver {Fern\'andez Gil} and Karin {Quaas}},
  booktitle = {Language and Automata Theory and Applications},
  doi = {10.1007/978-3-319-04921-2_20},
  editor = {Adrian-Horia {Dediu} and Carlos {Martin-V\'ide} and Jos\'e-Luis {Sierra-Rodr\'iguez} and Bianca {Truthe}},
  pages = {248--259},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  title = {Satisfiability for MTL and TPTL over Non-monotonic Data Words},
  volume = {8370},
  year = {2014},
}

BibTeX entry:

@inproceedings{ DBLP:journals/corr/CarapelleFGQ13,
  author = {Claudia {Carapelle} and Shiguang {Feng} and Oliver Fernandez {Gil} and Karin {Quaas}},
  booktitle = {Proceedings 14th International Conference on Automata and Formal Languages, AFL 2014, Szeged, Hungary, May 27-29, 2014},
  editor = {Zolt{\'a}n {\'E} and Zolt{\'a}n {F{\"u}l{\"o}p}},
  pages = {174--187},
  series = {EPTCS},
  title = {On the Expressiveness of TPTL and MTL over omega-Data Words},
  volume = {151},
  year = {2014},
}

BibTeX entry:

@inproceedings{ DP14,
  author = {M. {Droste} and V. {Perevoshchikov}},
  booktitle = {35th Int. Colloq. on Automata, Languages, and Programming (ICALP 2014)},
  pages = {171--182},
  publisher = {Springer},
  series = {LNCS},
  title = {A Nivat theorem for weighted timed automata and weighted relative distance logic},
  volume = {8573},
  year = {2014},
}

BibTeX entry:

@inproceedings{ DrDue-LATA-2014,
  address = {Madrid, Spain},
  author = {Manfred {Droste} and Stefan {D{\"u}ck}},
  booktitle = {8th International Conference on Language and Automata Theory and Application (LATA)},
  editor = {Adrian Horia {Dediu} and Carlos {Mart{\'i}n-Vide} and Jos{\'e} Luis {Sierra-Rodr{\'i}guez} and Bianca {Truthe}},
  pages = {323--334},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Weighted Automata and Logics for Infinite Nested Words},
  volume = {8370},
  year = {2014},
}

BibTeX entry:

@article{ drovog14a,
  author = {Manfred {Droste} and Heiko {Vogler}},
  doi = {10.1142/S0129054114400176},
  journal = {International Journal of Foundations of Computer Science},
  number = {8},
  pages = {955--969},
  title = {The Chomsky-Sch\"{u}tzenberger Theorem for Quantitative Context-Free Languages},
  volume = {25},
  year = {2014},
}

BibTeX entry:

@inproceedings{ Ecke-PRUV-14,
  author = {Andreas {Ecke}},
  booktitle = {Proceedings of the First Workshop on Logics for Reasoning about Preferences, Uncertainty, and Vagueness},
  editor = {Thomas {Lukasiewicz} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  pages = {101--113},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  title = {Similarity-based Relaxed Instance Queries in $\mathcal{EL}^{++}$},
  volume = {1205},
  year = {2014},
}

BibTeX entry:

@inproceedings{ EcPeTu-KR14,
  address = {Vienna, Austria},
  author = {Andreas {Ecke} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning ({KR'14})},
  pages = {248--257},
  publisher = {AAAI Press},
  title = {Answering Instance Queries Relaxed by Concept Similarity},
  year = {2014},
}

BibTeX entry:

@article{ EcPeTu-IJAR-14,
  author = {Andreas {Ecke} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  doi = {http://dx.doi.org/10.1016/j.ijar.2014.03.001},
  journal = {International Journal of Approximate Reasoning},
  number = {9},
  pages = {1939--1970},
  publisher = {Elsevier},
  title = {Completion-based Generalization Inferences for the Description Logic $\mathcal{ELOR}$ with Subjective Probabilities},
  volume = {55},
  year = {2014},
}

BibTeX entry:

@inproceedings{ EcPeTu-DL14,
  author = {Andreas {Ecke} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 27th International Workshop on Description Logics ({DL-2014})},
  month = {July},
  note = {Extended Abstract},
  title = {Mary, What's Like All Cats?},
  venue = {Vienna, Austria},
  year = {2014},
}

BibTeX entry:

@inproceedings{ Gil-NMR-14,
  address = {Vienna, Austria},
  author = {Oliver {Fern\'andez Gil}},
  booktitle = {Proceedings of the 15th International Workshop on Non-Monotonic Reasoning (NMR'14)},
  pages = {114--122},
  title = {On the Non-Monotonic Description Logic {ALC+Tmin}},
  year = {2014},
}

BibTeX entry:

@inproceedings{ DBLP:conf/lata/KleinMBK14,
  author = {Joachim {Klein} and David {M{\"u}ller} and Christel {Baier} and Sascha {Kl{\"u}ppelholz}},
  booktitle = {Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings},
  editor = {Adrian Horia {Dediu} and Carlos {Mart\'{\i}n-Vide} and Jos{\'e} Luis {Sierra-Rodr\'{\i}guez} and Bianca {Truthe}},
  pages = {453--465},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Are Good-for-Games Automata Good for Probabilistic Model Checking?},
  volume = {8370},
  year = {2014},
}

BibTeX entry:

@inproceedings{ ost14,
  author = {Johannes {Osterholzer}},
  booktitle = {Proceedings of 19th International Conference on Implementation and Application of Automata (CIAA 2014)},
  doi = {10.1007/978-3-319-08846-4_22},
  pages = {290--303},
  title = {Pushdown Machines for Weighted Context-Free Tree Translation},
  year = {2014},
}

BibTeX entry:

@incollection{ Weidner-LATA-2014,
  author = {Thomas {Weidner}},
  booktitle = {Language and Automata Theory and Applications},
  doi = {10.1007/978-3-319-04921-2_48},
  editor = {Adrian-Horia {Dediu} and Carlos {Mart\'in-Vide} and Jos\'e-Luis {Sierra-Rodr\'iguez} and Bianca {Truthe}},
  pages = {588--600},
  publisher = {Springer International Publishing},
  series = {Lecture Notes in Computer Science},
  title = {Probabilistic Omega-Regular Expressions},
  volume = {8370},
  year = {2014},
}

2013

BibTeX entry:

@inproceedings{ parametricCardinalityConstraint,
  author = {Ignasi {Ab{\'\i}o} and Robert {Nieuwenhuis} and Albert {Oliveras} and Enric {Rodr\'{\i}guez-Carbonell}},
  booktitle = {19th International Conference on Principles and Practice of Constraint Programming},
  series = {CP'13},
  title = {{A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints}},
  year = {2013},
}

BibTeX entry:

@inproceedings{ encodeOrPropagate,
  author = {Ignasi {Ab{\'\i}o} and Robert {Nieuwenhuis} and Albert {Oliveras} and Enric {Rodr\'{\i}guez-Carbonell} and Peter J. {Stuckey}},
  booktitle = {19th International Conference on Principles and Practice of Constraint Programming},
  series = {CP'13},
  title = {{To Encode or to Propagate? The Best Choice for Each Constraint in SAT}},
  year = {2013},
}

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporalizing Ontology-Based Data Access. In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), Lecture Notes in Artificial Intelligence. Lake Placid, NY, USA, Springer-Verlag, 2013.
Abstract Paper (PDF) Extended technical report (PDF) (The final publication is available at link.springer.com)

BibTeX entry:

@inproceedings{ BaBL-CADE13,
  address = {Lake Placid, NY, USA},
  author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}},
  booktitle = {Proceedings of the 24th International Conference on Automated Deduction (CADE-24)},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Temporalizing Ontology-Based Data Access},
  year = {2013},
}

BibTeX entry:

@inproceedings{ Borc-DL13,
  address = {Ulm, Germany},
  author = {Daniel {Borchmann}},
  booktitle = {Proceedings of the 26th International Workshop on Description Logics ({DL-2013})},
  editor = {Thomas {Eiter} and Birte {Glimm} and Yevgeny {Kazakov} and Markus {Kr{\"o}tzsch}},
  month = {July},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  title = {Axiomatizing $\mathcal{E\!L}^{\bot}_{\mathrm{gfp}}$-General Concept Inclusions in the Presence of Untrusted Individuals},
  volume = {1014},
  year = {2013},
}

BibTeX entry:

@inproceedings{ Borc-KCAP13,
  address = {New York, NY, USA},
  author = {Daniel {Borchmann}},
  booktitle = {Proceedings of the seventh international conference on Knowledge capture},
  doi = {10.1145/2479832.2479835},
  pages = {1--8},
  publisher = {ACM},
  series = {K-CAP '13},
  title = {Axiomatizing $\mathcal{E}\!\mathcal{L}^{\bot}$-Expressible Terminological Knowledge from Erroneous Data},
  year = {2013},
}

BibTeX entry:

@inproceedings{ Borc-ICFCA13,
  author = {Daniel {Borchmann}},
  booktitle = {Formal Concept Analysis, 11th International Conference, ICFCA 2013, Dresden, Germany, May 21-24, 2013. Proceedings},
  editor = {Peggy {Cellier} and Felix {Distel} and Bernhard {Ganter}},
  pages = {60--75},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Towards an Error-Tolerant Construction of $\mathcal{EL}^{\bot}$ -Ontologies from Data Using Formal Concept Analysis},
  volume = {7880},
  year = {2013},
}

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporal Query Answering in the Description Logic DL-Lite. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), volume 8152 of Lecture Notes in Computer Science, pages 165–180. Nancy, France, Springer-Verlag, 2013.
Abstract Paper (PDF) Extended technical report (PDF) (The final publication is available at link.springer.com)

BibTeX entry:

@inproceedings{ BoLiTh-FroCoS13,
  address = {Nancy, France},
  author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}},
  booktitle = {Proceedings of the 9th International Symposium on Frontiers of Combining Systems ({FroCoS 2013})},
  editor = {Pascal {Fontaine} and Christophe {Ringeissen} and Renate A. {Schmidt}},
  pages = {165--180},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Temporal Query Answering in the Description Logic {\textit{DL-Lite}}},
  volume = {8152},
  year = {2013},
}

BibTeX entry:

@inproceedings{ BoLiTh-DL13,
  address = {Ulm, Germany},
  author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}},
  booktitle = {Proceedings of the 26th International Workshop on Description Logics ({DL-2013})},
  editor = {Thomas {Eiter} and Birte {Glimm} and Yevgeny {Kazakov} and Markus {Kr{\"o}tzsch}},
  month = {July},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  title = {Temporal Query Answering in {\textit{DL-Lite}}},
  volume = {1014},
  year = {2013},
}

BibTeX entry:

@inproceedings{ BoPe-DL13,
  address = {Ulm, Germany},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  booktitle = {Proceedings of the 2013 International Workshop on Description Logics ({DL'13})},
  editor = {Thomas {Eiter} and Birte {Glimm} and Yevgeny {Kazakov} and Markus {Kr{\"o}tzsch}},
  pages = {526--538},
  series = {CEUR Workshop Proceedings},
  title = {About Subsumption in Fuzzy $\mathcal{EL}$},
  volume = {1014},
  year = {2013},
}

BibTeX entry:

@inproceedings{ BoPe-IJCAI13,
  address = {Beijing, China},
  author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}},
  booktitle = {Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI'13)},
  editor = {Francesca {Rossi}},
  pages = {789--795},
  publisher = {AAAI Press},
  title = {Positive Subsumption in Fuzzy $\mathcal{EL}$ with General t-norms},
  year = {2013},
}

Claudia Carapelle, Alexander Kartzow, and Markus Lohrey: Satisfiability of CTL* with Constraints. In Pedro R. D'Argenio and Hernán Melgratti, editors, CONCUR 2013 - Concurrency Theory, volume 8052 of Lecture Notes in Computer Science, pages 455–469. Springer Berlin Heidelberg, 2013.
Paper (PDF) DOI (The final publication is available at link.springer.com)

BibTeX entry:

@incollection{ CaKaLo-CONCUR13,
  author = {Claudia {Carapelle} and Alexander {Kartzow} and Markus {Lohrey}},
  booktitle = {CONCUR 2013 - Concurrency Theory},
  doi = {10.1007/978-3-642-40184-8_32},
  editor = {Pedro R. {D'Argenio} and Hern{\'a}n {Melgratti}},
  pages = {455--469},
  publisher = {Springer Berlin Heidelberg},
  series = {Lecture Notes in Computer Science},
  title = {Satisfiability of CTL* with Constraints},
  volume = {8052},
  year = {2013},
}

BibTeX entry:

@inproceedings{ DrGoe-NCMA13,
  address = {Ume{\aa}, Sweden},
  author = {Manfred {Droste} and Doreen {G{\"o}tze}},
  booktitle = {Non-Classical Models of Automata and Applications (NCMA)},
  editor = {Suna {Bensch} and Frank {Drewes} and Rudolf {Freund} and Friedrich {Otto}},
  pages = {101--116},
  publisher = {{\"O}sterreichische Computer Gesellschaft},
  series = {This email address is being protected from spambots. You need JavaScript enabled to view it.},
  title = {The Support of Nested Weighted Automata},
  year = {2013},
}

Manfred Droste and Vitaly Perevoshchikov: Multi-weighted Automata and MSO Logic. In Andrei A. Bulatov and Arseny M. Shur, editors, Proceedings of the 8th International Computer Science Symposium in Russia, volume 7913 of Lecture Notes in Artificial Intelligence, pages 418–430. Springer, 2013.
(The final publication is available at link.springer.com)

BibTeX entry:

@inproceedings{ DrPe-CSR13,
  author = {Manfred {Droste} and Vitaly {Perevoshchikov}},
  booktitle = {Proceedings of the 8th International Computer Science Symposium in Russia},
  editor = {Andrei A. {Bulatov} and Arseny M. {Shur}},
  pages = {418--430},
  publisher = {Springer},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Multi-weighted Automata and MSO Logic},
  volume = {7913},
  year = {2013},
}

BibTeX entry:

@inproceedings{ drovog13,
  author = {Manfred {Droste} and Heiko {Vogler}},
  booktitle = {Proceedings of the 17th International Conference on Developments in Language Theory (DLT 2013)},
  title = {The Chomsky-Sch\"{u}tzenberger Theorem for Quantitative Context-Free Languages},
  year = {2013},
}

Andreas Ecke, Rafael Peñaloza, and Anni-Yasmin Turhan: Computing Role-depth Bounded Generalizations in the Description Logic ELOR. In Proceedings of the 36th German Conference on Artificial Intelligence (KI 2013), volume 8077 of Lecture Notes in Artificial Intelligence. Koblenz, Germany, Springer-Verlag, 2013.
Abstract Paper (PDF) Extended technical report (PDF)

BibTeX entry:

@inproceedings{ EcPeTu-KI-13,
  address = {Koblenz, Germany},
  author = {Andreas {Ecke} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 36th German Conference on Artificial Intelligence (KI 2013)},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Computing Role-depth Bounded Generalizations in the Description Logic {$\mathcal{ELOR}$}},
  volume = {8077},
  year = {2013},
}

BibTeX entry:

@inproceedings{ EcPeTu-DL-13,
  address = {Ulm, Germany},
  author = {Andreas {Ecke} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  booktitle = {Proceedings of the 26th International Workshop on Description Logics ({DL-2013})},
  month = {July},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  title = {Role-depth bounded Least Common Subsumer in Prob-{$\mathcal{EL}$} with Nominals},
  year = {2013},
}

BibTeX entry:

@inproceedings{ EcPeTu-WL4AI-13,
  address = {Beijing, China},
  author = {Andreas {Ecke} and Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}},
  booktitle = {Workshop on {W}eighted {L}ogics for {AI} (in conjunction with IJCAI'13)},
  title = {Towards Instance Query Answering for Concepts Relaxed by Similarity Measures},
  year = {2013},
}

Uwe Ryssel, Felix Distel, and Daniel Borchmann: Fast algorithms for implication bases and attribute exploration using proper premises. Annals of Mathematics and Artificial Intelligence, Special Issue 65:1–29, 2013.
Abstract Paper (PDF) (The final publication is available at link.springer.com)

BibTeX entry:

@article{ RyDiBo-AMAI13,
  author = {Uwe {Ryssel} and Felix {Distel} and Daniel {Borchmann}},
  journal = {Annals of Mathematics and Artificial Intelligence},
  pages = {1--29},
  publisher = {Springer Netherlands},
  title = {Fast algorithms for implication bases and attribute exploration using proper premises},
  volume = {Special Issue 65},
  year = {2013},
}

2012

BibTeX entry:

@incollection{ Weidner-MFCS-2012,
  author = {Thomas {Weidner}},
  booktitle = {Mathematical Foundations of Computer Science 2012},
  doi = {10.1007/978-3-642-32589-2_70},
  editor = {Branislav {Rovan} and Vladimiro {Sassone} and Peter {Widmayer}},
  pages = {813--824},
  publisher = {Springer Berlin Heidelberg},
  series = {Lecture Notes in Computer Science},
  title = {Probabilistic Automata and Probabilistic Logic},
  volume = {7464},
  year = {2012},
}

Abstracts

The list of publications is also available as PDF document.

2022, 2021,
2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012

2022

Abstract:

Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The ``justifications'' usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.

Manfred Droste, Sven Dziadek, and Werner Kuich: Logic for omega-Pushdown Automata. Information and Computation, 282, 2022. Special issue on WATA 2018
BibTeX entry DOI

Abstract:

Context-free languages of infinite words have recently found increasing interest. Here, we will present a second-order logic with the same expressive power as Büchi or Muller pushdown automata for infinite words. This extends fundamental logical characterizations of Büchi, Elgot, Trakhtenbrot for regular languages of finite and infinite words and a more recent logical characterization of Lautemann, Schwentick and Thérien for context-free languages of finite words to ω-context-free languages. For our argument, we will investigate Greibach normal forms of ω-context-free grammars as well as a new type of Büchi pushdown automata which can alter their stack by at most one element and without ϵ-transitions. We show that they suffice to accept all ω-context-free languages. This enables us to use similar results recently developed for infinite nested words.

Abstract:

In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (as introduced by Cohen and Gold in 1977) and an extension of weighted context-free languages of finite words (that were already investigated by Chomsky and Schützenberger in 1963). As in the theory of formal grammars, these weighted context-free languages, or ω-algebraic series, can be represented as solutions of mixed ω-algebraic systems of equations and by weighted ω-pushdown automata. In our first main result, we show that (mixed) ω-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-reset automata do not use ϵ-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.

Abstract:

The generative capacity of combinatory categorial grammars (CCGs) as generators of tree languages is investigated. It is demonstrated that the tree languages generated by CCGs can also be generated by simple monadic context-free tree grammars. However, the important subclass of pure combinatory categorial grammars cannot even generate all regular tree languages. Additionally, the tree languages generated by combinatory categorial grammars with limited rule degrees are characterized: If only application rules are allowed, then these grammars can generate only a proper subset of the regular tree languages, whereas they can generate exactly the regular tree languages once first-degree composition rules are permitted.

2021

Abstract:

Logic-based approaches to AI have the advantage that their behavior can in principle be explained to a user. If, for instance, a Description Logic reasoner derives a consequence that triggers some action of the overall system, then one can explain such an entailment by presenting a proof of the consequence in an appropriate calculus. How comprehensible such a proof is depends not only on the employed calculus, but also on the properties of the particular proof, such as its overall size, its depth, the complexity of the employed sentences and proof steps, etc. For this reason, we want to determine the complexity of generating proofs that are below a certain threshold w.r.t. a given measure of proof quality. Rather than investigating this problem for a fixed proof calculus and a fixed measure, we aim for general results that hold for wide classes of calculi and measures. In previous work, we first restricted the attention to a setting where proof size is used to measure the quality of a proof. We then extended the approach to a more general setting, but important measures such as proof depth were not covered. In the present paper, we provide results for a class of measures called recursive, which yields lower complexities and also encompasses proof depth. In addition, we close some gaps left open in our previous work, thus providing a comprehensive picture of the complexity landscape.

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, and Alisa Kovtunova: Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Abstract). In Martin Homola, Vladislav Ryzhikov, and Renate A. Schmidt, editors, Proceedings of the 34th International Workshop on Description Logics (DL 2021) part of Bratislava Knowledge September (BAKS 2021), Bratislava, Slovakia, September 19th to 22nd, 2021, volume 2954 of CEUR Workshop Proceedings. CEUR-WS.org, 2021.
BibTeX entry Paper (PDF)

Abstract:

Although logical inferences are interpretable, actually explaining them to a user is still a challenging task. While sometimes it may be enough to point out the axioms from the ontology that lead to the consequence of interest, more complex inferences require proofs with intermediate steps that the user can follow. Our main hypothesis isthat different users need different representations of proofs for optimal understanding. To this end, we undertook some user experiments related to logical proofs. We explored how a user’s cognitive abilities influence the performance in and preference for certain proof representations. In particular, we compared tree-shaped representations with linear, textbased ones, and for each we offered an interactive and a static version. After each proof, participants had to solve some tasks measuring their level of understanding and rated each proof according to the perceived comprehensibility. At the end of the questionnaire, subjects ranked the proofs by comprehensibility. We found no differences between the general performance or the subjective ratings of the proof representations. However, in the final ranking participants preferred the conditions with tree-shaped proofs over the textual ones, with significant differences in the rankings of the higher cognitive ability group and across both groups but not in the low cognitive ability group.

Christian Alrabbaa, Stefan Borgwardt, Nina Knieriemen, Alisa Kovtunova, Anna Milena Rothermel, and Frederik Wiehr: In the Hand of the Beholder: Comparing Interactive Proof Visualizations (Extended Abstract). In Informal Proceedings of the Explainable Logic-Based Knowledge Representation (XLoKR 2021) workshop co-located with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), Online Event [Hanoi, Vietnam], November 3rd to 5th, 2021, 2021.
BibTeX entry Paper (PDF)

Abstract:

When subsumption relationships unexpectedly fail to be detected by a description logic reasoner, the cause for this non-entailment need not be evident. In this case, succinct automatically generated explanations would be helpful. Reasoners for the description logic EL compute the canonical model of a TBox in order to perform subsumption tests. We devise substructures of such models as relevant parts for explanation and propose an approach based on graph transductions to extract such relevant parts from canonical models.

Abstract:

When subsumption relationships unexpectedly fail to be detected by a description logic reasoner, the cause for this non-entailment need not be evident. In this case, succinct automatically generated explanations would be helpful. We devise substructures of such models as relevant parts suitable for explaining the non-entailment to users of description logic systems.

Abstract:

We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based on the notion of subgoals, which are slices of the game that the reachability player necessarily needs to pass through in order to reach the goal. We use Craig interpolation to identify these necessary sets of moves and recursively slice the game along these subgoals. Our approach allows us to infer winning strategies that are structured along the subgoals. If the game is won by the reachability player, this is a strategy that progresses through the subgoals towards the final goal; if the game is won by the safety player, it is a permissive strategy that completely avoids a single subgoal. We evaluate our prototype implementation on a range of different games. On multiple benchmark families, our prototype scales dramatically better than previously available tools.

Abstract:

We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters. More precisely, consider a d-dimensional square matrix M whose entries are algebraic functions in one or more real variables. Given initial and target vectors u,v ∈ ℚ^d, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix N ∈ ℝ^{d× d}, and a positive integer n ∈ ℕ, such that Nⁿ u = v. We show decidability for the case in which M depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.

Abstract:

The paper studies a probabilistic notion of causes in Markov chains that relies on the counterfactuality principle and the probability-raising property. This notion is motivated by the use of causes for monitoring purposes where the aim is to detect faulty or undesired behaviours before they actually occur. A cause is a set of finite executions of the system after which the probability of the effect exceeds a given threshold. We introduce multiple types of costs that capture the consump-tion of resources from different perspectives, and study the complexity of computing cost-minimal causes.

Manuel Bodirsky and Johannes Greiner: Tractable Combinations of Theories via Sampling. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, editors, Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, pages 133–146. Springer International Publishing, 2021.
BibTeX entry DOI (The final publication is available at link.springer.com)

Abstract:

For a first-order theory T, the Constraint Satisfaction Problem of T is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of T. In this article we develop sufficient conditions for polynomial-time tractability of the constraint satisfaction problem for the union of two theories with disjoint relational signatures. To this end, we introduce the concept of sampling for theories and show that samplings can be applied to examples which are not covered by the seminal result of Nelson and Oppen.

Frederic Dörband: Kleene and Büchi Theorems for Weighted Forest Languages over M-Monoids. Special issue of Information and Computation devoted to WATA 2020, 2021. In print
BibTeX entry DOI

Abstract:

We consider forests as tuples of trees and introduce weighted forest automata (wfa) over M- monoids. A wfa acts on each individual tree in a forest like a weighted tree automaton over the same M-monoid. In order to combine the values of trees in forests, a wfa uses an associative multiplication operation that distributes over the addition of the M-monoid. We continue by introducing two semantics for wfa, an “initial algebra”-like semantic and a run-semantic, and prove that these semantics are equal for distributive M-monoids. We prove that our automaton model accepts finite products of recognizable weighted tree languages over M-monoids. Next, we introduce rational weighted forest expressions and forest M-expressions over M-monoids and show that the classes of languages generated by these formalisms coincide with recognizable weighted forest languages under certain conditions on the underlying M-monoid.

Abstract:

We introduce the notion of t-approximated determinisation and the t-twinning property of weighted tree automata (WTA) over the tropical semiring. We provide an algorithm that accomplishes t-approximated determinisation of an input automaton 𝒜, whenever it terminates. Moreover, we prove that the t-twinning property of 𝒜 is a sufficient condition for the termination of our algorithm. Ultimately, we show decidability of the t-twinning property for WTA.

Abstract:

We introduce the notion of group-weighted tree automata over commutative groups and characterise sequentialisability of such automata. In particular, we introduce a fitting notion for tree distance and prove the equivalence between sequentialisability, the so-called Lipschitz property, and the so-called twinning property.

Abstract:

Knowledge engineers might face situations in which an unwanted consequence is derivable from an ontology. It is then desired to revise the ontology such that it no longer entails the consequence. For this purpose, we introduce a novel technique for repairing TBoxes formulated in the description logic EL. Specifically, we first compute a canonical model of the TBox and then transform it into a countermodel to the unwanted consequence. As formalism for the model transformation we employ transductions. We then obtain a TBox repair as the axiomatization of the logical intersection of the original TBox and the theory of the countermodel. In fact, we construct a set of countermodels, each of which induces a TBox repair. For the actual computation of the repairs we use results from Formal Concept Analysis.

Abstract:

A standard way of justifying that a certain probabilistic property holds in a system is to provide a witnessing subsystem (also called critical subsystem) for the property. Computing minimal witnessing subsystems is NP-hard already for acyclic Markov chains, but can be done in polynomial time for Markov chains whose underlying graph is a tree. This paper considers the problem for probabilistic systems that are similar to trees or paths. It introduces the parameters directed tree-partition width (dtpw) and directed path-partition width (dppw) and shows that computing minimal witnesses remains NP-hard for Markov chains with bounded dppw (and hence also for Markov chains with bounded dtpw). By observing that graphs of bounded dtpw have bounded width with respect to all known tree similarity measures for directed graphs, the hardness result carries over to these other tree similarity measures. Technically, the reduction proceeds via the conceptually simpler matrix-pair chain problem, which is introduced and shown to be NP-complete for nonnegative matrices of fixed dimension. Furthermore, an algorithm which aims to utilise a given directed tree partition of the system to compute a minimal witnessing subsystem is described. It enumerates partial subsystems for the blocks of the partition along the tree order, and keeps only necessary ones. A preliminary experimental analysis shows that it outperforms other approaches on certain benchmarks which have directed tree partitions of small width.

Abstract:

We study the problem of determinizing 𝜔-automata whose acceptance condition is defined on the transitions using Boolean formulas, also known as transition-based Emerson-Lei automata (TELA). The standard approach to determinize TELA first constructs an equivalent generalized Büchi automaton (GBA), which is later determinized. We introduce three new ways of translating TELA to GBA. Furthermore, we give a new determinization construction which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. We also study limit-determinization of TELA and show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

Abstract:

We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case.

Lena Katharina Schiffer and Andreas Maletti: Strong Equivalence of TAG and CCG. Transactions of the Association for Computational Linguistics, 9:707–720, 2021.
BibTeX entry DOI ©MIT Press

Abstract:

Tree-adjoining grammar (TAG) and combinatory categorial grammar (CCG) are two well-established mildly context-sensitive grammar formalisms that are known to have the same expressive power on strings (i.e., generate the same class of string languages). It is demonstrated that their expressive power on trees also essentially coincides. In fact, CCG without lexicon entries for the empty string and only first-order rules of degree at most 2 are sufficient for its full expressive power.

2020

Abstract:

Logic-based approaches to AI have the advantage that their behaviour can in principle be explained by providing their users with proofs for the derived consequences. However, if such proofs get very large, then it may be hard to understand a consequence even if the individual derivation steps are easy to comprehend. This motivates our interest in finding small proofs for Description Logic (DL) entailments. Instead of concentrating on a specific DL and proof calculus for this DL, we introduce a general framework in which proofs are represented as labeled, directed hypergraphs, where each hyperedge corresponds to a single sound derivation step. On the theoretical side, we investigate the complexity of deciding whether a certain consequence has a proof of size at most n along the following orthogonal dimensions: (i) the underlying proof system is polynomial or exponential; (ii) proofs may or may not reuse already derived consequences; and (iii) the number n is represented in unary or binary. We have determined the exact worst-case complexity of this decision problem for all but one of the possible combinations of these options. On the practical side, we have developed and implemented an approach for generating proofs for expressive DLs based on a non-standard reasoning task called forgetting. We have evaluated this approach on a set of realistic ontologies and compared the obtained proofs with proofs generated by the DL reasoner ELK, finding that forgetting-based proofs are often better w.r.t. different measures of proof complexity.

Abstract:

If a Description Logic (DL) system derives a consequence, then one can in principle explain such an entailment by presenting a proof of the consequence in an appropriate calculus. Intuitively, good proofs are ones that are simple enough to be comprehensible to a user of the system. In recent work, we have introduced a general framework in which proofs are represented as labeled, directed hypergraphs, and have investigated the complexity of finding small proofs. However, large size is not the only reason that can make a proof complex. In the present paper, we introduce other measures for the complexity of a proof, and analyze the computational complexity of deciding whether a given consequence has a proof of complexity at most q. This problem can be NP-complete even for EL , but we also identify measures where it can be decided in polynomial time.

Abstract:

The classical approach for repairing a Description Logic (DL) ontology in the sense of removing an unwanted consequence is to delete a minimal number of axioms from the ontology such that the resulting ontology no longer has the consequence. While there are automated tools for computing all possible such repairs, the user still needs to decide by hand which of the (potentially exponentially many) repairs to choose. In this paper, we argue that exploring a proof of the unwanted consequence may help us to locate other erroneous consequences within the proof, and thus allows us to make a more informed decision on which axioms to remove. In addition, we suggest that looking at the so-called atomic decomposition, which describes the modular structure of the ontology, enables us to judge the impact that removing a certain axiom has. Since both proofs and atomic decompositions of ontologies may be large, visual support for inspecting them is required. We describe a prototypical system that can visualize proofs and the atomic decomposition in an integrated visualization tool to support ontology debugging.

Abstract:

Approaches in knowledge representation based on formal logics and rule-based formalisms have the advantage that each step of reasoning can be understood by a user. However, often many of these inference steps are necessary, leading to a proof of the final conclusion that is hard to understand. If the set of inference rules is small, proofs may also look repetitious. Implemented systems (including the description logic (DL) reasoner ELK) that are able to produce formal proofs, are often bound to such predefined sets. In this work we present a black-box approach to generate proofs for expressive description logics (DLs) that are not based on a set of inference rules. Instead, it exploits the non-standard inference forgetting to generate intermediate proof steps. We have evaluated this approach on a set of realistic ontologies and compared the proofs obtained using the existing forgetting tools LETHE and Fame with ones generated by ELK.

Abstract:

Simple counting quantifiers that can be used to compare the number of role successors of an individual or the cardinality of a concept with a fixed natural number have been employed in Description Logics (DLs) for more than two decades under the respective names of number restrictions and cardinality restriction on concepts. Recently, we have considerably extended the expressivity of such quantifiers by allowing to impose set and cardinality constraints formulated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) on sets of role successors and concepts, respectively. We were able to prove that this extension does not increase the complexity of reasoning. In the present paper, we investigate the expressive power of the DLs obtained this way, using appropriate bisimulation characterizations and 0-1 laws as tools for distinguishing the expressiveness of different logics. In particular, we show that, in contrast to most classical DLs, these logics are no longer expressible in first-order predicate logic (FOL), and we characterize their first-order fragments. In most of our previous work on DLs with QFBAPA-based set and cardinality constraints we have employed finiteness restrictions on interpretations to ensure that the obtained sets are finite. Here we dispense with these restrictions to make the comparison with classical DLs, where one usually considers arbitrary models rather than finite ones, easier. It turns out that doing so does not change the complexity of reasoning.

Abstract:

Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones considered in the previous proofs may cause undecidability. To regain decidability in the presence of GCIs, quite strong restrictions, in sum called omega-admissiblity, need to be imposed on the concrete domain. On the one hand, we generalize the notion of omega-admissiblity from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate omega-admissiblity to well-known notions from model theory. In particular, we show that finitely bounded, homogeneous structures yield omega-admissible concrete domains. This allows us to show omega-admissibility of concrete domains using existing results from model theory.

Abstract:

We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix M ∈ ℚ^{d × d}, an initial vector x ∈ ℚ^d, a granularity g ∈ ℚ₊ and a rounding operation [⋅] projecting a vector of ℚ^d onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit 𝒪 = ⟨[x], [M[x]],[M[M[x]]],… ⟩, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability - whether a given target y ∈ ℚ^d belongs to 𝒪 - is PSPACE-complete for hyperbolic systems (when no eigenvalue of M has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.

Abstract:

The CSP of a first-order theory T is the problem of deciding for a given finite set S of atomic formulas whether T u S is satisfiable. Let T1 and T2 be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of CSP(T1 u T2) under the assumption that CSP(T1) and CSP(T2) are decidable (or polynomial-time decidable). We show that for a large class of omega-categorical theories T1, T2 the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of CSP(T1 u T2) (unless P=NP).

Abstract:

Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes can be described by a strong height-one Maltsev condition. For infinite-domain CSPs, the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (Q;<); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs.

Abstract:

Recently, weighted ω-pushdown automata have been introduced by Droste, Ésik, Kuich. This new type of automaton has access to a stack and models quantitative aspects of infinite words. Here, we consider a simple version of those automata. The simple ω-pushdown automata do not use ε-transitions and have a very restricted stack access. In previous work, we could show this automaton model to be expressively equivalent to context-free ω-languages in the unweighted case. Furthermore, semiring-weighted simple ω-pushdown automata recognize all ω-algebraic series. Here, we consider ω-valuation monoids as weight structures. As a first result, we prove that for this weight structure and for simple ω-pushdown automata, Büchi-acceptance and Muller-acceptance are expressively equivalent. In our second result, we derive a Nivat theorem for these automata stating that the behaviors of weighted ω-pushdown automata are precisely the projections of very simple ω-series restricted to ω-context-free languages. The third result is a weighted logic with the same expressive power as the new automaton model. To prove the equivalence, we use a similar result for weighted nested ω-word automata and apply our present result of expressive equivalence of Muller and Büchi acceptance.

Abstract:

As the creation of large ontologies is a difficult and error-prone process, we think it is particularly relevant to develop new visual and interactive tools that support exploring ontologies as well as finding and resolving defects, such as undesired logical entailments. Exhibiting formal proofs for the undesired entailments can help in understanding how a defect happens, and linking the steps in the proof to the ontology can help in determining how the defect can be fixed. We present an interface that visualizes proofs and the corresponding ontology in form of side-by-side node-link diagrams. Building on linked brushing, users benefit from a strong interplay between these views, which allows for discovering and understanding defects. Besides traditional desktop workplaces, our interaction design also considers the use of touch input enabled by interactive displays. As part of an iterative design process, we developed an initial web-based prototype implementation and gathered feedback from an interview with domain experts. With this ongoing research and development, we aim to further investigate the potential and general utility of interactive visualizations for ontology engineering.

Abstract:

This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an MDP-variant of Farkas' Lemma. The set of all such certificates is shown to form a polytope whose points correspond to witnessing subsystems of the model and the property. Using this correspondence we can translate the problem of finding minimal witnesses to the problem of finding vertices with a maximal number of zeros. While computing such vertices is computationally hard in general, we derive new heuristics from our formulations that exhibit competitive performance compared to state-of-the-art techniques. As an argument that asymptotically better algorithms cannot be hoped for, we show that the decision version of finding minimal witnesses is NP-complete even for acyclic Markov chains.

Abstract:

Models for Description Logic (DL) ontologies can be used for explanation purposes, but the models computed by standard DL reasoner systems are not necessarily suitable for this task. In this paper we investigate the general task of transforming an arbitrary model into a target model that admits the desired property. To this end, we introduce a general framework for model transformation that abstracts from the DL in use, the property of the target model and the transformation formalism. We consider instantiations of the framework for the DLs ALC and EL and use transductions as transformation formalism.

Simon Jantsch, Florian Funke, and Christel Baier: Minimal Witnesses for Probabilistic Timed Automata. In Automated Technology for Verification and Analysis (ATVA), 2020.
BibTeX entry DOI

Abstract:

Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity.

Abstract:

The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding number-theoretic problems whose decidability has been open for many decades. In this paper, the inherent mathematical difficulty of a series of optimization problems on Markov decision processes (MDPs) is shown by a reduction from the Positivity problem to the associated decision problems which establishes that the problems are also at least as hard as the Skolem problem as an immediate consequence. The optimization problems under consideration are two non-classical variants of the stochastic shortest path problem (SSPP) in terms of expected partial or conditional accumulated weights, the optimization of the conditional value-at-risk for accumulated weights, and two problems addressing the long-run satisfaction of path properties, namely the optimization of long-run probabilities of regular co-safety properties and the model-checking problem of the logic frequency-LTL. To prove the Positivity- and hence Skolem-hardness for the latter two problems, a new auxiliary path measure, called weighted long-run frequency, is introduced and the Positivity-hardness of the corresponding decision problem is shown as an intermediate step. For the partial and conditional SSPP on MDPs with non-negative weights and for the optimization of long-run probabilities of constrained reachability properties (a U b), solutions are known that rely on the identification of a bound on the accumulated weight or the number of consecutive visits to certain sates, called a saturation point, from which on optimal schedulers behave memorylessly. In this paper, it is shown that also the optimization of the conditional value-at-risk for the classical SSPP and of weighted long-run frequencies on MDPs with non-negative weights can be solved in pseudo-polynomial time exploiting the existence of a saturation point. As a consequence, one obtains the decidability of the qualitative model-checking problem of a frequency-LTL formula that is not included in the fragments with known solutions.

2019

Abstract:

We present a method for answering ontology-mediated queries for DL-Lite extended with a concrete domain, where we allow concrete domain predicates to be used in the query as well. Our method is based on query rewriting, a well-known technique for ontology-based query answering (OBQA), where the knowledge provided by the ontology is compiled into the query so that the rewritten query can be evaluated directly over a database. This technique reduces the problem of query answering w.r.t. an ontology to query evaluation over a database instance. Specifically, we consider members of the DL-Lite family extended with unary and binary concrete domain predicates over the real numbers. While approaches for query rewriting DL-Lite with these concrete domain have been investigated theoretically, these approaches use a combined approach in which also the data is processed, and require the concrete domain values occurring in the data to be known in advance, which makes the procedure data-dependent. In contrast, we show how rewritings can be computed in a data-independent fashion.

Franz Baader and Filippo De Bortoli: On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets. In Andreas Herzig and Andrei Popescu, editors, Proc. of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019), volume 11715 of Lecture Notes in Computer Science, pages 203–219. Springer, 2019.
BibTeX entry Paper (PDF) DOI (The final publication is available at link.springer.com) ©Springer Nature Switzerland AG 2019

Abstract:

In recent work we have extended the description logic (DL) by means of more expressive number restrictions using numerical and set constraints stated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA). It has been shown that reasoning in the resulting DL, called ALCSCC, is PSpace-complete without a TBox and ExpTime-complete w.r.t. a general TBox. The semantics of ALCSCC is defined in terms of finitely branching interpretations, that is, interpretations where every element has only finitely many role successors. This condition was needed since QFBAPA considers only finite sets. In this paper, we first introduce a variant of ALCSCC, called ALCSCC^\infty, in which we lift this requirement (inexpressible in first-order logic) and show that the complexity results for ALCSCC mentioned above are preserved. Nevertheless, like ALCSCC, ALCSCC^\infty is not a fragment of first-order logic. The main contribution of this paper is to give a characterization of the first-order fragment of ALCSCC^\infty. The most important tool used in the proof of this result is a notion of bisimulation that characterizes this fragment.

Abstract:

Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics two decades ago, motivated by applications in the Classic system. Shortly afterwards, a polynomial-time matching algorithm was developed for the DL FL0. However, this algorithm cannot deal with general TBoxes (i.e., finite sets of general concept inclusions). Here we show that matching in FL0 w.r.t. general TBoxes is in ExpTime, which is the best possible complexity for this problem since already subsumption w.r.t. general TBoxes is ExpTime-hard in FL0. We also show that, w.r.t. a restricted form of TBoxes, the complexity of matching in FL0 can be lowered to PSpace.

Abstract:

The paper introduces the concepts of long-run frequency of path properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. We then study the natural optimization problem of computing the optimal values of these measures, when ranging over all paths or all schedulers, and the corresponding decision problem when given a threshold. The main results are as follows. For (repeated) reachability and other simple properties, optimal long-run probabilities and corresponding optimal memoryless schedulers are computable in polynomial time. When it comes to constrained reachability properties, memoryless schedulers are no longer sufficient, even in the non-probabilistic setting. Nevertheless, optimal long-run probabilities for constrained reachability are computable in pseudo-polynomial time in the probabilistic setting and in polynomial time for Kripke structures. Finally for co-safety properties expressed by NFA, we give an exponential-time algorithm to compute the optimal long-run frequency, and prove the PSPACE-completeness of the threshold problem.

Abstract:

We define the class of rational weighted tree languages with storage over complete, not necessarily commutative, semirings and we repeat its charaterization by weighted regular tree grammars with storage. Moreover, we show an alternative proof of the fact that the class of rational weighted tree languages with storage is closed under the rational operations, i.e., top-concatenation, scalar multiplication, sum, tree concatenation, and Kleene-star, where the latter two closure results require that the storage has a reset instruction.

Abstract:

In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of omega-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted languages, or omega-algebraic series, can be represented as solutions of mixed omega-algebraic systems of equations and by weighted omega-pushdown automata. In our first main result, we show that mixed omega-algebraic systems can be transformed into Greibach normal form. Our second main result proves that simple omega-reset pushdown automata recognize all omega-algebraic series that are a solution of an omega-algebraic system in Greibach normal form. Simple reset automata do not use epsilon-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted languages.

Manfred Droste, Sven Dziadek, and Werner Kuich: Weighted simple reset pushdown automata. Theoretical Computer Science, 777:252–259, 2019.
BibTeX entry DOI

Abstract:

We define a new normal form for weighted pushdown automata. The new type of automaton uses a stack but has only limited access to it. Only three stack commands are available: popping a symbol, pushing a symbol or leaving the stack unaltered. Additionally, ϵ-transitions are not used. We prove that this automaton model can recognize all weighted context-free languages (i.e., generates all algebraic power series).

Abstract:

This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool Duggi and discuss experimental results that compare the automata sizes and computation times of Duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.

Abstract:

The generative capacity of combinatory categorial grammars as acceptors of tree languages is investigated. It is demonstrated that the such obtained tree languages can also be generated by simple monadic context-free tree grammars. However, the subclass of pure combinatory categorial grammars cannot even accept all regular tree languages. Additionally, the tree languages accepted by combinatory categorial grammars with limited rule degrees are characterized: If only application rules are allowed, then they can accept only a proper subset of the regular tree languages, whereas they can accept exactly the regular tree languages once first degree composition rules are permitted.

Erik Paul: Finite Sequentiality of Unambiguous Max-Plus Tree Automata. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 55:1–55:17, 2019.
BibTeX entry

Abstract:

The paper addresses two variants of the stochastic shortest path problem ("optimize the accumulated weight until reaching a goal state") in Markov decision processes (MDPs) with integer weights. The first variant optimizes partial expected accumulated weights, where paths not leading to a goal state are assigned weight 0, while the second variant considers conditional expected accumulated weights, where the probability mass is redistributed to paths reaching the goal. Both variants constitute useful approaches to the analysis of systems without guarantees on the occurrence of an event of interest (reaching a goal state), but have only been studied in structures with non-negative weights. Our main results are as follows. There are polynomial-time algorithms to check the finiteness of the supremum of the partial or conditional expectations in MDPs with arbitrary integer weights. If finite, then optimal weight-based deterministic schedulers exist. In contrast to the setting of non-negative weights, optimal schedulers can need infinite memory and their value can be irrational. However, the optimal value can be approximated up to an absolute error of eps in time exponential in the size of the MDP and polynomial in log(1/eps).

Abstract:

Minimal inconsistent subsets of knowledge bases in monotonic logics play an important role when investigating the reasons for conflicts and trying to handle them. In the context of non-monotonic reasoning this notion is not as meaningful due to the possibility of resolving conflicts by adding information. In this paper we investigate inconsistency in non-monotonic logics while taking this issue into account. In particular, we show that the well-known classical duality between hitting sets of minimal inconsistent subsets and maximal consistent subsets generalizes to arbitrary logics even if we allow adding novel information to a given knowledge base. We illustrate the versatility of the main theorems by covering more sophisticated situations and demonstrate how to utilize our results to analyze inconsistency in abstract argumentation.

2018

Abstract:

Even for small logic programs, the number of resulting answer-sets can be tremendous. In such cases, users might be incapable of comprehending the space of answer-sets as a whole nor being able to identify a specific answer-set according to their needs. To overcome this difficulty, we propose a general formal framework that takes an arbitrary logic program as input, and allows for navigating the space of answer- sets in a systematic interactive way analogous to faceted browsing. The navigation is carried out stepwise, where each step narrows down the remaining solutions, eventually arriving at a single one. We formulate two navigation modes, one stringent conflict avoiding, and a “free” mode, where conflicting selections of facets might occur. For the latter mode, we provide efficient algorithms for resolving the conflicts. We provide an implementation of our approach and demonstrate that our framework is able to handle logic programs for which it is currently infeasible to retrieve all answer sets.

Abstract:

Although being quite inexpressive, the description logic (DL) FL0, which provides only conjunction, value restriction and the top concept as concept constructors, has an intractable subsumption problem in the presence of terminologies (TBoxes): subsumption reasoning w.r.t. acyclic FL0 TBoxes is coNP-complete, and becomes even ExpTime-complete in case general TBoxes are used. In the present paper, we use automata working on infinite trees to solve both standard and non-standard inferences in FL0 w.r.t. general TBoxes. First, we give an alternative proof of the ExpTime upper bound for subsumption in FL0 w.r.t. general TBoxes based on the use of looping tree automata. Second, we employ parity tree automata to tackle non-standard inference problems such as computing the least common subsumer and the difference of FL0 concepts w.r.t. general TBoxes.

Abstract:

It is well-known that the unification problem for a binary associative-commutative-idempotent function symbol with a unit (ACUI-unification) is polynomial for unification with constants and NP-complete for general unification. We prove that the same is true if we add a finite set of ground identities. To be more precise, we first show that not only unification with constants, but also unification with linear constant restrictions is in P for any extension of ACUI with a finite set of ground identities. Using well-known combination results for unification algorithms, this then yields an NP-upper bound for general unification modulo such a theory. The matching lower bound can be shown as in the case without ground identities.

Abstract:

Ontology-mediated query answering can be used to access large data sets through a mediating ontology. It has drawn considerable attention in the Description Logic (DL) community where both the complexity of query answering and practical query answering approaches based on rewriting were investigated in detail. Surprisingly, there is still a gap in what is known about the data complexity of query answering w.r.t. ontologies formulated in the inexpressive DL FL0. While it is known that the data complexity of answering conjunctive queries w.r.t. FL0 ontologies is coNP-complete, the exact complexity of answering instance queries was open until now. In the present paper, we show that answering instance queries w.r.t. FL0 ontologies is in P for data complexity. Together with the known lower bound of P-completeness for a fragment of FL0, this closes the gap mentioned above.

Parvaneh Babari, Manfred Droste, and Vitaly Perevoshchikov: Weighted register automata and weighted logic on data words. Theoretical Computer Science, 744:3–21, 2018.
BibTeX entry DOI

Abstract:

Data words are sequences of pairs where the first element is taken from a finite alphabet and the second element is taken from an infinite data domain. Register automata provide a widely studied model for reasoning on data words. In this paper, we investigate automata models for quantitative aspects of systems with infinite data domains, e.g., the costs of storing data on a remote server or the consumption of resources (e.g., memory, energy, time) during a data analysis. We introduce weighted register automata on data words over commutative data semirings equipped with a collection of binary data functions, and we investigate their closure properties. Unlike the other models considered in the literature, we allow data comparison by means of an arbitrary collection of binary data relations. This enables us to incorporate timed automata and weighted timed automata into our framework. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic; for the proof we employ a new class of determinizable visibly register automata.

Abstract:

Conflicting information in an agent's knowledge base may lead to a semantical defect, that is, a situation where it is impossible to draw any plausible conclusion. Finding out the reasons for the observed inconsistency (so-called diagnosis) and/or restoring consistency in a certain minimal way (so-called repairs) are frequently occurring issues in knowledge representation and reasoning. In this paper we provide a series of first results for these problems in the context of abstract argumentation theory regarding the two most important reasoning modes, namely credulous as well as sceptical acceptance. Our analysis includes the following problems regarding minimal repairs/diagnosis: existence, verification, computation of one and enumeration of all solutions. The latter problem is tackled with a version of the so-called hitting set duality first introduced by Raymond Reiter in 1987. It turns out that grounded semantics plays an outstanding role not only in terms of complexity, but also as a useful tool to reduce the search space for diagnosis regarding other semantics.

Manuel Bodirsky and Johannes Greiner: Complexity of Combinations of Qualitative Constraint Satisfaction Problems. In Didier, Galmiche, Stephan, Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning (IJCAR), volume 10900 of Lecture Notes in Computer Science, pages 263–278. Springer International Publishing, 2018.
BibTeX entry DOI (The final publication is available at link.springer.com)

Abstract:

Manuel Bodirsky, Peter Jonsson, Barnaby Martin, and Antoine Mottet: Classification Transfer for Qualitative Reasoning Problems. In Proceedings of IJCAI'18, 2018.
BibTeX entry

Manuel Bodirsky, Florent Madelaine, and Antoine Mottet: A universal-algebraic proof of the dichotomy for Monotone Monadic SNP. In Proceedings of LICS'18, pages 105–114, 2018.
BibTeX entry DOI

Manuel Bodirsky, Marcello Mamino, Barnaby Martin, and Antoine Mottet: The complexity of disjunctive linear Diophantine constraints. In Proceedings of MFCS'18, 2018.
BibTeX entry

Manuel Bodirsky and Antoine Mottet: A Dichotomy for First-Order Reducts of Unary Structures. Logical Methods in Computer Science, Volume 14, Issue 2, 2018.
BibTeX entry DOI

Gerhard Brewka, Matthias Thimm, and Markus Ulbricht: Strong inconsistency. Artificial Intelligence, 267:78–117, 2018.
BibTeX entry DOI

Abstract:

Minimal inconsistent subsets of knowledge bases play an important role in propositional logic, most notably for diagnosis, axiom pinpointing, and inconsistency measurement. It turns out that for nonmonotonic reasoning a stronger notion is needed. In this paper we develop such a notion, called strong inconsistency. We show that—in an arbitrary logic, monotonic or not—minimal strongly inconsistent subsets play a similar role as minimal inconsistent subsets in propositional logic. In particular, we show that the well-known duality between hitting sets of minimal inconsistent subsets and maximal consistent subsets generalises to arbitrary logics if the strong notion of inconsistency is used. We investigate the complexity of various related reasoning problems and present a generic algorithm for computing minimal strongly inconsistent subsets of a knowledge base. We also demonstrate the potential of our new notion for applications, focusing on axiom pinpointing and inconsistency measurement.

Manfred Droste and Erik Paul: A Feferman-Vaught decomposition theorem for weighted MSO logic. In Proceedings of MFCS'18, 2018.
BibTeX entry

Abstract:

The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one way to tackle the challenging state explosion problem, PRISM supports symbolic storage and manipulation using multi-terminal binary decision diagrams for representing the models and in the computations. However, it lacks automated heuristics for variable reordering, even though it is well known that the order of BDD variables plays a crucial role for compact representations and efficient computations. In this article we present a collection of extensions to PRISM. First, we provide support for automatic variable reordering within the symbolic engines of PRISM and allow users to manually control the variable ordering at a fine-grained level. Second, we provide extensions in the realm of reward-bounded properties, namely symbolic computations of quantiles in Markov decision processes and, for both the explicit and symbolic engines, the approximative computation of quantiles for continuous time Markov chains as well as support for multi-reward-bounded properties. Finally, we provide an implementation for obtaining minimal weak deterministic Büchi automata for the obligation fragment of Linear Temporal Logic (LTL), with applications for expected accumulated reward computations with a finite horizon given by a co-safe LTL formula.

Abstract:

Defeasible Description Logics (DDLs) extend Description Logics with defeasible concept inclusions. Reasoning in DDLs often employs rational closure according to the (propositional) KLM postulates. A well-known approach to lift this closure to DDLs is by so-called materialisation. Previously investigated algorithms for materialisation-based reasoning employ reductions to classical reasoning using all Boolean connectors. As a first result in this paper, we present a materialisation-based algorithm for the sub-Boolean DDL EL_bot, using a reduction to reasoning in classical EL_bot, rendering materialisation-based defeasible reasoning tractable. The main contribution of this article is a kind of canonical model construction, which can be used to decide defeasible subsumption and instance queries in EL_bot under rational and the stronger relevant entailment. Our so-called typicality models can reproduce the entailments obtained from materialisation-based rational and relevant closure and, more importantly, obtain stronger versions of rational and relevant entailment. These do not suffer from neglecting defeasible information for concepts appearing nested inside quantifications, which all materialisation-based approaches do. We also show the computational complexity of defeasible subsumption and instance checking in our stronger rational and relevant semantics.

Abstract:

We address the issue of quantitatively assessing the severity of inconsistencies in nonmonotonic frameworks. While measuring inconsistency in classical logics has been investigated for some time now, taking the nonmonotonicity into account poses new challenges. In order to tackle them, we focus on the structure of minimal strongly K-inconsistent subsets of a knowledge base K—a generalization of minimal inconsistency to arbitrary, possibly nonmonotonic, frameworks. We propose measures based on this notion and investigate their behavior in a nonmonotonic setting by revisiting existing rationality postulates, analyzing the compliance of the proposed measures with these postulates, and by investigating their computational complexity.

2017

Abstract:

In a recent research paper, we have proposed an extension of the light-weight Description Logic (DL) EL in which concepts can be defined in an approximate way. To this purpose, the notion of a graded membership function m, which instead of a Boolean membership value 0 or 1 yields a membership degree from the interval [0,1], was introduced. Threshold concepts can then, for example, require that an individual belongs to a concept C with degree at least 0.8. Reasoning in the threshold DL tel(m) obtained this way of course depends on the employed graded membership function m. The paper defines a specific such function, called deg, and determines the exact complexity of reasoning in tel(deg). In addition, it shows how concept similarity measures (CSMs) satisfying certain properties can be used to define graded membership functions m , but it does not investigate the complexity of reasoning in the induced threshold DLs tel(m ). In the present paper, we start filling this gap. In particular, we show that computability of implies decidability of tel(m ), and we introduce a class of CSMs for which reasoning in the induced threshold DLs has the same complexity as in tel(deg).

Abstract:

Recently introduced approaches for relaxed query answering, approximately defining concepts, and approximately solving unification problems in Description Logics have in common that they are based on the use of concept comparison measures together with a threshold construction. In this paper, we will briefly review these approaches, and then show how weighted automata working on infinite trees can be used to construct computable concept comparison measures for FL0 that are equivalence invariant w.r.t. general TBoxes. This is a first step towards employing such measures in the mentioned approximation approaches.

Abstract:

Both matching and unification in the Description Logic FL0 can be reduced to solving certain formal language equations. In previous work, we have extended unification in FL0 to approximate unification, and have shown that approximate unification can be reduced to approximately solving language equations. An approximate solution of a language equation need not make the languages on the left- and right-hand side of the equation equal, but close w.r.t. a given distance function. In the present paper, we consider approximate matching. We show that, for a large class of distance functions, approximate matching is in NP. We then consider a particular distance function d1(K,L) = 2⁻n, where n is the length of the shortest word in the symmetric difference of the languages K, L, and show that w.r.t. this distance function approximate matching is polynomial.

Abstract:

Minimal inconsistent subsets of knowledge bases play an important role in classical logics, most notably for repair and inconsistency measurement. It turns out that for nonmonotonic reasoning a stronger notion is needed. In this paper we develop such a notion, called strong inconsistency. We show that—in an arbitrary logic, monotonic or not—minimal strongly inconsistent subsets play the same role as minimal inconsistent subsets in classical reasoning. In particular, we show that the well-known classical duality between hitting sets of minimal inconsistent subsets and maximal consistent subsets generalises to arbitrary logics if the strong notion of inconsistency is used. We investigate the complexity of various related reasoning problems and present a generic algorithm for computing minimal strongly inconsistent subsets of a knowledge base. We also demonstrate the potential of our new notion for applications, focusing on repair and inconsistency measurement.

Manfred Droste and Stefan Dück: Weighted Automata and Logics for Infinite Nested Words. Inf. Comp., 253, Part 3:448–466, 2017.
BibTeX entry DOI

Manfred Droste, Stefan Dück, Dino Mandrioli, and Matteo Pradella: Weighted Operator Precedence Languages. In Proceedings of MFCS'17, pages 31:1–31:15, 2017.
BibTeX entry

Andreas Ecke: Quantitative Methods for Similarity in Description Logics. Künstliche Intelligenz, 2017. To appear
BibTeX entry

Abstract:

We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are -automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure allows the shift of complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction that exploits knowledge of its components to reduce the number of states. We identify two fragments of LTL, for which one can easily construct deterministic automata and show how knowledge of these components can reduce the number of states. We extend this idea to a general LTL framework, where we can use arbitrary LTL to deterministic automata translators for parts of formulas outside the mentioned fragments. Further, we show succinctness of the translation compared to existing construction. The construction is implemented in the tool Delag, which we evaluate on several benchmarks of LTL formulas and probabilistic model checking case studies.

Erik Paul: Monitor logics for quantitative monitor automata. In Proceedings of MFCS'17, 2017.
BibTeX entry

Erik Paul: The equivalence, unambiguity and sequentiality problems of finitely ambiguous max-plus tree automata are decidable. In Proceedings of MFCS'17, 2017.
BibTeX entry

Abstract:

Defeasible Description Logics (DDLs) extend classical Description Logics with defeasible concept inclusions and offer thereby a form of non-monotonicity. For reasoning in such settings often the rational closure according to the well-known KLM postulates (for propositional logic) was employed in earlier approaches. If in DDLs that use quantification a defeasible subsumption relationship holds between two concepts, such a relationship might also hold if these concepts appear nested in existential restrictions. Earlier reasoning algorithms for DDLs do not detect this kind of defeasible subsumption relationships. We devise a new form of canonical models that extend classical canonical models for EL_bot by elements that satisfy increasing amounts of defeasible knowledge. We show that reasoning based on these models yields the missing entailments.

Abstract:

Defeasible Description Logics (DDLs) extend Description Logics with defeasible concept inclusions. Reasoning in DDLs often employs rational or relevant closure according to the (propositional) KLM postulates. If in DDLs with quantification a defeasible subsumption relationship holds between concepts, this relationship might also hold if these concepts appear in existential restrictions. Such nested defeasible subsumption relationships were not detected by earlier reasoning algorithms—neither for rational nor relevant closure. Recently, we devised a new approach for EL_bot that alleviates this problem for rational closure by the use of typicality models that extend classical canonical models by domain elements that individually satisfy any amount of consistent defeasible knowledge. In this paper we lift our approach to relevant closure and show that reasoning based on typicality models yields the missing entailments.

2016

Abstract:

We introduce an extension to Description Logics that allows us to use prototypes to define concepts. To accomplish this, we introduce the notion of a prototype distance functions (pdf), which assign to each element of an interpretation a distance value. Based on this, we define a new concept constructor of the form P n(d) for being a relation from ≤,<,≥,>, which is interpreted as the set of all elements with a distance n according to the pdf d. We show how weighted alternating parity tree automata (wapta) over the integers can be used to define pdfs, and how this allows us to use both concepts and pointed interpretations as prototypes. Finally, we investigate the complexity of reasoning in ALCP(wapta), which extends the Description Logic ALC with prototype constructors for pdfs defined using wapta.

Abstract:

In a previous paper, we have introduced an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we have defined a graded membership function deg, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C t for in <, <=, >, >= then collect all the individuals that belong to C with degree t. We have then investigated the complexity of reasoning in the Description Logic tEL(deg), which is obtained from EL by adding such threshold concepts. In the present paper, we extend these results, which were obtained for reasoning without TBoxes, to the case of reasoning w.r.t. acyclic TBoxes. Surprisingly, this is not as easy as might have been expected. On the one hand, one must be quite careful to define acyclic TBoxes such that they still just introduce abbreviations for complex concepts, and thus can be unfolded. On the other hand, it turns out that, in contrast to the case of EL, adding acyclic TBoxes to tEL(deg) increases the complexity of reasoning by at least on level of the polynomial hierarchy.

Manuel Bodirsky, Victor Dalmau, Barnaby Martin, Antoine Mottet, and Michael Pinsker: Distance Constraint Satisfaction Problems. Information and Computation, 247:87–105, 2016.
BibTeX entry DOI

Abstract:

Reasoning for Description logics with concrete domains and w.r.t. general TBoxes easily becomes undecidable. However, with some restriction on the concrete domain, decidability can be regained. We introduce a novel way to integrate concrete domains D into the well-known description logic ALC, we call the resulting logic ALCP(D). We then identify sufficient conditions on D that guarantee decidability of the satisfiability problem, even in the presence of general TBoxes. In particular, we show decidability of ALCP(D) for several domains over the integers, for which decidabil- ity was open. More generally, this result holds for all negation-closed concrete domains with the EHD-property, which stands for ‘the exis- tence of a homomorphism is definable’. Such technique has recently been used to show decidability of CTL∗ with local constraints over the integers.

M. Droste and V. Perevoshchikov: Multi-weighted automata and MSO logic. Theory of Computing Systems, 2016. DOI: 10.1007/s00224-015-9658-9. Accepted for publication.
BibTeX entry

Abstract:

For modeling and reasoning about complex systems, symbolic methods provide a prominent way to tackle the state explosion problem. It is well-known that for symbolic approaches based on binary decision diagrams (BDD), the ordering of BDD variables plays a crucial role for compact representations and efficient computations. We have extended the popular probabilistic model checker PRISM with support for automatic variable reordering in its multi-terminal-BDD-based engines and report on benchmark results. Our extensions additionally allow the user to manually control the variable ordering at a finer-grained level. Furthermore, we present our implementation of the symbolic computation of quantiles and support for multi-reward-bounded properties, automata specifications and accepting end component computations for Streett conditions.

Abstract:

We introduce a weighted MSO-logic in which one outermost existential quantification over behaviours of a storage type is allowed. As weight structures we take unital valuation monoids which include all semirings, bounded lattices, and computations of average or discounted costs. Each formula is interpreted over finite words yielding elements in the weight structure. We prove that this logic is expressively equivalent to weighted automata with storage. In particular, this implies a Büchi-Elgot-Trakhtenbrot Theorem for weighted iterated pushdown languages. For this choice of storage type, the satisfiability problem of the logic is decidable for each bounded lattice provided that its infimum is computable.

2015

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporal Query Entailment in the Description Logic SHQ. Journal of Web Semantics, 33:71–93, 2015.
BibTeX entry DOI

Abstract:

Ontology-based data access (OBDA) generalizes query answering in databases towards deductive entailment since (i) the fact base is not assumed to contain complete knowledge (i.e., there is no closed world assumption), and (ii) the interpretation of the predicates occurring in the queries is constrained by axioms of an ontology. OBDA has been investigated in detail for the case where the ontology is expressed by an appropriate Description Logic (DL) and the queries are conjunctive queries. Motivated by situation awareness applications, we investigate an extension of OBDA to the temporal case. As the query language we consider an extension of the well-known propositional temporal logic LTL where conjunctive queries can occur in place of propositional variables, and as the ontology language we use the expressive DL SHQ. For the resulting instance of temporalized OBDA, we investigate both data complexity and combined complexity of the query entailment problem. In the course of this investigation, we also establish the complexity of consistency of Boolean knowledge bases in SHQ.

Abstract:

We introduce an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we use a graded membership function, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C t for in <,<=,>,>= then collect all the individuals that belong to C with degree t. We generalize a well-known characterization of membership in EL concepts to construct a specific graded membership function deg , and investigate the complexity of reasoning in the Description Logic tauEL(deg), which extends EL by threshold concepts defined using deg . We also compare the instance problem for threshold concepts of the form C >t in tauEL(deg) with the relaxed instance queries of Ecke et al.

Abstract:

We propose a flexible exchange format for omega-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people's work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporalizing Rewritable Query Languages over Knowledge Bases. Journal of Web Semantics, 33:50–70, 2015.
BibTeX entry DOI

Abstract:

Ontology-based data access (OBDA) generalizes query answering in relational databases. It allows to query a database by using the language of an ontology, abstracting from the actual relations of the database. OBDA can sometimes be realized by compiling the information of the ontology into the query and the database. The resulting query is then answered using classical database techniques. In this paper, we consider a temporal version of OBDA. We propose a generic temporal query language that combines linear temporal logic with queries over ontologies. This language is well-suited for expressing temporal properties of dynamic systems and is useful in context-aware applications that need to detect specific situations. We show that, if atemporal queries are rewritable in the sense described above, then the corresponding temporal queries are also rewritable such that we can answer them over a temporal database. We present three approaches to answering the resulting queries.

M. Droste and D. Heusel: The supports of weighted unranked tree automata. Fundamenta Informaticae, 136:37–58, 2015.
BibTeX entry

Abstract:

We introduce a new behavior of weighted unranked tree automata. We prove a characterization of this behavior by two fragments of weighted MSO logic and thereby provide a solution of an open equivalence problem of Droste and Vogler. The characterization works for valuation monoids as weight structures; they include all semirings and, in addition, enable us to cope with average.

Abstract:

In Description Logics (DL) knowledge bases (KBs), information is typically captured by clear-cut concepts. For many practical applications querying the KB by crisp concepts is too restrictive; a user might be willing to lose some precision in the query, in exchange of a larger selection of answers. Similarity measures can offer a controlled way of gradually relaxing a query concept within a user-specified limit. In this paper we formalize the task of instance query answering for DL KBs using concepts relaxed by concept similarity measures (CSMs). We investigate computation algorithms for this task in the DL EL, their complexity and properties for the CSMs employed regarding whether unfoldable or general TBoxes are used. For the case of general TBoxes we define a family of CSMs that take the full TBox information into account, when assessing the similarity of concepts.

Abstract:

Recently an approach has been devised how to employ concept similarity measures (CSMs) for relaxing instance queries over EL ontologies in a controlled way. The approach relies on similarity measures between pointed interpretations to yield CSMs with certain properties. We report in this paper on ELASTIQ, which is a first implementation of this approach and propose initial optimizations for this novel inference. We also provide a first evaluation of ELASTIQ on the Gene Ontology.

Zoltán Fülöp and Heiko Vogler: Characterizations of recognizable weighted tree languages by logic and bimorphisms. Soft Computing1–12, 2015.
BibTeX entry DOI

Abstract:

We give a general definition of weighted tree automata (wta) and define three instances which differ in the underlying weight algebras: semirings, multi-operator monoids, and tree-valuation monoids. Also, we define a general concept of weighted expressions based on monadic second-order logics. In the same way as for wta, we define three instances corresponding to the above-mentioned weight algebras. We prove that wta over semirings are equivalent to weighted expressions over semirings, and prove the same equivalence over tree-valuation monoids. For wta over semirings and for wta over tree-valuation monoids we prove characterizations in terms of bimorphisms.

Zoltán Fülöp and Heiko Vogler: Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics.. Theoretical Computer Science, 594:82–105, 2015.
BibTeX entry DOI

Abstract:

We introduce the branching transitive closure operator on progressing weighted monadic second-order logic formulas where the branching corresponds in a natural way to the branching inherent in trees. For arbitrary commutative semirings, we prove that weighted monadic second order logics on trees is equivalent to the definability by formulas which start with one of the following operators: (i) a branching transitive closure or (ii) one existential second-order quantifier followed by one universal first-order quantifier; in both cases the operator is applied to step-formulas over (a) Boolean first-order logic enriched by modulo counting or (b) Boolean monadic-second order logic.

Abstract:

The tree languages of tree-adjoining grammars are precisely those of linear monadic context-free tree grammars. Unlike the original proof, we present a direct transformation of a tree-adjoining grammar into an equivalent linear monadic context-free tree grammar.

Abstract:

We introduce an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we use a graded membership function which, for each individual and concept, yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts then collect all the individuals that belong to an EL concept C with degree less, less or equal, greater, respectively greater or equal r, for some r in [0,1] . We generalize a well-known characterization of membership in EL concepts to obtain an appropriate graded membership function deg, and investigate the complexity of reasoning in the Description Logic which extends EL by threshold concepts defined using deg.

Abstract:

We enrich the concept of automata with storage by weights taken from any unital valuation monoid. We prove a Schomsky-Schützenberger theorem for the class of weighted languages recognizable by such weighted automata with storage.

V. Perevoshchikov: Weight assignment logic. In 19th International Conference on Developments in Language Theory (DLT 2015), volume 9168 of LNCS, pages 413–425. Springer, 2015.
BibTeX entry

Markus Teichmann and Johannes Osterholzer: A link between multioperator and tree valuation automata and logics. Theoretical Computer Science, 594:106–119, 2015.
BibTeX entry DOI

Abstract:

Weighted tree languages over semirings lack the expressive power to model computations like taking the average or the discounting of weights in a straightforward manner. This limitation was overcome by weighted tree automata and logics using (a) tree valuation monoids and (b) multioperator monoids. We compare the expressive power of these two solutions and show that a weighted tree language recognizable (resp. definable) over a tree valuation monoid is also recognizable (resp. definable) using a multioperator monoid. For this, we provide direct, semantic-preserving transformations between the automata models and between the respective logics.

2014

Franz Baader and Marcel Lippmann: Runtime Verification Using the Temporal Description Logic ALC-LTL Revisited. Journal of Applied Logic, 12(4):584–613, 2014.
BibTeX entry DOI

Abstract:

Formulae of linear temporal logic (LTL) can be used to specify (wanted or unwanted) properties of a dynamical system. In model checking, the system's behaviour is described by a transition system, and one needs to check whether all possible traces of this transition system satisfy the formula. In runtime verification, one observes the actual system behaviour, which at any point in time yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix to a trace satisfy (violate) the formula. More precisely, one wants to construct a monitor, i.e., a finite automaton that receives the finite prefix as input and then gives the right answer based on the state currently reached. In this paper, we extend the known approaches to LTL runtime verification in two directions. First, instead of propositional LTL we use the more expressive temporal logic ALC-LTL, which can use axioms of the Description Logic (DL) ALC instead of propositional variables to describe properties of single states of the system. Second, instead of assuming that the observed system behaviour provides us with complete information about the states of the system, we assume that states are described in an incomplete way by ALC-knowledge bases. We show that also in this setting monitors can effectively be constructed. The (double-exponential) size of the constructed monitors is in fact optimal, and not higher than in the propositional case. As an auxiliary result, we show how to construct BÃ¼chi automata for ALC-LTL-formulae, which yields alternative proofs for the known upper bounds of deciding satisfiability in ALC-LTL.

Abstract:

Probabilistic model checking is a well-established method for the automated quantitative system analysis. It has been used in various application areas such as coordination algorithms for distributed systems, communication and multimedia protocols, biological systems, resilient systems or security. In this paper, we report on the experiences we made in inter-disciplinary research projects where we contribute with formal methods for the analysis of hardware and software systems. Many performance measures that have been identified as highly relevant by the respective domain experts refer to multiple objectives and require a good balance between two or more cost or reward functions, such as energy and utility. The formalization of these performance measures requires several concepts like quantiles, conditional probabilities and expectations and ratios of cost or reward functions that are not supported by state-of-the-art probabilistic model checkers. We report on our current work in this direction, including applications in the field of software product line verification.

Abstract:

Energy-utility analysis using probabilistic model checking Probabilistic model checking is a well-established technique for the automated quantitative system analysis that has been applied successfully in various application areas, such as coordination algorithms for distributed systems, communication and multimedia protocols, biological systems, resilient systems or security. The talk reports on the experiences made in inter-disciplinary research projects where probabilistic model checking is applied for the analysis of the trade-off between several cost and reward values, such as energy and utility. The formalization of the relevant performance measures requires several concepts like quantiles, conditional probabilities and expectations and ratios of cost or reward functions that are not supported by state-of-the-art probabilistic model checkers. The talk will provide an overview of the challenges that we had to address and reports on our current work in this direction.

Abstract:

Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the model-checking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA.

Abstract:

In the last few years, there has been a large effort for analyzing the computational properties of reasoning in fuzzy description logics. This has led to a number of papers studying the complexity of these logics, depending on the chosen semantics. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy description logics w.r.t. witnessed models over the Gödel t-norm. We show that in the logic G-IALC, reasoning cannot be restricted to finitely-valued models in general. Despite this negative result, we also show that all the standard reasoning problems can be solved in exponential time, matching the complexity of reasoning in classical ALC.

Stefan Borgwardt and Rafael Peñaloza: Consistency Reasoning in Lattice-Based Fuzzy Description Logics. International Journal of Approximate Reasoning, 2014.
BibTeX entry Paper (PDF) DOI

Abstract:

Fuzzy Description Logics have been widely studied as a formalism for representing and reasoning with vague knowledge. One of the most basic reasoning tasks in (fuzzy) Description Logics is to decide whether an ontology representing a knowledge domain is consistent. Surprisingly, not much is known about the complexity of this problem for semantics based on complete De Morgan lattices. To cover this gap, in this paper we study the consistency problem for the fuzzy Description Logic L-SHI and its sublogics in detail. The contribution of the paper is twofold. On the one hand, we provide a tableaux-based algorithm for deciding consistency when the underlying lattice is finite. The algorithm generalizes the one developed for classical SHI. On the other hand, we identify decidable and undecidable classes of fuzzy Description Logics over infinite lattices. For all the decidable classes, we also provide tight complexity bounds.

Abstract:

Weighted automata model quantitative aspects of systems like the consumption of resources during executions. Traditionally, the weights are assumed to form the algebraic structure of a semiring, but recently also other weight computations like average have been considered. Here, we investigate quantitative context-free languages over very general weight structures incorporating all semirings, average computations, lattices. In our main result, we derive the Chomsky-Schützenberger Theorem for such quantitative context-free languages, showing that each arises as the image of the intersection of a Dyck language and a recognizable language under a suitable morphism. Moreover, we show that quantitative context-free languages are expressively equivalent to a model of weighted pushdown automata. This generalizes results previously known only for semirings. We also investigate under which conditions quantitative context-free languages assume only finitely many values.

Abstract:

Description Logic (DL) knowledge bases (KBs) allow to express knowledge about concepts and individuals in a formal way. This knowledge is typically crisp, i.e., an individual either is an instance of a given concept or it is not. However, in practice this is often too restrictive: when querying for instances, one may often also want to find suitable alternatives, i.e., individuals that are not instances of query concept, but could still be considered `good enough'. Relaxed instance queries have been introduced to gradually relax this inference in a controlled way via the use of concept similarity measures (CSMs). So far, those algorithms only work for the DL EL, which has limited expressive power. In this paper, we introduce a suitable CSM for EL++-concepts. EL++ adds nominals, role inclusion axioms, and concrete domains to EL. We extend the algorithm to compute relaxed instance queries w.r.t. this new CSM, and thus to work for general EL++ KBs.

Abstract:

In Description Logics (DL) knowledge bases (KBs) information is typically captured by crisp concepts. For many applications querying the KB by crisp query concepts is too restrictive. A controlled way of gradually relaxing a query concept can be achieved by the use of concept similarity. In this paper we formalize the task of instance query answering for crisp DL KBs using concepts relaxed by concept similarity measures (CSM). For the DL EL we investigate computation algorithms for this task, their complexity and properties for the employed CSM in case unfoldabel Tboxes or general TBoxes aer used.

Abstract:

Description Logics (DLs) are a well-established family of knowledge representation formalisms. One of its members, the DL ELOR has been successfully used for representing knowledge from the bio-medical sciences, and is the basis for the OWL 2 EL profile of the standard ontology language for the Semantic Web. Reasoning in this DL can be performed in polynomial time through a completion-based algorithm. In this paper we study the logic Prob-ELOR, that extends ELOR with subjective probabilities, and present a completion-based algorithm for polynomial time reasoning in a restricted version, Prob-ELOR^c₀₁, of Prob-ELOR. We extend this algorithm to computation algorithms for approximations of (i) the most specific concept, which generalizes a given individual into a concept description, and (ii) the least common subsumer, which generalizes several concept descriptions into one. Thus, we also obtain methods for these inferences for the OWL 2 EL profile. These two generalization inferences are fundamental for building ontologies automatically from examples. The feasibility of our approach is demonstrated empirically by our prototype system GEL.

Abstract:

In the last 20 years many proposals have been made to incorporate non-monotonic reasoning into description logics, ranging from approaches based on default logic and circumscription to those based on preferential semantics. In particular, the non-monotonic description logic ALC+Tmin uses a combination of the preferential semantics with minimization of a certain kind of concepts, which represent atypical instances of a class of elements. One of its drawbacks is that it suffers from the problem known as the property blocking inheritance, which can be seen as a weakness from an inferential point of view. In this paper we propose an extension of ALC+Tmin, namely ALC+T+min, with the purpose to solve the mentioned problem. In addition, we show the close connection that exists between ALC+T+min and concept-circumscribed knowledge bases. Finally, we study the complexity of deciding the classical reasoning tasks in ALC+T+min.

Abstract:

In this paper, we consider weighted synchronous context-free tree grammars and identify a certain syntactic restriction of these grammars. We suggest a new weighted tree transducer formalism and prove that the transformations of the restricted grammars are precisely those of the linear and nondeleting instances of these transducers.

2013

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporalizing Ontology-Based Data Access. In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), Lecture Notes in Artificial Intelligence. Lake Placid, NY, USA, Springer-Verlag, 2013.
BibTeX entry Paper (PDF) Extended technical report (PDF) (The final publication is available at link.springer.com)

Abstract:

Ontology-based data access (OBDA) generalizes query answering in databases towards deduction since (i) the fact base is not assumed to contain complete knowledge (i.e., there is no closed world assumption), and (ii) the interpretation of the predicates occurring in the queries is constrained by axioms of an ontology. OBDA has been investigated in detail for the case where the ontology is expressed by an appropriate Description Logic (DL) and the queries are conjunctive queries. Motivated by situation awareness applications, we investigate an extension of OBDA to the temporal case. As query language we consider an extension of the well-known propositional temporal logic LTL where conjunctive queries can occur in place of propositional variables, and as ontology language we use the prototypical expressive DL ALC. For the resulting instance of temporalized OBDA, we investigate both data complexity and combined complexity of the query entailment problem.

Abstract:

To extract terminological knowledge from data, Baader and Distel have proposed an effective method that allows for the extraction of a base of all valid general concept inclusions of a given finite interpretation. In previous works, to be able to handle small amounts of errors in our data, we have extended this approach to also extract general concept inclusions which are ``almost valid'' in the interpretation. This has been done by demanding that general concept inclusions which are ``almost valid'' are those having only an allowed percentage of counterexamples in the interpretation. In this work, we shall further extend our previous work to allow the interpretation to contain both trusted and untrusted individuals, i.e. individuals from which we know and do not know that they are correct, respectively. The problem we then want to solve is to find a compact representation of all terminological knowledge that is valid for all trusted individuals and is almost valid for all others.

Abstract:

In a recent approach, Baader and Distel proposed an algorithm to axiomatize all terminological knowledge that is valid in a given data set and is expressible in the description logic EL. This approach is based on the mathematical theory of formal concept analysis. However, this algorithm requires the initial data set to be free of errors, an assumption that normally cannot be made for real-world data. In this work, we propose a first extension of the work of Baader and Distel to handle errors in the data set. The approach we present here is based on the notion of confidence, as it has been developed and used in the area of data mining.

Abstract:

In the work of Baader and Distel, a method has been proposed to axiomatize all general concept inclusions (GCIs) expressible in the description logic EL and valid in a given interpretation I. This provides us with an effective method to learn $EL-ontologies from interpretations. In this work, we want to extend this approach in the direction of handling errors, which might be present in the data-set. We shall do so by not only considering valid GCIs but also those whose confidence is above a given threshold c. We shall give the necessary definitions and show some first results on the axiomatization of all GCIs with confidence at least c. Finally, we shall provide some experimental evidence based on real-world data that supports our approach.

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporal Query Answering in the Description Logic DL-Lite. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), volume 8152 of Lecture Notes in Computer Science, pages 165–180. Nancy, France, Springer-Verlag, 2013.
BibTeX entry Paper (PDF) Extended technical report (PDF) (The final publication is available at link.springer.com)

Abstract:

Ontology-based data access (OBDA) generalizes query answering in relational databases. It allows to query a database by using the language of an ontology, abstracting from the actual relations of the database. For ontologies formulated in Description Logics of the DL-Lite family, OBDA can be realized by rewriting the query into a classical first-order query, e.g. an SQL query, by compiling the information of the ontology into the query. The query is then answered using classical database techniques. In this paper, we consider a temporal version of OBDA. We propose a temporal query language that combines a linear temporal logic with queries over DL-Lite_core-ontologies. This language is well-suited to express temporal properties of dynamical systems and is useful in context-aware applications that need to detect specific situations. Using a first-order rewriting approach, we transform our temporal queries into queries over a temporal database. We then present three approaches to answering the resulting queries, all having different advantages and drawbacks.

Abstract:

The Description Logic EL is used to formulate several large biomedical ontologies. Fuzzy extensions of EL can express the vagueness inherent in many biomedical concepts. We consider fuzzy EL with semantics based on general t-norms, and study the reasoning problems of deciding positive subsumption and 1-subsumption and computing the best subsumption degree.

Abstract:

The Description Logic EL is used to formulate several large biomedical ontologies. Fuzzy extensions of EL can express the vagueness inherent in many biomedical concepts. We study the reasoning problem of deciding positive subsumption in fuzzy EL with semantics based on general t-norms. We show that the complexity of this problem depends on the specific t-norm chosen. More precisely, if the t-norm has zero divisors, then the problem is co-NP-hard; otherwise, it can be decided in polynomial time. We also show that the best subsumption degree cannot be computed in polynomial time if the t-norm contains the Łukasiewicz t-norm.

Abstract:

Weighted automata model quantitative aspects of systems like the consumption of resources during executions. Traditionally, the weights are assumed to form the algebraic structure of a semiring, but recently also other weight computations like average have been considered. Here, we investigate quantitative context-free languages over very general weight structures incorporating all semirings, average computations, lattices, and more. In our main result, we derive the fundamental Chomsky-Schützenberger theorem for such quantitative context-free languages, showing that each arises as the image of a Dyck language and a regular language under a suitable morphism. Moreover, we show that quantitative context-free language are expressively equivalent to a model of weighted pushdown automata. This generalizes results previously known only for semirings. We also investigate when quantitative context-free languages assume only finitely many values.

Abstract:

Description Logics (DLs) are a family of knowledge representation formalisms, that provides the theoretical basis for the standard web ontology language OWL. Generalization services like the least common subsumer (lcs) and the most specific concept (msc) are the basis of several ontology design methods, and form the core of similarity measures. For the DL ELOR, which covers most of the OWL 2 EL profile, the lcs and msc need not exist in general, but they always exist if restricted to a given role-depth. We present algorithms that compute these role-depth bounded generalizations. Our method is easy to implement, as it is based on the polynomial-time completion algorithm for ELOR.

Abstract:

Completion-based algorithms can be employed for computing the least common subsumer of two concepts up to a given role-depth, in extensions of the lightweight DL EL. This approach has been applied also to the probabilistic DL Prob-EL, which is variant of EL with subjective probabilities. In this paper we extend the completion-based lcs-computation algorithm to nominals, yielding a procedure for the DL Prob-ELO⁰¹.

Abstract:

In Description Logics (DL) knowledge bases (KBs) information is typically captured by crisp concept descriptions. However, for many practical applications querying the KB by crisp concepts is too restrictive. A controlled way of gradually relaxing a query concept can be achieved by the use of similarity measures. To this end we formalize the task of instance query answering for crisp DL KBs using concepts relaxed by similarity measures. We identify relevant properties for the similarity measure and give first results on a computation algorithm.

Uwe Ryssel, Felix Distel, and Daniel Borchmann: Fast algorithms for implication bases and attribute exploration using proper premises. Annals of Mathematics and Artificial Intelligence, Special Issue 65:1–29, 2013.
BibTeX entry Paper (PDF) (The final publication is available at link.springer.com)

Abstract:

A central task in formal concept analysis is the enumeration of a small base for the implications that hold in a formal context. The usual stem base algorithms have been proven to be costly in terms of runtime. Proper premises are an alternative to the stem base. We present a new algorithm for the fast computation of proper premises. It is based on a known link between proper premises and minimal hypergraph transversals. Two further improvements are made, which reduce the number of proper premises that are obtained multiple times and redundancies within the set of proper premises. We have evaluated our algorithms within an application related to refactoring of model variants. In this application an implicational base needs to be computed, and runtime is more crucial than minimal cardinality. In addition to the empirical tests, we provide heuristic evidence that an approach based on proper premises will also be beneficial for other applications. Finally, we show how our algorithms can be extended to an exploration algorithm that is based on proper premises.

2012

Details: Last Updated: February 17 2020