EN | DE
Theoretische Informatik
@string{hp_SergeyGoncharov="http://www8.informatik.uni-erlangen.de/~sergey/"}
@string{hp_LutzSchröder="http://www8.informatik.uni-erlangen.de/schroeder/"}
@string{hp_StefanMilius="http://www8.informatik.uni-erlangen.de/~milius/"}
@string{hp_TadeuszLitak="http://www8.informatik.uni-erlangen.de/~litak/"}
@string{hp_DanielGorín="http://www8.informatik.uni-erlangen.de/~gorin/"}

%
% 2014
%


@inproceedings{DBLP:conf/fossacs/DahlqvistP13,
  author    = {Fredrik Dahlqvist and
               Dirk Pattinson},
  title     = {Some Sahlqvist Completeness Results for Coalgebraic Logics},
  booktitle = {FoSSaCS},
  pages     = {193-208},
  editor    = {Frank Pfenning},
  booktitle     = {Foundations of Software Science and Computation Structures
               - 16th International Conference, FOSSACS 2013,
               Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7794},
  year      = {2013},
  isbn      = {978-3-642-37074-8},
  ee        = {http://dx.doi.org/10.1007/978-3-642-37075-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/corr/abs-1105-2246,
  author    = {Corina C\^{\i}rstea and
               Clemens Kupke and
               Dirk Pattinson},
  title     = {EXPTIME Tableaux for the Coalgebraic mu-Calculus},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  nonumber    = {3},
  year      = {2011},
  ee        = {http://dx.doi.org/10.2168/LMCS-7(3:3)2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/tcs/KupkeP11,
  author    = {Clemens Kupke and
               Dirk Pattinson},
  title     = {Coalgebraic semantics of modal logics: An overview},
  journal   = {Theor. Comput. Sci.},
  volume    = {412},
  nonumber    = {38},
  year      = {2011},
  pages     = {5070-5094},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2011.04.023},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/calco/DahlqvistP11,
  author    = {Fredrik Dahlqvist and
               Dirk Pattinson},
  title     = {On the Fusion of Coalgebraic Logics},
  booktitle = {CALCO},
  editor    = {Andrea Corradini and
               Bartek Klin and
               Corina C\^{\i}rstea},
  booktitle     = {Algebra and Coalgebra in Computer Science - 4th International
               Conference, CALCO 2011, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6859},
  year      = {2011},
  isbn      = {978-3-642-22943-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22944-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/tbillc/LitakPS11,
  author    = {Tadeusz Litak and
               Dirk Pattinson and
               Katsuhiko Sano},
  title     = {Coalgebraic Predicate Logic: Equipollence Results and Proof
               Theory},
  booktitle = {TbiLLC},
  editor    = {Guram Bezhanishvili and
               Sebastian L{\"o}bner and
               Vincenzo Marra and
               Frank Richter},
  booktitle     = {Logic, Language, and Computation - 9th International Tbilisi
               Symposium on Logic, Language, and Computation, TbiLLC 2011, Revised Selected
               Papers},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7758},
  year      = {2013},
  isbn      = {978-3-642-36975-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-36976-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/tacas/GoreKP10,
  author    = {Rajeev Gor{\'e} and
               Clemens Kupke and
               Dirk Pattinson},
  title     = {Optimal Tableau Algorithms for Coalgebraic Logics},
  booktitle = {TACAS},
  editor    = {Javier Esparza and
               Rupak Majumdar},
  booktitle     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 16th International Conference, TACAS 2010, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6015},
  year      = {2010},
  isbn      = {978-3-642-12001-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-12002-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/mscs/KurzP05,
  author    = {Alexander Kurz and
               Dirk Pattinson},
  title     = {Coalgebraic modal logic of finite rank},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {15},
  number    = {3},
  year      = {2005},
  pages     = {453-473},
  ee        = {http://dx.doi.org/10.1017/S0960129505004755},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{KupkeEA04,
  author    = {Clemens Kupke and
               Alexander Kurz and
               Dirk Pattinson},
  title     = {Algebraic Semantics for Coalgebraic Logics},
  booktitle = {Coalgebraic Methods in Computer Science, CMCS 2004},
  series   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {106},
  year      = {2004},
  pages     = {219-241},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2004.02.037},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/tcs/Pattinson03,
  author    = {Dirk Pattinson},
  title     = {Coalgebraic modal logic: soundness, completeness and decidability
               of local consequence},
  journal   = {Theor. Comput. Sci.},
  volume    = {309},
  nonumber    = {1-3},
  year      = {2003},
  pages     = {177-193},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(03)00201-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/corr/abs-1206-4935,
  author    = {Clemens Kupke and
               Alexander Kurz and
               Yde Venema},
  title     = {Completeness for the coalgebraic cover modality},
  journal   = {Logical Methods in Computer Science},
  volume    = {8},
  nonumber    = {3},
  year      = {2012},
  ee        = {http://dx.doi.org/10.2168/LMCS-8(3:2)2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/calco/BergfeldV11,
  author    = {Jort Bergfeld and
               Yde Venema},
  title     = {Model Constructions for Moss' Coalgebraic Logic},
  booktitle = {CALCO},
  editor    = {Andrea Corradini and
               Bartek Klin and
               Corina C\^{\i}rstea},
  booktitle     = {Algebra and Coalgebra in Computer Science - 4th International
               Conference, CALCO 2011, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6859},
  year      = {2011},
  isbn      = {978-3-642-22943-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22944-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/logcom/KurzPV10,
  author    = {Alexander Kurz and
               Alessandra Palmigiano and
               Yde Venema},
  title     = {Coalgebra and Logic: A Brief Overview},
  journal   = {J. Log. Comput.},
  volume    = {20},
  nonumber    = {5},
  year      = {2010},
  pages     = {985-990},
  ee        = {http://dx.doi.org/10.1093/logcom/exn094},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/aiml/KurzV10,
  author    = {Alexander Kurz and
               Yde Venema},
  title     = {Coalgebraic Lindstr{\"o}om Theorems},
  booktitle = {Advances in Modal Logic},
  editor    = {Lev D. Beklemishev and
               Valentin Goranko and
               Valentin Shehtman},
  booktitle     = {Advances in Modal Logic, AiML 2010},
  booktitle = {Advances in Modal Logic},
  publisher = {College Publications},
  year      = {2010},
  isbn      = {978-1-84890-013-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/ndjfl/Pattinson04,
  author    = {Dirk Pattinson},
  title     = {Expressive Logics for Coalgebras via Terminal Sequence Induction},
  journal   = {Notre Dame Journal of Formal Logic},
  volume    = {45},
  nonumber    = {1},
  year      = {2004},
  pages     = {19-33},
  ee        = {http://projecteuclid.org/euclid.ndjfl/1094155277},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icalp/FontaineLV10,
  author    = {Ga{\"e}lle Fontaine and
               Raul Andres Leal and
               Yde Venema},
  title     = {Automata for Coalgebras: An Approach Using Predicate Liftings},
  booktitle = {ICALP (2)},
  editor    = {Samson Abramsky and
               Cyril Gavoille and
               Claude Kirchner and
               Friedhelm {Meyer auf der Heide} and
               Paul G. Spirakis},
  booktitle     = {Automata, Languages and Programming, 37th International
               Colloquium, ICALP 2010, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6199},
  year      = {2010},
  isbn      = {978-3-642-14161-4},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14162-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/calco/KissigV09,
  author    = {Christian Kissig and
               Yde Venema},
  title     = {Complementation of Coalgebra Automata},
  booktitle = {CALCO},
  editor    = {Alexander Kurz and
               Marina Lenisa and
               Andrzej Tarlecki},
  title     = {Algebra and Coalgebra in Computer Science, Third International
               Conference, CALCO 2009, 
               Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5728},
  year      = {2009},
  isbn      = {978-3-642-03740-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03741-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/lmcs/KupkeV08,
  author    = {Clemens Kupke and
               Yde Venema},
  title     = {Coalgebraic Automata Theory: Basic Results},
  journal   = {Logical Methods in Computer Science},
  volume    = {4},
  nonumber    = {4},
  year      = {2008},
  ee        = {http://dx.doi.org/10.2168/LMCS-4(4:10)2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/corr/abs-1207-2732,
  author    = {Alexander Kurz and
               Jir\'{\i} Rosick{\'y}},
  title     = {Strongly Complete Logics for Coalgebras},
  journal   = {Logical Methods in Computer Science},
  volume    = {8},
  nonumber    = {3},
  year      = {2012},
  ee        = {http://dx.doi.org/10.2168/LMCS-8(3:14)2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/tcs/KurzL12,
  author    = {Alexander Kurz and
               Raul Andres Leal},
  title     = {Modalities in the Stone age: A comparison of coalgebraic
               logics},
  journal   = {Theor. Comput. Sci.},
  volume    = {430},
  year      = {2012},
  pages     = {88-116},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2012.03.027},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/aiml/KapulkinKV12,
  author    = {Krzysztof Kapulkin and
               Alexander Kurz and
               Jiri Velebil},
  title     = {Expressiveness of Positive Coalgebraic Logic},
  booktitle = {Advances in Modal Logic},
  editor    = {Thomas Bolander and
               Torben Bra{\"u}ner and
               Silvio Ghilardi and
               Lawrence S. Moss},
  booktitle     = {Advances in Modal Logic, AiML 2012},
  publisher = {College Publications},
  year      = {2012},
  isbn      = {978-1-84890-068-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/sigact/Kurz06,
  author    = {Alexander Kurz},
  title     = {Coalgebras and their logics},
  journal   = {SIGACT News},
  volume    = {37},
  nonumber    = {2},
  year      = {2006},
  pages     = {57-77},
  ee        = {http://doi.acm.org/10.1145/1140612.1140628},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:journals/entcs/Klin07,
  author    = {Bartek Klin},
  title     = {Coalgebraic Modal Logic Beyond Sets},
  booktitle = {623rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII), Proceedings},
  series   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {173},
  year      = {2007},
  pages     = {177-201},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2007.02.034},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/lics/Klin07,
  author    = {Bartek Klin},
  title     = {Bialgebraic Operational Semantics and Modal Logic},
  booktitle = {LICS},
  booktitle     = {22nd IEEE Symposium on Logic in Computer Science, LICS 2007, Proceedings},
  publisher = {IEEE Computer Society},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/logcom/JacobsS10,
  author    = {Bart Jacobs and
               Ana Sokolova},
  title     = {Exemplaric Expressivity of Modal Logics},
  journal   = {J. Log. Comput.},
  volume    = {20},
  nonumber    = {5},
  year      = {2010},
  pages     = {1041-1068},
  ee        = {http://dx.doi.org/10.1093/logcom/exn093},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{GorinSchroder13,
 author = {Daniel Gor{\'i}n and Lutz Schr{\"o}der},
  title = {Simulations and Bisimulations For Coalgebraic Modal Logics},
  booktitle = {Proc. 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013},
  editor = {Reiko Heckel and Stefan Milius},
  series = {Lect. Notes Comput. Sci.},
  publisher = {Springer},
  volume    = {8089},
  doi        = {10.1007/978-3-642-40206-7_19},
  year = {2013},
  pages     = {253-266},
  url = {http://arxiv.org/pdf/1303.2467},
}

@InProceedings{CarreiroEA13,
  author = {Facundo Carreiro and Daniel Gor{\'i}n and Lutz Schr{\"o}der},
  title = {Coalgebraic Announcement Logics},
  booktitle = {Proc. 40th International Colloquium on Automata, Languages and Programming, ICALP 2013},
  series = {Lect. Notes Comput. Sci.},
  publisher = {Springer},
  pages     = {101-112},
  editor    = {Fedor V. Fomin and
               Rusins Freivalds and
               Marta Z. Kwiatkowska and
               David Peleg},
  volume    = {7966},
  year = {2013},
  url = {http://www8.cs.fau.de/_media/research:papers:icalp13.pdf},
  doi = {10.1007/978-3-642-39212-2_12},
}


@InProceedings{KulackaEA13,
  author = 	 {Agnieszka Kulacka and Dirk Pattinson and Lutz Schr{\"o}der},
  title = 	 {Syntactic Labelled Tableaux for Lukasiewicz Fuzzy {ALC}},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proc. 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013},
  OPTpages = 	 {},
  year =	 {2013},
  editor =	 {Francesca Rossi},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {IJCAI/AAAI},
  OPTannote = 	 {},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/_media/research:papers:lukasiewicz-tableau.pdf"> [updated version]</a>},       
  url =          {http://ijcai.org/papers13/Papers/IJCAI13-147.pdf},
}


@inproceedings{GorinSchroder12,
  author    = {Daniel Gor\'{\i}n and
               Lutz Schr{\"o}der},
  title     = {Narcissists Are Easy, Stepmothers Are Hard},
  pages     = {240-254},
  ee        = {http://dx.doi.org/10.1007/978-3-642-28729-9_16},
  doi        = {10.1007/978-3-642-28729-9_16},
  editor    = {Lars Birkedal},
  booktitle     = {Proc. 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2012},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7213},
  year      = {2012},
  isbn      = {978-3-642-28728-2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  url = {http://www8.cs.fau.de/_media/research:papers:fossacs12.pdf},
}


@InProceedings{GorinSchroder14,
  author = 	 {Daniel Gor{\'\i}n and Lutz Schr{\"o}der},
  title = 	 {Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics},
  booktitle =	 {Proc. Advances in Modal Logic, AiML 2014},
  year =	 {2014},
  editor =	 {Agi Kurucz and Rajeev Gor{\'e}},
  series =	 {LNCS},
  publisher =	 {Springer},
  note =	 {To appear},
}

@Article{CirsteaEA09,
  author = {Corina Cirstea and Alexander Kurz and  Dirk Pattinson and Lutz Schr{\"o}der and Yde Venema},
  title = {Modal logics are coalgebraic},
  year = {2011},
  journal = {The Computer Journal},
  volume = {54},
  pages = {31-41},
  number = {1},
  keywords = {Modal logic coalgebra knowledge representation automata modularity pi-calculus},
  doi = {"> [preprint] </a>http://comjnl.oxfordjournals.org/cgi/content/abstract/bxp004},
  url = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/ModalCoalgRev.pdf},
  abstract = {Applications of modal logics are abundant in computer science, and
a large number of structurally different modal logics have been successfully 
employed in a diverse spectrum of application contexts. 
Coalgebraic semantics, on the other hand,  provides  a uniform
and encompassing view on the large variety of specific logics used
in particular domains.  The coalgebraic
approach is generic and compositional: tools and
techniques simultaneously apply to a large class of application
areas and can moreover be combined in a modular way.
In particular, this facilitates a pick-and-choose approach to domain
specific formalisms, applicable across the entire scope of
application areas, leading to generic software tools that are easier
to design, to implement, and to maintain.
This paper substantiates the authors' firm belief that the systematic
exploitation of the coalgebraic nature of modal logic will not only
have impact on the field of modal logic itself but also lead to
significant progress in a number of areas within computer science,
such as knowledge representation and concurrency/mobility.
}}


@InProceedings{GoreEA10,
  author = {Rajeev Gore and Clemens Kupke and Dirk Pattinson and Lutz Schr{\"o}der},
  title = {Global Caching for Coalgebraic Description Logics},
  year = {2010},
  editor = {J{\"u}rgen Giesl and Reiner Haehnle},
  booktitle = {International Joint Conference on Automated Reasoning, IJCAR 2010},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6173},
  pages = {46-60},
  keywords = {Coalgebra description logic modal logic hybrid logic tableaux global caching},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/hyGlobalCaching.pdf"> [preprint] </a>},
  abstract = {  Coalgebraic description logics offer a common semantic umbrella for
  extensions of description logics with reasoning principles outside
  relational semantics, e.g. quantitative uncertainty, non-monotonic
  conditionals, or coalitional power. Specifically, we work in
  coalgebraic logic with global assumptions (i.e. a general TBox),
  nominals, and satisfaction operators, and prove soundness and
  completeness of an associated tableau algorithm of optimal
  complexity ExpTime. The algorithm uses the (known) tableau rules for
	the underlying modal logics, and is based on  on global caching, which
  raises hopes of practically feasible implementation. Instantiation
  of this result to concrete logics yields new algorithms in all cases
  including standard relational hybrid logic.},
}



@InProceedings{MyersEA09,
  author = {Rob Myers and Dirk Pattinson and Lutz Schr{\"o}der},
  title = {Coalgebraic Hybrid Logic},
  year = {2009},
  editor = {Luca de Alfaro},
  booktitle = {Foundations of Software Science and Computation Structures (FOSSACS 2009)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5504},
  pages = {137-151},
  keywords = {coalgebra hybrid logic decision procedures polynomial space hilbert gentzen sequent tableaux},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/chl.pdf"> [preprint] </a>},
  abstract = { We introduce a generic framework for hybrid logics, i.e. modal
logics additionally featuring nominals and satisfaction operators, thus providing the necessary facilities for reasoning about individual states in a model. This framework, coalgebraic hybrid logic, works at the same level of generality as coalgebraic modal logic, and in particular subsumes, besides normal hybrid logics such as hybrid K, a wide variety of logics with non-normal modal operators such as probabilistic, graded, or coalitional modalities and non-monotonic conditionals. We prove a generic finite model property and an ensuing weak completeness result, and we give  a semantic criterion for decidability in PSPACE. Moreover, we present a fully internalised PSPACE tableau calculus. These generic results are easily instantiated to particular hybrid logics and thus yield a wide range of new results, including e.g. decidability in PSPACE of probabilistic and graded hybrid logics.},
}

@InProceedings{PattinsonSchroder08,
  author = {Dirk Pattinson and Lutz Schr{\"o}der},
  title = {Beyond Rank 1: Algebraic Semantics and Finite Models for Coalgebraic Logics},
  year = {2008},
  editor = {Roberto Amadio},
  booktitle = {Foundations of Software Science and Computation Structures (FOSSACS 2008)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4962},
  pages = {66-80},
  keywords = {Coalgebra modal logic frame conditions algebraic semantics quantitative uncertainty coalition logic},
  url = {http://dx.doi.org/10.1007/978-3-540-78499-9_6},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/fmp-fap.pdf"> [preprint] </a>},
  abstract = {  Coalgebras provide a uniform framework for the semantics of a large
  class of (mostly non-normal) modal logics, including e.g. monotone
  modal logic, probabilistic and graded modal logic, and coalition
  logic, as well as the usual Kripke semantics of modal logic.  In
  earlier work, the finite model property for coalgebraic logics has
  been established w.r.t. the class of emph{all} structures
  appropriate for a given logic at hand; the corresponding modal
  logics are characterised by being axiomatised in rank 1, i.e.
  without nested modalities. Here, we extend the range of coalgebraic
  techniques to cover logics that impose global properties on their
  models, formulated as frame conditions with possibly nested
  modalities on the logical side (in generalisation of frame
  conditions such as symmetry or transitivity in the context of Kripke
  frames).
  We show that the finite model property for such logics follows from
  the finite algebra property of the associated class of complex
  algebras, and then investigate sufficient conditions for the finite
  algebra property to hold.  Example applications include extensions
  of coalition logic and logics of uncertainty and knowledge.
},
}

@Article{PattinsonSchroder10,
  author = {Dirk Pattinson and Lutz Schr{\"o}der},
  title = {Cut Elimination in Coalgebraic Logics},
  year = {2010},
  journal = {Information and Computation},
  volume = {208},
  pages = {1447-1468},
  keywords = {Coalgebra modal logic cut elimination interpolation coalition logic conditiona logic},
  url = {http://dx.doi.org/10.1016/j.ic.2009.11.008},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/cut-ext.pdf"> [preprint] </a>},
  abstract = {We give two generic proofs for cut elimination in
  propositional modal logics, interpreted over coalgebras. We first
  investigate semantic coherence conditions between the axiomatisation
  of a particular logic and its coalgebraic semantics that guarantee
  that the cut-rule is admissible in the ensuing sequent calculus. We
  then independently isolate a purely syntactic property of the set of
  modal rules that guarantees cut elimination.  Apart from the fact
  that cut elimination holds, our main result is that the syntactic
  and semantic assumptions are equivalent in case the logic is
  amenable to coalgebraic semantics.  As applications we present a new
  proof of the (already known) interpolation property for coalition
  logic and newly establish the interpolation property for the conditional
  logics CK and CK+ID.},
}

@Article{Schroder06Expr-TCS,
  author = {Lutz Schr{\"o}der},
  title = {Expressivity of Coalgebraic Modal Logic: The Limits and Beyond},
  year = {2008},
  journal = {Theoretical Computer Science},
  volume = {390},
  pages = {230-247},
  keywords = {coalgebra expressivity modal logic predicate lifting natural relation},
  url = {http://dx.doi.org/10.1016/j.tcs.2007.09.023},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/coalgml-ext.pdf"> [preprint] </a>},
  abstract = {Modal logic has a good claim to being the logic of choice for describing
the reactive behaviour of systems modeled as coalgebras. Logics with
modal operators obtained from so-called predicate liftings have been
shown to be invariant under behavioral equivalence. Expressivity results
stating that, conversely, logically indistinguishable states are
behaviorally equivalent depend on the existence of separating sets of
predicate liftings for the signature functor at hand. Here, we provide a
classification result for predicate liftings which leads to an easy
criterion for the existence of such separating sets, and we give simple
examples of functors that fail to admit expressive normal or monotone
modal logics, respectively, or in fact an expressive (unary) modal logic
at all. We then move on to polyadic modal logic, where modal operators
may take more than one argument formula. We show that every accessible
functor admits an expressive polyadic modal logic. Moreover, expressive
polyadic modal logics are, unlike unary modal logics, compositional.
}}

@Article{Schroder07,
  author = {Lutz Schr{\"o}der},
  title = {A finite model construction for coalgebraic modal logic},
  year = {2007},
  journal = {Journal of Logic and Algebraic Programming (FOSSACS 06 special issue)},
  volume = {73},
  pages = {97-110},
  keywords = {Coalgebra Modal Logic Decision Procedures Complexity Filtrations},
  url = {http://dx.doi.org/10.1016/j.jlap.2006.11.004},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/CMLfmp-ext.pdf"> [preprint] </a>},
  abstract = {In recent years, a tight connection has emerged between modal logic on
the one hand and coalgebras, understood as generic transition systems,
on the other hand. Here, we prove that (finitary) coalgebraic modal
logic has the finite model property. This fact not only reproves known
completeness results for coalgebraic modal logic, which we push further
by establishing that every coalgebraic modal logic admits a complete
axiomatisation in rank 1; it also enables us to establish a generic
decidability result and a first complexity bound. Examples covered by
these general results include, besides standard Hennessy-Milner logic,
graded modal logic and probabilistic modal logic.
}
}

@InProceedings{SchroderEA09,
  author = {Lutz Schr{\"o}der and Dirk Pattinson and Clemens Kupke},
  title = {Nominals for Everyone},
  year = {2009},
  editor = {Craig Boutilier},
  booktitle = {International Joint Conferences on Artificial Intelligence (IJCAI 2009)},
  publisher = {AAAI Press; Menlo Park, CA},
  pages = {917-922},
  keywords = {Description logic coalgebra hybrid logic modal logic nominals uncertainty Tudor dynasty},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/Nominals.pdf"> [preprint] </a>},
  abstract = {  It has been recognised that the expressivity of ontology languages
  benefits from the introduction of non-standard modal operators
  beyond the usual existential restrictions and the number
  restrictions already featured by many description logics. Such
  operators serve to support notions such as uncertainty, defaults,
  agency, obligation, or evidence, which are hard to capture using
  only the standard operators, and whose semantics often goes beyond
  relational structures. We work in a unified theory for logics that
  combine non-standard modal operators and nominals, a feature of
  established description logics that provides the necessary means for
  reasoning about individuals; in particular, the logics of this
  framework allow for internalisation of ABoxes. We reenforce the
  general framework by proving decidability in EXPTIME of concept
  satisfiability over general TBoxes; moreover, we discuss example
  instantiations in various probabilistic logics with nominals.
},
}



@Article{SchroderPattinson08,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {PSPACE Bounds for Rank-1 Modal Logics},
  year = {2009},
  journal = {ACM Transactions on Computational Logic},
  volume = {10},
  pages = {1-33},
  number = {2:13},
  keywords = {Modal logic coalgebra non-iterative majority probabilistic graded coalition PSPACE},
  url = {http://arxiv.org/abs/0706.4044},
  comment = { <a href = "http://tocl.acm.org/accepted/352schroeder.pdf"> [preprint] </a>},
  abstract = {For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics.  Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.},
}

@Article{SchroderPattinson08b,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Rank-1 modal logics are coalgebraic },
  year = {2010},
  journal = {Journal of Logic and Computation},
  volume = {20},
  pages = {1113-1147},
  number = {5},
  keywords = {Modal logic coalgebra neighbourhood frames deontic logic decision procedures},
  url = {http://logcom.oxfordjournals.org/content/20/5/1113.abstract},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/rank1coalg-ext.pdf"> [preprint] </a>},
  abstract = {Coalgebras provide a unifying semantic framework for a wide variety of modal logics. It has previously been shown that the class of coalgebras for an endofunctor can always be axiomatised in rank 1. Here we establish the converse, i.e. every rank 1 modal logic has a sound and strongly complete coalgebraic semantics. This is achieved by constructing for a given modal logic a canonical coalgebraic semantics, consisting of a signature functor and interpretations of modal operators, which turns out to be final among all such structures. The canonical semantics may be seen as a coalgebraic reconstruction of neighbourhood semantics, broadly construed. A finitary restriction of the canonical semantics yields a canonical weakly complete semantics which moreover enjoys the Hennessy-Milner property.

As a consequence, the machinery of coalgebraic modal logic, in particular generic decision procedures and upper complexity bounds, becomes applicable to arbitrary rank 1 modal logics, without regard to their semantic status; we thus obtain purely syntactic versions of such results. As an extended example, we apply our framework to recently defined deontic logics. In particular, our methods lead to the new result that these logics are strongly complete.
}}

@InProceedings{SchroderPattinson08c,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {How Many Toes Do I Have? Parthood and Number Restrictions in Description Logics},
  year = {2008},
  editor = {Gerhard Brewka and Jer{\^o}me Lang},
  booktitle = {Principles of Knowledge Representation and Reasoning (KR 2008)},
  publisher = {AAAI Press; Menlo Park, CA},
  pages = {307-218},
  keywords = {Coalgebra modal logic description logic number restriction parthood trees},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/TreeDL.pdf"> [preprint] </a>},
  abstract = {The modelling of parthood relations in description logics via
transitive roles often leads to undecidability when combined with
number restrictions and role hierarchies.  Here, we introduce the
description logic PHQ that explicitly supports reasoning about
parthood in the presence of qualified number restrictions. Our main
results are completeness and decidability in NEXPTIME. Conceptually, we argue that PHQ provides a better semantic fit for many
applications: more often than not, parthoods occurring e.g. in
biomedical ontologies are expected to be tree-like. In such cases,
PHQ supports stronger inferences than standard description
logics.  Technically this is achieved by explicitly excluding the
merging of descendants, which, at the same time, eliminates the
prime source of undecidability.  We work in the general setting of
coalgebraic modal logic, a generic semantic framework for
not-necessarily-normal modal logics. This added generality allows
the re-use of many of our results for other logics of sometimes
quite different flavour.
},
}

@InProceedings{SchroderPattinson09,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Strong completeness of coalgebraic modal logics},
  year = {2009},
  editor = {Susanne Albers and Jean-Yves Marion},
  booktitle = {26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009)},
  publisher = {Schloss Dagstuhl - Leibniz-Center of Informatics; Dagstuhl, Germany},
  series = {Leibniz International Proceedings in Informatics},
  pages = {673--684},
  url = {http://drops.dagstuhl.de/opus/volltexte/2009/1855},
  abstract = {Canonical models are of central importance in modal logic, in particular as they witness strong completeness and hence compactness. While the canonical model construction is well understood for Kripke semantics, non-normal modal logics often present subtle difficulties - up to the point that canonical models may fail to exist, as is the case e.g. in most probabilistic logics. Here, we present a generic canonical model construction in the semantic framework of coalgebraic modal logic, which pinpoints coherence conditions between syntax and semantics of modal logics that guarantee strong completeness. We apply this method to reconstruct canonical model theorems that are either known or folklore, and moreover instantiate our method to obtain new strong completeness results. In particular, we prove strong completeness of graded modal logic with finite multiplicities, and of the modal logic of exact probabilities.},
}

@InProceedings{SchroderPattinson10,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Named Models in Coalgebraic Hybrid Logic},
  year = {2010},
  editor = {Jean-Yves Marion and Thomas Schwentick},
  booktitle = {27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010},
  publisher = {Schloss Dagstuhl - Leibniz-Center of Informatics; Dagstuhl, Germany},
  series = {Leibniz International Proceedings in Informatics},
  volume = {5},
  pages = {645--656},
  keywords = {coalgebra modal logic named models pure completeness local binding},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/namedModels.pdf"> [preprint] </a>},
  abstract = {  Hybrid logic extends modal logic with support for reasoning about
  individual states, designated by so-called nominals. We study hybrid
  logic in the broad context of coalgebraic semantics, where
  Kripke frames are replaced with coalgebras for a given functor, thus
  covering a wide range of reasoning principles including, e.g.,
  probabilistic, graded, default, or coalitional
  operators. Specifically, we establish generic criteria for a given
  coalgebraic hybrid logic to admit named canonical models, with
  ensuing completeness proofs for pure extensions on the one hand, and
  for an extended hybrid language with local binding on the other.
  We instantiate our framework with a number of examples.
  Notably, we prove completeness of graded hybrid logic with local
  binding.
},
}

@InProceedings{SchroderPattinson10b,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Coalgebraic correspondence theory},
  year = {2010},
  editor = {Luke Ong},
  booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS 2010)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6014},
  pages = {328--342},
  keywords = {coalgebra modal logic correspondence theory rosen van benthem theorem first order logic},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/correspondence.pdf"> [preprint] </a>},
  abstract = {  We lay the foundations of a first-order correspondence theory for
  coalgebraic logics that makes the transition structure explicit in the
  first-order modelling. In particular, we prove a coalgebraic version
  of the van Benthem/Rosen theorem stating that both over arbitrary
  structures and over finite structures, coalgebraic modal logic is
  precisely the bisimulation invariant fragment of first-order logic. 
},
}

@Article{SchroderPattinson10c,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Modular   Algorithms for Heterogeneous Modal Logics via Multi-Sorted Coalgebra},
  year = {2011},
  journal = {Math. Struct. Comput. Sci.},
  volume = {21},
  pages = {235-266},
  number = {2},
  keywords = {multisorted coalgebra modal logic complexity pspace shallow models features},
  url = {http://journals.cambridge.org/action/displayAbstract?aid=8238956},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/ModAlg-Ext.pdf"> [preprint] </a>},
  abstract = {State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. Here, we show that the combination of features can be reflected algorithmically and  develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalizing the underlying state-based systems as multi-sorted coalgebras and associating both a logical and an algorithmic description to a number of basic building blocks. Our main result is that logics arising as combinations of these building blocks can be decided in polynomial space provided that this is the case for the components.  By instantiating the general framework to concrete cases, we obtain PSPACE decision procedures for a wide variety of structurally different logics, describing e.g. Segala systems and games with uncertain information.},
  note = {Copyright Cambridge University Press},
}

@InProceedings{SchroderPattinson11,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Description Logics and Fuzzy Probability},
  year = {2011},
  editor = {Toby Walsh},
  booktitle = {International Joint Conference on Artificial Intelligence, IJCAI 2011},
  publisher = {AAAI Press; Menlo Park, CA},
  keywords = {fuzzy logic coalgebra probability expectation lukasiewicz semantics complexity},
  comment = { <a href = "http://informatik.uni-bremen.de/~lschrode/papers/FuzzyCDL.pdf"> [preprint] </a>},
  pages     = {1075-1081},
  url        = {http://ijcai.org/papers11/Papers/IJCAI11-184.pdf},
  abstract = {Uncertainty and vagueness are pervasive phenomena in real-life
knowledge. They are supported in extended description logics
that adapt classical description logics to deal with numerical
probabilities or fuzzy truth values. While the two concepts are
distinguished for good reasons, they combine in the notion of
probably, which is ultimately a fuzzy qualification of
probabilities. Here, we develop existing propositional logics of
fuzzy probability into a full-blown description logic, and we show
decidability of several variants of this logic under Lukasiewicz
semantics. We obtain these results in a novel generic framework f
fuzzy coalgebraic logic; this enables us to extend our
results to logics that combine crisp ingredients including standard
crisp roles and crisp numerical probabilities with fuzzy roles and
fuzzy probabilities.},
  note = {Oral and poster presentation},
}

@InProceedings{SchroderPattison08d,
  author = {Lutz Schr{\"o}der and Dirk Pattinson},
  title = {Shallow models for non-iterative modal logics},
  year = {2008},
  editor = {Andreas Dengel and Karsten Berns and Thomas Breuel and Frank Bomarius and Thomas Roth-Berghofer},
  booktitle = {Advances in Artificial Intelligence (KI 2008)},
  publisher = {Springer},
  series = {Lecture Notes in Artificial Intelligence},
  volume = {5243},
  pages = {324-331},
  keywords = {Modal logic coalgebra agent shallow model PSPACE decision procedures},
  url = {http://dx.doi.org/10.1007/978-3-540-85845-4_40},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/nonitPSP.pdf"> [preprint] </a>},
  abstract = {Modal logics see a wide variety of applications in artificial
intelligence, e.g. in reasoning about knowledge, belief,
uncertainty, agency, defaults, and relevance. From the perspective of applications, the attractivity of modal logics stems from a combination of expressive power and comparatively low computational complexity. Compared to the classical treatment of modal logics with relational semantics, the use of modal logics in AI has two characteristic traits: Firstly, a large and growing variety of logics is used, adapted to the concrete situation at hand, and secondly, these logics are often non-normal. Here, we present a shallow model construction that witnesses PSPACE bounds for a broad class of mostly non-normal modal logics. Our approach is uniform and generic: we present general criteria that uniformly apply to and are easily checked in large numbers of examples.  Thus, we not only re-prove known complexity bounds for a wide variety of structurally different logics and obtain previously unknown PSPACE-bounds, e.g. for Elgesem's logic of agency, but also lay the foundations upon which the complexity of newly emerging logics can be determined.
},
  note = {<a href="http://arxiv.org/abs/0802.0116">Full version</a> available as e-print arXiv:0802.0116},
}

@InProceedings{SchroderVenema10,
  author = {Lutz Schr{\"o}der and Yde Venema},
  title = {Flat coalgebraic fixed point logics},
  year = {2010},
  editor = {Paul Gastin and Fran\c{c}ois Laroussinie},
  booktitle = {21st International Conference on Concurrency Theory, CONCUR 2010},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6269},
  pages = {524-538},
  keywords = {Coalgebra modal logic fixpoints fixed points mu-calculus flat single-variable alternating time graded ATL AMC},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/flatfix.pdf"> [preprint] </a>},
  abstract = {Fixed point logics
  are widely used in computer science, in particular in artificial
  intelligence and concurrency. The most expressive logics of this
  type are the mu-calculus and its relatives. However, popular
  fixed point logics tend to trade expressivity for simplicity and
  readability, and in fact often live within the single variable
  fragment of the mu-calculus. The family of such flat fixed
  point logics includes, e.g., CTL, the *-nesting-free fragment of
  PDL, and the logic of common knowledge. Here, we extend this notion
  to the generic semantic framework of coalgebraic logic, thus
  covering a wide range of logics beyond the standard mu-calculus
  including, e.g., flat fragments of the graded mu-calculus and the
  alternating-time mu-calculus (such as ATL), as well as
  probabilistic and monotone fixed point logics. Our main results are
  completeness of the Kozen-Park axiomatization and a timed-out
  tableaux method that matches ExpTime upper bounds inherited from the
  coalgebraic mu-calculus but avoids using automata.
},
}