Last update:
Sat Jun 30 09:51:48 MDT 2018
Lawrence C. Paulson Mechanizing UNITY in Isabelle . . . . . 3--32 Leonid Libkin Logics with counting and local properties . . . . . . . . . . . . . . . 33--59 Dexter Kozen On Hoare logic and Kleene algebra with tests . . . . . . . . . . . . . . . . . 60--76 Yuri Gurevich Sequential abstract-state machines capture sequential algorithms . . . . . 77--111 Martin Grohe and Thomas Schwentick Locality of order-invariant first-order formulas . . . . . . . . . . . . . . . . 112--130 Paolo Liberatore Compilability and compact representations of revision of Horn knowledge bases . . . . . . . . . . . . 131--161 Adnan Aziz and Kumud Sanwal and Vigyan Singhal and Robert Brayton Model-checking continuous-time Markov chains . . . . . . . . . . . . . . . . . 162--170 Ernie Cohen and Dexter Kozen A note on the complexity of propositional Hoare logic . . . . . . . 171--174
Nir Friedman and Joseph Y. Halpern and Daphne Koller First-order conditional logic for default reasoning revisited . . . . . . 175--207 Jürgen Dix and Mirco Nanni and V. S. Subrahmanian Probabilistic agent programs . . . . . . 208--246 Alessio R. Lomuscio and Ron van der Meyden and Mark Ryan Knowledge in multiagent systems: initial configurations and broadcast . . . . . . 247--284 Pascal van Hentenryck and Laurent Perron and Jean-François Puget Search and strategies in OPL . . . . . . 285--320
Andreas Blass and Yuri Gurevich Inadequacy of computable loop invariants 1--11 Michael Fisher and Clare Dixon and Martin Peim Clausal temporal resolution . . . . . . 12--56 Sofie Verbaeten and Danny De Schreye and Konstantinos Sagonas Termination proofs for logic programs with tabling . . . . . . . . . . . . . . 57--92 Randal E. Bryant and Steven German and Miroslav N. Velev Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic . . . . 93--134 Leonid Libkin Logics capturing local properties . . . 135--153
Tatiana Rybina and Andrei Voronkov A decision procedure for term algebras with queues . . . . . . . . . . . . . . 155--181 Andrei Voronkov How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi 182--215 Joost Engelfriet and Hendrik Jan Hoogeboom MSO definable string transductions and two-way finite-state transducers . . . . 216--254 Grigoris Antoniou and David Billington and Guido Governatori and Michael J. Maher Representation results for defeasible logic . . . . . . . . . . . . . . . . . 255--287
Thomas Lukasiewicz Probabilistic logic programming with conditional constraints . . . . . . . . 289--339 Uwe Egly and Hans Tompits Proof-complexity results for nonmonotonic reasoning . . . . . . . . . 340--387 Rajeev Alur and Kousha Etessami and Salvatore La Torre and Doron Peled Parametric temporal logic for ``model measuring'' . . . . . . . . . . . . . . 388--407 Orna Kupferman and Moshe Y. Vardi Weak alternating automata are not that weak . . . . . . . . . . . . . . . . . . 408--429
Krzysztof R. Apt and Antonis C. Kakas and Fariba Sadri Editorial . . . . . . . . . . . . . . . 431--431 Ray Reiter On knowledge-based programming with sensing in the situation calculus . . . 433--457 Nada Lavra\vc and Peter A. Flach An extended transformation approach to inductive logic programming . . . . . . 458--494 Giuseppe De Giacomo and Hector J. Levesque and Sebastian Sardiña Incremental execution of guarded theories . . . . . . . . . . . . . . . . 495--525 Vladimir Lifschitz and David Pearce and Agustín Valverde Strongly equivalent logic programs . . . 526--541 Luigia Carlucci Aiello and Fabio Massacci Verifying security protocols as planning in logic programming . . . . . . . . . . 542--580 Marek Sergot A computational theory of normative positions . . . . . . . . . . . . . . . 581--622 Marc Denecker and Maurice Bruynooghe and Victor Marek Logic programming revisited: Logic programs as inductive definitions . . . 623--654
Gerald Lüttgen and Michael Mendler The intuitionism behind Statecharts steps . . . . . . . . . . . . . . . . . 1--41 Georg Gottlob and Erich Grädel and Helmut Veith Datalog LITE: a deductive query language with linear time model checking . . . . 42--79 Raymond C. McDowell and Dale A. Miller Reasoning with higher-order abstract syntax in a logical framework . . . . . 80--136 Andrea Asperti and Luca Roversi Intuitionistic Light Affine Logic . . . 137--175
Francesco M. Donini and Daniele Nardi and Riccardo Rosati Description logics of minimal knowledge and negation as failure . . . . . . . . 177--225 Piero Andrea Bonatti and Nicola Olivetti Sequent calculi for propositional nonmonotonic logics . . . . . . . . . . 226--278 J. V. Tucker and J. I. Zucker Abstract computability and algebraic specification . . . . . . . . . . . . . 279--333
Martín Abadi and Leonid Libkin and Frank Pfenning Editorial . . . . . . . . . . . . . . . 335--335 Martin Grohe and Luc Segoufin On first-order topological queries . . . 336--358 Vincent Danos and Russell S. Harmer Probabilistic game semantics . . . . . . 359--382 Klaus Aehlig and Helmut Schwichtenberg A syntactical analysis of non-size-increasing polynomial time computation . . . . . . . . . . . . . . 383--401 Samuel R. Buss and Bruce M. Kapron Resource-bounded continuity and sequentiality for type-two functionals 402--417 Erich Grädel and Colin Hirsch and Martin Otto Back and forth between guarded and modal logics . . . . . . . . . . . . . . . . . 418--463
Mario Bravetti and Roberto Gorrieri Deciding and axiomatizing weak ST bisimulation for a process algebra with recursion and action refinement . . . . 465--520 Robert Givan and David Mcallester Polynomial-time computation via local inference relations . . . . . . . . . . 521--541 Michael Kaminski and Guy Rey Revisiting quantification in autoepistemic logic . . . . . . . . . . 542--561 Viviana Bono and Michele Bugliesi and Silvia Crafa Typed interpretations of extensible objects . . . . . . . . . . . . . . . . 562--603 Randal E. Bryant and Miroslav N. Velev Boolean satisfiability with transitivity constraints . . . . . . . . . . . . . . 604--627
Philip Wadler and Peter Thiemann The marriage of effects and monads . . . 1--32 Hubert Comon and Paliath Narendran and Robert Nieuwenhuis and Michael Rusinowitch Deciding the confluence of ordered term rewrite systems . . . . . . . . . . . . 33--55 James Harland and David Pym Resource-distribution via Boolean constraints . . . . . . . . . . . . . . 56--90 Zbigniew Lonc and Miroslaw Truszczy\'nski Fixed-parameter complexity of semantics for logic programs . . . . . . . . . . . 91--119 M. Dezani-Ciancaglini and F. Honsell and F. Alessi A complete characterization of complete intersection-type preorders . . . . . . 120--147
Fabrizio Angiulli and Rachel Ben-Eliyahu-Zohary and Giovambattista Ianni and Luigi Palopoli Computational properties of metaquerying problems . . . . . . . . . . . . . . . . 149--180 Doron Bustan and Orna Grumberg Simulation-based minimization . . . . . 181--206 Fred Mesnard and Salvatore Ruggieri On proving left termination of constraint logic programs . . . . . . . 207--259 Oliver Kutz and Frank Wolter and Holger Sturm and Nobu-Yuki Suzuki and Michael Zakharyaschev Logics of metric spaces . . . . . . . . 260--294
Erich Grädel and Joseph Y. Halpern and Radha Jaghadeesan and Adolfo Piperno LICS 2001 special issue . . . . . . . . 295--295 Micah Adler and Neil Immerman An $n!$ lower bound on formula size . . 296--314 Noga Alon and Tova Milo and Frank Neven and Dan Suciu and Victor Vianu Typechecking XML views of relational databases . . . . . . . . . . . . . . . 315--354 Dexter Kozen and Jerzy Tiuryn Substructural logic and partial correctness . . . . . . . . . . . . . . 355--378 Antonino Salibra Topological incompleteness and order incompleteness of the lambda calculus 379--401 Jeremy Avigad Eliminating definitions and Skolem functions in first-order logic . . . . . 402--415
Yi-Dong Shen and Jia-Huai You and Li-Yan Yuan and Samuel S. P. Shen and Qiang Yang A dynamic approach to characterizing termination of general logic programs 417--430 Leonid Libkin Variable independence for first-order definable constraints . . . . . . . . . 431--451 Jeremy Bryans and Howard Bowman and John Derrick Model checking stochastic automata . . . 452--492 Alberto Momigliano and Frank Pfenning Higher-order pattern complement and the strict $\lambda$-calculus . . . . . . . 493--529 Peter Buneman and Wenfei Fan and Scott Weinstein Interaction between path and type constraints . . . . . . . . . . . . . . 530--577 Andreas Blass and Yuri Gurevich Abstract state machines capture parallel algorithms . . . . . . . . . . . . . . . 578--651
Rajeev Alur and Salvatore La Torre Deterministic generators and games for Ltl fragments . . . . . . . . . . . . . 1--25 Bard Bloom and Wan Fokkink and Rob J. Van Glabbeek Precongruence formats for decorated trace semantics . . . . . . . . . . . . 26--78 Rocco De Nicola and Michele Loreti A modal logic for mobile agents . . . . 79--128 Stefan Brass and Jürgen Dix and Teodor C. Przymusinski Super logic programs . . . . . . . . . . 129--176
Slim Abdennadher and Christophe Rigotti Automatic generation of rule-based constraint solvers over finite domains 177--205 Thomas Eiter and Wolfgang Faber and Nicola Leone and Gerald Pfeifer and Axel Polleres A logic programming approach to knowledge-state planning: Semantics and complexity . . . . . . . . . . . . . . . 206--263 Stefan Ratschan Convergent approximate solving of first-order constraints by approximate quantifiers . . . . . . . . . . . . . . 264--281 Anuj Dawar and Erich Grädel and Stephan Kreutzer Inflationary fixed points in modal logic 282--315 K. Subramani Optimal length tree-like resolution refutations for 2SAT formulas . . . . . 316--320 Guillem Godoy and Robert Nieuwenhuis and Ashish Tiwari Classes of term rewrite systems with polynomial confluence problems . . . . . 321--331 Aleksandar Ignjatovic and Arun Sharma Some applications of logic to feasibility in higher types . . . . . . 332--350 Laurent Michel and Pascal Van Hentenryck A decomposition-based implementation of search strategies . . . . . . . . . . . 351--383
Pawel Mielniczuk Basic theory of feature trees . . . . . 385--402 Frank Neven and Thomas Schwentick and Victor Vianu Finite state machines for strings over infinite alphabets . . . . . . . . . . . 403--435 Marco Bernardo Symbolic semantic rules for producing compact STGLAs from value passing process descriptions . . . . . . . . . . 436--469 Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus Termination of simply moded logic programs with dynamic scheduling . . . . 470--507 Yann Loyer and Nicolas Spyratos and Daniel Stamate Hypothesis-based semantics of logic programs in multivalued logics . . . . . 508--527 David Basin and Manuel Clavel and José Meseguer Reflective metalogical frameworks . . . 528--576
David Griffioen and Frits Vaandrager A theory of normed simulations . . . . . 577--610 J. V. Tucker and J. I. Zucker Abstract versus concrete computation on metric partial algebras . . . . . . . . 611--668 Carsten Lutz NEXP TIME-complete description logics with concrete domains . . . . . . . . . 669--705 Frank S. De Boer and Maurizio Gabbrielli and Maria Chiara Meo Proving correctness of timed concurrent constraint programs . . . . . . . . . . 706--731 Frédéric Benhamou and Frédéric Goualard and Éric Languénou and Marc Christie Interval constraint solving for camera control and motion planning . . . . . . 732--767
Thomas A. Henzinger and Rupak Majumdar and Jean-François Raskin A classification of symbolic transition systems . . . . . . . . . . . . . . . . 1--32 Roberto Giacobazzi and Francesco Ranzato and Francesca Scozzari Making abstract domains condensing . . . 33--60 Robert Harper and Frank Pfenning On equivalence and canonical forms in the LF type theory . . . . . . . . . . . 61--101 Rakesh Verma and Ara Hayrapetyan A new decidability technique for ground term rewriting systems with applications 102--123 Churn-Jung Liau A modal logic framework for multi-agent belief fusion . . . . . . . . . . . . . 124--174 Wim H. Hesselink Eternity variables to prove simulation of specifications . . . . . . . . . . . 175--201
Chiaki Sakama Induction from answer sets in nonmonotonic logic programs . . . . . . 203--231 Marco Cadoli and Thomas Eiter and Georg Gottlob Complexity of propositional nested circumscription and nested abnormality theories . . . . . . . . . . . . . . . . 232--272 Orna Kupferman and Moshe Y. Vardi From linear time to branching time . . . 273--294 Kewen Wang and Lizhu Zhou Comparisons and computation of well-founded semantics for disjunctive logic programs . . . . . . . . . . . . . 295--327 Sara Cohen and Yehoshua Sagiv and Werner Nutt Equivalences among aggregate queries with negation . . . . . . . . . . . . . 328--360 Konstantin Korovin and Andrei Voronkov Knuth--Bendix constraint solving is NP-complete . . . . . . . . . . . . . . 361--388 Thomas Eiter and Michael Fink and Giuliana Sabbatini and Hans Tompits Reasoning about evolving nonmonotonic knowledge bases . . . . . . . . . . . . 389--440 Panos Rondogiannis and William W. Wadge Minimum model semantics for logic programs with negation-as-failure . . . 441--467 Klaus Aehlig and Jan Johannsen An elementary fragment of second-order lambda calculus . . . . . . . . . . . . 468--480
Foto Afrati and Stavros Cosmadakis and Eugénie Foustoucos Datalog programs and their persistency numbers . . . . . . . . . . . . . . . . 481--518 Mauro Ferrari and Camillo Fiorentini and Guido Fiorino On the complexity of the disjunction property in intuitionistic and modal logics . . . . . . . . . . . . . . . . . 519--538 Matthew Stone Disjunction and modular goal-directed proof search . . . . . . . . . . . . . . 539--577 George Metcalfe and Nicola Olivetti and Dov Gabbay Sequent and hypersequent calculi for abelian and \Lukasiewicz logics . . . . 578--613 Bernard Boigelot and Sébastien Jodogne and Pierre Wolper An effective decision procedure for linear arithmetic over the integers and reals . . . . . . . . . . . . . . . . . 614--633 Nicole Schweikardt Arithmetic, first-order logic, and counting quantifiers . . . . . . . . . . 634--671
Krzysztof R. Apt Editorial . . . . . . . . . . . . . . . 673--673 Phokion G. Kolaitis LICS 2003 special issue . . . . . . . . 674--674 Bakhadyr Khoussainov and Sasha Rubin and Frank Stephan Automatic linear orders and trees . . . 675--700 Andrzej S. Murawski About the undecidability of program equivalence in finitary languages with state . . . . . . . . . . . . . . . . . 701--726 James F. Lynch Convergence law for random graphs with specified degree sequence . . . . . . . 727--748 Dale Miller and Alwen Tiu A proof theory for generic judgments . . 749--783 Dominic J. D. Hughes and Rob J. Van Glabbeek Proof nets for unit-free multiplicative-additive linear logic . . 784--842
Tomi Janhunen and Ilkka Niemelä and Dietmar Seipel and Patrik Simons and Jia-Huai You Unfolding partiality and disjunctions in stable model semantics . . . . . . . . . 1--37 Deborah East and Miroslaw Truszczy\'nski Predicate-calculus-based logics for modeling and solving search problems . . 38--83 Paolo Liberatore Complexity results on DPLL and resolution . . . . . . . . . . . . . . . 84--107 Anatoli Degtyarev and Michael Fisher and Boris Konev Monodic temporal resolution . . . . . . 108--150 Jürgen Dix and Sarit Kraus and V. S. Subrahmanian Heterogeneous temporal probabilistic agents . . . . . . . . . . . . . . . . . 151--198
Russell Impagliazzo and Nathan Segerlind Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations . . . . . . 199--218 Paolo Coppola and Simone Martini Optimizing optimal reduction: a type inference algorithm for elementary affine logic . . . . . . . . . . . . . . 219--260 Vladimir Lifschitz and Alexander Razborov Why are there so many loop formulas? . . 261--268 Agostino Dovier and Andrea Formisano and Eugenio G. Omodeo Decidability results for sets with atoms 269--301 Giorgi Japaridze Propositional computability logic I . . 302--330 Giorgi Japaridze Propositional computability logic II . . 331--362 Andreas Blass and Yuri Gurevich Ordinary interactive small-step algorithms, I . . . . . . . . . . . . . 363--419
Yan Zhang Logic program-based updates . . . . . . 421--472 Andrzej S. Murawski and C.-H. Luke Ong Fast verification of MLL proof nets via IMLL . . . . . . . . . . . . . . . . . . 473--498 Nicola Leone and Gerald Pfeifer and Wolfgang Faber and Thomas Eiter and Georg Gottlob and Simona Perri and Francesco Scarcello The DLV system for knowledge representation and reasoning . . . . . . 499--562 Stefano Bistarelli and Ugo Montanari and Francesca Rossi Soft concurrent constraint programming 563--589 Arthur Charlesworth Comprehending software correctness implies comprehending an intelligence-related limitation . . . . 590--612
Tran Cao Son and Chitta Baral and Nam Tran and Sheila Mcilraith Domain-dependent knowledge in answer set planning . . . . . . . . . . . . . . . . 613--657 Lawrence C. Paulson Defining functions on equivalence classes . . . . . . . . . . . . . . . . 658--675 Christopher A. Stone and Robert Harper Extensional equivalence and singleton types . . . . . . . . . . . . . . . . . 676--722 Stefan Ratschan Efficient solving of quantified inequality constraints over the real numbers . . . . . . . . . . . . . . . . 723--748 Stephen Cook and Neil Thapen The strength of replacement in weak arithmetic . . . . . . . . . . . . . . . 749--764 Joost Vennekens and David Gilis and Marc Denecker Splitting an operator: Algebraic modularity results for logics with fixpoint semantics . . . . . . . . . . . 765--797 Jules Desharnais and Bernhard Möller and Georg Struth Kleene algebra with domain . . . . . . . 798--833
Maria Paola Bonacina and Nachum Dershowitz Abstract canonical inference . . . . . . ?? Alessio Guglielmi A system of interaction and structure ?? Paolo Liberatore and Marco Schaerf Compilability of propositional abduction ?? Annabelle McIver and Carroll Morgan Results on the quantitative $\mu$-calculus $q{M}\mu$ . . . . . . . . ?? Alexander Rabinovich On compositionality and its limitations ?? Joost Vennekens and David Gilis and Marc Denecker Erratum to splitting an operator: Algebraic modularity results for logics with fixpoint semantics . . . . . . . . ?? Greta Yorsh and Thomas Reps and Mooly Sagiv and Reinhard Wilhelm Logical characterizations of heap abstractions . . . . . . . . . . . . . . ??
Michael Benedikt and Leonid Libkin and Frank Neven Logical definability and query languages over ranked and unranked trees . . . . . ?? Karl Crary Sound and complete elimination of singleton kinds . . . . . . . . . . . . ?? John M. Hitchcock and Jack H. Lutz and Sebastiaan A. Terwijn The arithmetical complexity of dimension and randomness . . . . . . . . . . . . . ?? Paolo Liberatore Where fail-safe default logics fail . . ?? Fangzhen Lin and Jia-Huai You Recycling computed answers in rewrite systems for abduction . . . . . . . . . ?? Viorica Sofronie-Stokkermans On unification for bounded distributive lattices . . . . . . . . . . . . . . . . ??
Marco Pedicini and Francesco Quaglia PELCR: Parallel environment for optimal lambda-calculus reduction . . . . . . . 14:1--14:?? Andreas Blass and Yuri Gurevich Ordinary interactive small-step algorithms, II . . . . . . . . . . . . . 15:1--15:?? Andreas Blass and Yuri Gurevich Ordinary interactive small-step algorithms, III . . . . . . . . . . . . 16:1--16:?? Thomas Eiter and Michael Fink and Stefan Woltran Semantical characterizations and complexity of equivalences in answer set programming . . . . . . . . . . . . . . 17:1--17:?? Ofer Arieli Paraconsistent reasoning and preferential entailments by signed quantified Boolean formulae . . . . . . 18:1--18:??
Renate A. Schmidt and Ullrich Hustadt The axiomatic translation principle for modal logic . . . . . . . . . . . . . . 19:1--19:?? Sophie Laplante and Richard Lassaigne and Frédéric Magniez and Sylvain Peyronnet and Michel de Rougemont Probabilistic abstraction for model checking: an approach based on property testing . . . . . . . . . . . . . . . . 20:1--20:?? Arnaud Durand and Etienne Grandjean First-order queries on structures of bounded degree are computable with constant delay . . . . . . . . . . . . . 21:1--21:?? Nicola Olivetti and Gian Luca Pozzato and Camilla B. Schwind A sequent calculus and a theorem prover for standard conditional logics . . . . 22:1--22:?? C. W. Choi and J. H. M. Lee and P. J. Stuckey Removing propagation redundant constraints in redundant modeling . . . 23:1--23:?? Edward Hung and Lise Getoor and V. S. Subrahmanian Probabilistic interval XML . . . . . . . 24:1--24:??
Sharon Shoham and Orna Grumberg A game-based framework for CTL counterexamples and 3-valued abstraction-refinement . . . . . . . . . 1:1--1:?? Jeremy Avigad and Kevin Donnelly and David Gray and Paul Raff A formally verified proof of the prime number theorem . . . . . . . . . . . . . 2:1--2:23 Jan Van den Bussche and Stijn Vansummeren Polymorphic type inference for the named nested relational calculus . . . . . . . 3:1--3:?? Shuvendu K. Lahiri and Randal E. Bryant Predicate abstraction with indexed predicates . . . . . . . . . . . . . . . 4:1--4:?? Christel Baier and Nathalie Bertrand and Philippe Schnoebelen Verifying nondeterministic probabilistic channel systems against $\omega$-regular linear-time properties . . . . . . . . . 5:1--5:?? Ma\lgorzata Biernacka and Olivier Danvy A concrete framework for environment machines . . . . . . . . . . . . . . . . 6:1--6:?? Fabrizio Angiulli and Gianluigi Greco and Luigi Palopoli Outlier detection by logic programming 7:1--7:??
Silvio Ghilardi and Enrica Nicolini and Daniele Zucchelli A comprehensive combination framework 8:1--8:?? Chiaki Sakama and Katsumi Inoue Coordination in answer set programming 9:1--9:?? Slawomir Lasota and Igor Walukiewicz Alternating timed automata . . . . . . . 10:1--10:?? Felix Klaedtke Bounds on the automata size for Presburger arithmetic . . . . . . . . . 11:1--11:?? Véronique Bruy\`ere and Emmanuel Dall'olio and Jean-François Raskin Durations and parametric model-checking in timed automata . . . . . . . . . . . 12:1--12:?? Floris Geerts and Sofie Haesevoets and Bart Kuijpers First-order complete and computationally complete query languages for spatio-temporal databases . . . . . . . 13:1--13:?? Marc Denecker and Eugenia Ternovska A logic of nonmonotone inductive definitions . . . . . . . . . . . . . . 14:1--14:??
Agostino Dovier and Carla Piazza and Gianfranco Rossi A uniform approach to constraint-solving for lists, multisets, compact lists, and sets . . . . . . . . . . . . . . . . . . 15:1--15:?? Karl Crary and Susmit Sarkar Foundational certified code in the Twelf metalogical framework . . . . . . . . . 16:1--16:?? Samir Genaim and Andy King Inferring non-suspension conditions for logic programs with dynamic scheduling 17:1--17:?? Andreas Blass and Yuri Gurevich Program termination and well partial orderings . . . . . . . . . . . . . . . 18:1--18:?? Andreas Blass and Yuri Gurevich Abstract state machines capture parallel algorithms: Correction and extension . . 19:1--19:?? Hana Chockler and Joseph Y. Halpern and Orna Kupferman What causes a system to satisfy a specification? . . . . . . . . . . . . . 20:1--20:?? Simone Bova and Franco Montagna Proof search in Hájek's basic logic . . . 21:1--21:?? Diego Calvanese and Giuseppe De Giacomo and Maurizio Lenzerini Conjunctive query containment and answering under description logic constraints . . . . . . . . . . . . . . 22:1--22:?? Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka Contextual modal type theory . . . . . . 23:1--23:??
Yannick Chevalier and Ralf Küsters and Michaël Rusinowitch and Mathieu Turuani Complexity results for security protocols with Diffie--Hellman exponentiation and commuting public key encryption . . . . . . . . . . . . . . . 24:1--24:?? Frank Wolter and Michael Zakharyaschev Undecidability of the unification and admissibility problems for modal and description logics . . . . . . . . . . . 25:1--25:?? Stijn Heymans and Davy Van Nieuwenborgh and Dirk Vermeir Open answer set programming with guarded programs . . . . . . . . . . . . . . . . 26:1--26:?? Yi-Dong Shen Reasoning with recursive loops under the PLP framework . . . . . . . . . . . . . 27:1--27:?? Helmut Seidl and Kumar Neeraj Verma Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying . . 28:1--28:?? Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni Verifiable agent interaction in abductive logic programming: The SCIFF framework . . . . . . . . . . . . . . . 29:1--29:??
Alexander Artikis and Marek Sergot and Jeremy Pitt Specifying norm-governed computational societies . . . . . . . . . . . . . . . 1:1--1:?? Lou Van Den Dries and Yiannis N. Moschovakis Arithmetic complexity . . . . . . . . . 2:1--2:?? Neil Yorke-Smith and Carmen Gervet Certainty closure: Reliable constraint reasoning with incomplete or erroneous data . . . . . . . . . . . . . . . . . . 3:1--3:?? Alessandro Armando and Maria Paola Bonacina and Silvio Ranise and Stephan Schulz New results on rewrite-based satisfiability procedures . . . . . . . 4:1--4:?? Luca Iocchi and Thomas Lukasiewicz and Daniele Nardi and Riccardo Rosati Reasoning about actions with sensing under qualitative and probabilistic uncertainty . . . . . . . . . . . . . . 5:1--5:?? Luca Aceto and Wan Fokkink and Anna Ingolfsdottir and Bas Luttik A finite equational base for CCS with left merge and communication merge . . . 6:1--6:?? Juha Kontinen A logical characterization of the counting hierarchy . . . . . . . . . . . 7:1--7:??
Ugo Dal Lago The geometry of linear higher-order recursion . . . . . . . . . . . . . . . 8:1--8:?? Ruggero Lanotte and Simone Tini Probabilistic bisimulation as a congruence . . . . . . . . . . . . . . . 9:1--9:?? Isabelle Gnaedig and Hél\`ene Kirchner Termination of rewriting under strategies . . . . . . . . . . . . . . . 10:1--10:?? Maurizio Gabbrielli and Maria Chiara Meo A compositional semantics for CHR . . . 11:1--11:?? Stefano Guerrini and Andrea Masini Proofs, tests and continuation passing style . . . . . . . . . . . . . . . . . 12:1--12:?? Lutz Schröder and Dirk Pattinson PSPACE bounds for rank-1 modal logics 13:1--13:?? Paola Bruscoli and Alessio Guglielmi On the proof complexity of deep inference . . . . . . . . . . . . . . . 14:1--14:??
Stavros Tripakis Checking timed Büchi automata emptiness on simulation graphs . . . . . . . . . . 15:1--15:?? Stéphane Demri and Ranko Lazi\'c LTL with the freeze quantifier and register automata . . . . . . . . . . . 16:1--16:?? Lucas Bordeaux and Marco Cadoli and Toni Mancini Generalizing consistency and other constraint properties to quantified constraints . . . . . . . . . . . . . . 17:1--17:?? Laura Giordano and Valentina Gliozzi and Nicola Olivetti and Gian Luca Pozzato Analytic tableaux calculi for KLM logics of nonmonotonic reasoning . . . . . . . 18:1--18:?? Mingsheng Ying and Yuan Feng and Runyao Duan and Zhengfeng Ji An algebra of quantum processes . . . . 19:1--19:?? Adel Bouhoula Simultaneous checking of completeness and ground confluence for algebraic specifications . . . . . . . . . . . . . 20:1--20:?? Laura Giordano and Valentina Gliozzi and Nicola Olivetti and Camilla Schwind Tableau calculus for preference-based conditional logics: PCL and its extensions . . . . . . . . . . . . . . . 21:1--21:?? Akitoshi Kawamura Differential recursion . . . . . . . . . 22:1--22:??
Patrick Baillot and Jean-Yves Marion and Simona Ronchi Della Rocca Guest editorial: Special issue on implicit computational complexity . . . 23:1--23:?? Toshiyasu Arai and Naohi Eguchi A new function algebra of EXPTIME functions by safe nested recursion . . . 24:1--24:?? Ugo Dal Lago Context semantics, linear logic, and computational complexity . . . . . . . . 25:1--25:?? Tristan Crolard and Emmanuel Polonowski and Pierre Valarcher Extending the loop language with higher-order procedural variables . . . 26:1--26:?? Jean-Yves Marion and Romain Péchoux Sup-interpretations, a semantic method for static analysis of program resources 27:1--27:?? Neil D. Jones and Lars Kristiansen A flow calculus of mwp-bounds for complexity analysis . . . . . . . . . . 28:1--28:?? Jean-Yves Moyen Resource control graphs . . . . . . . . 29:1--29:??
Krishnendu Chatterjee and Thomas A. Henzinger and Florian Horn Finitary winning in $\omega$-regular games . . . . . . . . . . . . . . . . . 1:1--1:?? Peter Schneider-Kamp and Jürgen Giesl and Alexander Serebrenik and René Thiemann Automated termination proofs for logic programs by term rewriting . . . . . . . 2:1--2:?? Valentin Goranko and Dmitry Shkatov Tableau-based decision procedures for logics of strategic ability in multiagent systems . . . . . . . . . . . 3:1--3:?? Michael Benedikt and Luc Segoufin Regular tree languages definable in FO and in FO$_{mod}$ . . . . . . . . . . . 4:1--4:?? Ferruccio Guidi The formal system $\lambda \delta$ . . . 5:1--5:?? Brigitte Pientka Higher-order term indexing using substitution trees . . . . . . . . . . . 6:1--6:?? Rob Arthan and Ursula Martin and Erik A. Mathiesen and Paulo Oliva A general framework for sound and complete Floyd-Hoare logics . . . . . . 7:1--7:??
James Bailey and Guozhu Dong and Anthony Widjaja To Logical queries over views: Decidability and expressiveness . . . . . . . . . . . 8:1--8:?? Hubert Comon-Lundh and Véronique Cortier and Eugen Zãlinescu Deciding security properties for cryptographic protocols. Application to key cycles . . . . . . . . . . . . . . . 9:1--9:?? Octavian Udrea and Diego Reforgiato Recupero and V. S. Subrahmanian Annotated RDF . . . . . . . . . . . . . 10:1--10:?? Robin Adams and Zhaohui Luo Weyl's predicative classical mathematics as a logic-enriched type theory . . . . 11:1--11:?? Stavros Cosmadakis and Eugenie Foustoucos and Anastasios Sidiropoulos Undecidability and intractability results concerning datalog programs and their persistency numbers . . . . . . . 12:1--12:?? Alwen Tiu and Dale Miller Proof search specifications of bisimulation and modal logics for the $\pi$-calculus . . . . . . . . . . . . . 13:1--13:?? Thomas Eiter and Mantas \vSimkus FDNC: Decidable nonmonotonic disjunctive logic programs with function symbols . . 14:1--14:??
Manuel Bodirsky and Jan Kára A fast algorithm and datalog inexpressibility for temporal reasoning 15:1--15:?? Kedar S. Namjoshi and Richard J. Trefler On the completeness of compositional reasoning methods . . . . . . . . . . . 16:1--16:?? Detlef Kähler and Ralf Küsters and Thomas Wilke Deciding strategy properties of contract-signing protocols . . . . . . . 17:1--17:?? Nachum Dershowitz and Iddo Tzameret Complexity of propositional proofs under a promise . . . . . . . . . . . . . . . 18:1--18:?? Eli Ben-Sasson and Prahladh Harsha Lower bounds for bounded depth Frege proofs via Pudlák--Buss games . . . . . . 19:1--19:?? Marko Samer and Helmut Veith On the distributivity of LTL specifications . . . . . . . . . . . . . 20:1--20:??
Michael Kaminski and Simone Martini CSL 2008 special issue . . . . . . . . . 21:1--21:?? Olaf Beyersdorff and Sebastian Müller A tight Karp--Lipton collapse result in bounded arithmetic . . . . . . . . . . . 22:1--22:?? Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger Quantitative languages . . . . . . . . . 23:1--23:?? Nadia Creignou and Henning Schnoor and Ilka Schnoor Nonuniform Boolean constraint satisfaction problems with cardinality constraint . . . . . . . . . . . . . . . 24:1--24:?? Mariangiola Dezani-Ciancaglini and Roberto Di Cosmo and Elio Giovannetti and Makoto Tatsuta On isomorphisms of intersection types 25:1--25:?? Martin Hofmann and Ulrich Schöpp Pure pointer programs with iteration . . 26:1--26:?? Matthias Horbach and Christoph Weidenbach Superposition for fixed domains . . . . 27:1--27:?? Alexis Saurin Typing streams in the $\Lambda \mu$-calculus . . . . . . . . . . . . . 28:1--28:?? Hana Chockler and Joseph Y. Halpern and Orna Kupferman Erratum for ``What causes a system to satisfy a specification?'' . . . . . . . 29:1--29:??
Rohit Chadha and Mahesh Viswanathan A counterexample-guided abstraction-refinement framework for Markov decision processes . . . . . . . 1:1--1:?? Axel Legay and Pierre Wolper On (Omega-)regular model checking . . . 2:1--2:?? Georg Gottlob and Reinhard Pichler and Fang Wei Monadic datalog over finite structures of bounded treewidth . . . . . . . . . . 3:1--3:?? Nicola Galesi and Massimo Lauria Optimality of size-degree tradeoffs for polynomial calculus . . . . . . . . . . 4:1--4:?? Stefano Bistarelli and Ugo Montanari and Francesca Rossi and Francesco Santini Unicast and multicast QoS routing with soft-constraint logic programming . . . 5:1--5:?? David Billington and Grigoris Antoniou and Guido Governatori and Michael Maher An inclusion theorem for defeasible logics . . . . . . . . . . . . . . . . . 6:1--6:?? Alessandro Cimatti and Alberto Griggio and Roberto Sebastiani Efficient generation of Craig interpolants in satisfiability modulo theories . . . . . . . . . . . . . . . . 7:1--7:?? Carlo A. Furia and Matteo Rossi A theory of sampling for continuous-time metric temporal logic . . . . . . . . . 8:1--8:??
Yuri Gurevich and Itay Neeman Logic of infons: The propositional case 9:1--9:?? Ranko Lazi\'c Safety alternating automata on data words . . . . . . . . . . . . . . . . . 10:1--10:?? Thomas Eiter and Giovambattista Ianni and Thomas Lukasiewicz and Roman Schindlauer Well-founded semantics for description logic programs in the Semantic Web . . . 11:1--11:?? Stefan Szeider Monadic second order logic on graphs with local cardinality constraints . . . 12:1--12:?? Michael Bauland and Martin Mundhenk and Thomas Schneider and Henning Schnoor and Ilka Schnoor and Heribert Vollmer The tractability of model checking for LTL: The good, the bad, and the ugly fragments . . . . . . . . . . . . . . . 13:1--13:?? Paulo Shakarian and Austin Parker and Gerardo Simari and Venkatramana V. S. Subrahmanian Annotated probabilistic temporal logic 14:1--14:?? Christian Urban and James Cheney and Stefan Berghofer Mechanizing the metatheory of LF . . . . 15:1--15:?? Andreas Blass and Yuri Gurevich Persistent queries in the behavioral theory of algorithms . . . . . . . . . . 16:1--16:?? Anastasia Analyti and Grigoris Antoniou and Carlos Viegas Damasio MWeb: a principled framework for modular Web rule bases and its semantics . . . . 17:1--17:??
Flemming Nielson and Sebastian Nanz and Hanne Riis Nielson Modal abstractions of concurrent behavior . . . . . . . . . . . . . . . . 18:1--18:?? Marcin Jurdzi\'nski and Ranko Lazi\'c Alternating automata on data trees and XPath satisfiability . . . . . . . . . . 19:1--19:?? Jos De Bruijn and Thomas Eiter and Axel Polleres and Hans Tompits Embedding nonground logic programs into autoepistemic logic for knowledge-base combination . . . . . . . . . . . . . . 20:1--20:?? Jan A. Bergstra and Alban Ponse Proposition algebra . . . . . . . . . . 21:1--21:?? José Espírito Santo and Luís Pinto A calculus of multiary sequent terms . . 22:1--22:??
Lutz Straß Burger and Alessio Guglielmi A system of interaction and structure IV: The exponentials and decomposition 23:1--23:?? Andrei A. Bulatov Complexity of conservative constraint satisfaction problems . . . . . . . . . 24:1--24:?? Paolo Ferraris Logic programs with propositional connectives and aggregates . . . . . . . 25:1--25:?? Adri\`a Gascón and Guillem Godoy and Manfred Schmidt-Schauss Unification and matching on compressed terms . . . . . . . . . . . . . . . . . 26:1--26:?? Miko\laj Boja\'nczyk and Claire David and Anca Muscholl and Thomas Schwentick and Luc Segoufin Two-variable logic on data words . . . . 27:1--27:?? Krishnendu Chatterjee and Luca De Alfaro and Thomas A. Henzinger Qualitative concurrent parity games . . 28:1--28:?? Md. Aquil Khan and Mohua Banerjee Logics for information systems and their dynamic extensions . . . . . . . . . . . 29:1--29:??
Arie Gurfinkel and Marsha Chechik Robust Vacuity for Branching Temporal Logic . . . . . . . . . . . . . . . . . 1:1--1:?? David Baelde Least and Greatest Fixed Points in Linear Logic . . . . . . . . . . . . . . 2:1--2:?? Benno van den Berg and Richard Garner Topological and Simplicial Models of Identity Types . . . . . . . . . . . . . 3:1--3:?? Wouter Gelade and Frank Neven Succinctness of the Complement and Intersection of Regular Expressions . . 4:1--4:?? Florent Madelaine and Barnaby Martin The Complexity of Positive First-Order Logic without Equality . . . . . . . . . 5:1--5:?? Cinzia Di Giusto and Maurizio Gabbrielli and Maria Chiara Meo On the Expressive Power of Multiple Heads in CHR . . . . . . . . . . . . . . 6:1--6:?? Naghmeh Ghafari and Arie Gurfinkel and Nils Klarlund and Richard Trefler Reachability Problems in Piecewise FIFO Systems . . . . . . . . . . . . . . . . 7:1--7:?? Jeroen J. A. Keiren and Michel A. Reniers and Tim A. C. Willemse Structural Analysis of Boolean Equation Systems . . . . . . . . . . . . . . . . 8:1--8:?? Phuong Nguyen and Stephen Cook The Complexity of Proving the Discrete Jordan Curve Theorem . . . . . . . . . . 9:1--9:??
Jordi Levy and Mateu Villaret Nominal Unification from a Higher-Order Perspective . . . . . . . . . . . . . . 10:1--10:?? Stefano Berardi and Ugo de'Liguoro Interactive Realizers: a New Approach to Program Extraction from Nonconstructive Proofs . . . . . . . . . . . . . . . . . 11:1--11:?? Kousha Etessami and Mihalis Yannakakis Model Checking of Recursive Probabilistic Systems . . . . . . . . . 12:1--12:?? Paulo Shakarian and Gerardo I. Simari and V. S. Subrahmanian Annotated Probabilistic Temporal Logic: Approximate Fixpoint Implementation . . 13:1--13:?? Mauro Ferrari and Camillo Fiorentini and Guido Fiorino Simplification Rules for Intuitionistic Propositional Tableaux . . . . . . . . . 14:1--14:?? Sebastian Danicic and Robert M. Hierons and Michael R. Laurence Complexity of Data Dependence Problems for Program Schemas with Concurrency . . 15:1--15:?? Jakob Nordström On the Relative Strength of Pebbling and Resolution . . . . . . . . . . . . . . . 16:1--16:?? Nadia Creignou and Arne Meier and Heribert Vollmer and Michael Thomas The Complexity of Reasoning for Fragments of Autoepistemic Logic . . . . 17:1--17:?? Marco Gaboardi and Jean-Yves Marion and Simona Ronchi Della Rocca An Implicit Characterization of PSPACE 18:1--18:??
Wouter Gelade and Marcel Marquardt and Thomas Schwentick The dynamic complexity of formal languages . . . . . . . . . . . . . . . 19:1--19:?? Gilles Dowek and Murdoch J. Gabbay Permissive-nominal logic: First-order logic over nominal terms and sets . . . 20:1--20:?? Franz Baader and Silvio Ghilardi and Carsten Lutz LTL over description logic axioms . . . 21:1--21:?? Sara Miner More and Pavel Naumov Calculus of cooperation and game-based reasoning about protocol privacy . . . . 22:1--22:?? Kazuhisa Makino and Hirotaka Ono Deductive inference for the interiors and exteriors of Horn theories . . . . . 23:1--23:?? Bjòrn Kjos-Hanssen and Frank Stephan and Jason Teutsch Arithmetic complexity via effective names for random sequences . . . . . . . 24:1--24:?? Alessandro Bianco and Fabio Mogavero and Aniello Murano Graded computation tree logic . . . . . 25:1--25:?? Robert Goldblatt and Marcel Jackson Well-structured program equivalence is highly undecidable . . . . . . . . . . . 26:1--26:?? Rajeev Alur and Pavol Cerný and Scott Weinstein Algorithmic analysis of array-accessing programs . . . . . . . . . . . . . . . . 27:1--27:??
Konstantinos Chatzikokolakis and Sophia Knight and Catuscia Palamidessi and Prakash Panangaden Epistemic Strategies and Games on Concurrent Processes . . . . . . . . . . 28:1--28:?? Udi Boker and Orna Kupferman Translating to Co--Büchi Made Tight, Unified, and Useful . . . . . . . . . . 29:1--29:?? Pavlos Peppas and Costas D. Koutras and Mary-Anne Williams Maps in Multiple Belief Change . . . . . 30:1--30:?? Arnaud Durand and Juha Kontinen Hierarchies in Dependence Logic . . . . 31:1--31:?? Ewa Madali\'nska-Bugaj and Linh Anh Nguyen A Generalized QSQR Evaluation Method for Horn Knowledge Bases . . . . . . . . . . 32:1--32:?? Steven Schockaert and Jeroen Janssen and Dirk Vermeir Fuzzy Equilibrium Logic: Declarative Problem Solving in Continuous Domains 33:1--33:?? Diego Figueira Decidability of Downward XPath . . . . . 34:1--34:??
Hariolf Betz and Thom Frühwirth Linear-Logic Based Analysis of Constraint Handling Rules with Disjunction . . . . . . . . . . . . . . 1:1--1:?? Markus Krötzsch and Sebastian Rudolph and Pascal Hitzler Complexities of Horn Description Logics 2:1--2:?? Xiaoping Chen and Jianmin Ji and Fangzhen Lin Computing Loops with at Most One External Support Rule . . . . . . . . . 3:1--3:?? Mathieu Baudet and Véronique Cortier and Stéphanie Delaune YAPA: a Generic Tool for Computing Intruder Knowledge . . . . . . . . . . . 4:1--4:?? Richard McKinley Proof Nets for Herbrand's Theorem . . . 5:1--5:?? Dominique Larchey-Wendling and Didier Galmiche Nondeterministic Phase Semantics and the Undecidability of Boolean BI . . . . . . 6:1--6:?? Marcello M. Bonsangue and Stefan Milius and Alexandra Silva Sound and Complete Axiomatizations of Coalgebraic Language Equivalence . . . . 7:1--7:??
Alexander Kartzow First-Order Logic on Higher-Order Nested Pushdown Trees . . . . . . . . . . . . . 8:1--8:?? Paul Gastin and Nathalie Sznajder Fair Synthesis for Asynchronous Distributed Systems . . . . . . . . . . 9:1--9:?? Paulo Shakarian and Matthias Broecheler and V. S. Subrahmanian and Cristian Molinaro Using Generalized Annotated Programs to Solve Social Network Diffusion Optimization Problems . . . . . . . . . 10:1--10:?? Mnacho Echenim and Nicolas Peltier Instantiation Schemes for Nested Theories . . . . . . . . . . . . . . . . 11:1--11:?? Gerardo I. Simari and John P. Dickerson and Amy Sliva and V. S. Subrahmanian Parallel Abductive Query Answering in Probabilistic Logic Programs . . . . . . 12:1--12:?? Roman Kontchakov and Yavor Nenov and Ian Pratt-Hartmann and Michael Zakharyaschev Topological Logics with Connectedness over Euclidean Spaces . . . . . . . . . 13:1--13:?? James Delgrande and Torsten Schaub and Hans Tompits and Stefan Woltran A Model-Theoretic Approach to Belief Change in Answer Set Programming . . . . 14:1--14:?? Martin Gebser and Torsten Schaub Tableau Calculi for Logic Programs under Answer Set Semantics . . . . . . . . . . 15:1--15:?? José Júlio Alferes and Matthias Knorr and Terrance Swift Query-Driven Procedures for Hybrid MKNF Knowledge Bases . . . . . . . . . . . . 16:1--16:??
Johan Wittocx and Marc Denecker and Maurice Bruynooghe Constraint Propagation for First-Order Logic and Inductive Definitions . . . . 17:1--17:?? M. Praveen Does Treewidth Help in Modal Satisfiability? . . . . . . . . . . . . 18:1--18:?? Tony Tan Graph Reachability and Pebble Automata over Infinite Alphabets . . . . . . . . 19:1--19:?? Olaf Beyersdorff and Nicola Galesi and Massimo Lauria Parameterized Complexity of DPLL Search Procedures . . . . . . . . . . . . . . . 20:1--20:?? Angelos Charalambidis and Konstantinos Handjopoulos and Panagiotis Rondogiannis and William W. Wadge Extensional Higher-Order Logic Programming . . . . . . . . . . . . . . 21:1--21:?? Elvira Albert and Samir Genaim and Abu Naser Masud On the Inference of Resource Usage Upper and Lower Bounds . . . . . . . . . . . . 22:1--22:?? Floor Sietsma and Krzysztof R. Apt Common Knowledge in Email Exchanges . . 23:1--23:?? Andreas Herzig and Jerome Lang and Pierre Marquis Propositional Update Operators Based on Formula/Literal Dependence . . . . . . . 24:1--24:??
Wojciech Kazana and Luc Segoufin Enumeration of monadic second-order queries on trees . . . . . . . . . . . . 25:1--25:?? Jónathan Heras and Thierry Coquand and Anders Mörtberg and Vincent Siles Computing persistent homology within Coq/SSReflect . . . . . . . . . . . . . 26:1--26:?? Ori Lahav and Arnon Avron A unified semantic framework for fully structural propositional sequent systems 27:1--27:?? Jose Gaintzarain and Paqui Lucio Logical foundations for more expressive declarative temporal logic programming languages . . . . . . . . . . . . . . . 28:1--28:?? Olivier Danvy and Ian Zerny Three syntactic theories for combinatory graph reduction . . . . . . . . . . . . 29:1--29:?? Manuel Bodirsky and H. Dugald Macpherson and Johan Thapper Constraint satisfaction tractability from semi-lattice operations on infinite sets . . . . . . . . . . . . . . . . . . 30:1--30:?? Jeroen Ketema and Jakob Grue Simonsen Least upper bounds on the size of confluence and Church--Rosser diagrams in term rewriting and $ \lambda $-calculus . . . . . . . . . . . . . . . 31:1--31:?? Florian Rabe and Kristina Sojakova Logical relations for a logical framework . . . . . . . . . . . . . . . 32:1--32:?? Taolue Chen and Marco Diciolla and Marta Kwiatkowska and Alexandru Mereacre Verification of linear duration properties over continuous-time Markov chains . . . . . . . . . . . . . . . . . 33:1--33:?? Roy Dyckhoff and Mehrnoosh Sadrzadeh and Julien Truffaut Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators . . . . . . . . . . . . . . . 34:1--34:??
Matthew S. Bauer A PSPACE-complete first-order fragment of computability logic . . . . . . . . . 1:1--1:?? Arnold Beckmann and Samuel R. Buss Improved witnessing and local improvement principles for second-order bounded arithmetic . . . . . . . . . . . 2:1--2:?? Filippo Bonchi and Marcello M. Bonsangue and Helle H. Hansen and Prakash Panangaden and Jan J. M. M. Rutten and Alexandra Silva Algebra-coalgebra duality in Brzozowski's minimization algorithm . . 3:1--3:?? David Fernández-Duque Non-finite axiomatizability of dynamic topological logic . . . . . . . . . . . 4:1--4:?? Roberto Bruttomesso and Silvio Ghilardi and Silvio Ranise Quantifier-free interpolation in combinations of equality interpolating theories . . . . . . . . . . . . . . . . 5:1--5:?? Albert Atserias and Anuj Dawar Degree lower bounds of tower-type for approximating formulas with parity quantifiers . . . . . . . . . . . . . . 6:1--6:?? Renate A. Schmidt and Dmitry Tishkovsky Using tableau to decide description logics with full role negation and identity . . . . . . . . . . . . . . . . 7:1--7:?? Tony Tan Extending two-variable logic on data trees with order on data values and its automata . . . . . . . . . . . . . . . . 8:1--8:?? Hubie Chen On the complexity of existential positive queries . . . . . . . . . . . . 9:1--9:?? Lan Zhang and Ullrich Hustadt and Clare Dixon A resolution calculus for the branching-time temporal logic CTL . . . 10:1--10:??
Vernon Asuncion and Yan Zhang and Yi Zhou Preferred First-Order Answer Set Programs . . . . . . . . . . . . . . . . 11:1--11:?? Tran Cao Son and Enrico Pontelli and Ngoc-Hieu Nguyen and Chiaki Sakama Formalizing Negotiations Using Logic Programming . . . . . . . . . . . . . . 12:1--12:?? Cindy Eisner and Dana Fisman and John Havlicek Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations . . . . . . . . . . . . . . . 13:1--13:?? Yuan Feng and Yuxin Deng and Mingsheng Ying Symbolic Bisimulation for Quantum Processes . . . . . . . . . . . . . . . 14:1--14:?? Benedikt Bollig and Paul Gastin and Benjamin Monmege and Marc Zeitoun Pebble Weighted Automata and Weighted Logics . . . . . . . . . . . . . . . . . 15:1--15:?? Krishnendu Chatterjee and Laurent Doyen Partial-Observation Stochastic Games: How to Win when Belief Fails . . . . . . 16:1--16:?? Arnold Beckmann and Pavel Pudlák and Neil Thapen Parity Games and Propositional Proofs 17:1--17:??
Cristian Molinaro and Amy Sliva and V. S. Subrahmanian Super-Solutions: Succinctly Representing Solutions in Abductive Annotated Probabilistic Temporal Logic . . . . . . 18:1--18:?? Nadia Creignou and Uwe Egly and Johannes Schmidt Complexity Classifications for Logic-Based Argumentation . . . . . . . 19:1--19:?? Markus Aschinger and Conrad Drescher and Georg Gottlob and Heribert Vollmer LoCo --- a Logic for Configuration Problems . . . . . . . . . . . . . . . . 20:1--20:?? Robert J. Simmons Structural Focalization . . . . . . . . 21:1--21:?? Mingsheng Ying and Yangjia Li and Nengkun Yu and Yuan Feng Model-Checking Linear-Time Properties of Quantum Systems . . . . . . . . . . . . 22:1--22:?? María Poza and César Domínguez and Jónathan Heras and Julio Rubio A Certified Reduction Strategy for Homological Image Processing . . . . . . 23:1--23:?? Arnaud Carayol and Axel Haddad and Olivier Serre Randomization in Automata on Infinite Trees . . . . . . . . . . . . . . . . . 24:1--24:?? Alessandro Artale and Roman Kontchakov and Vladislav Ryzhikov and Michael Zakharyaschev A Cookbook for Temporal Conceptual Data Modelling with Description Logics . . . 25:1--25:??
Stefan Göller and Anthony Widjaja Lin Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems . . . . . . . . . . . . . . . . 26:1--26:?? Udi Boker and Krishnendu Chatterjee and Thomas A. Henzinger and Orna Kupferman Temporal Specifications with Accumulative Values . . . . . . . . . . 27:1--27:?? Maciej Komosinski and Adam Kups and Dorota Leszczy\'nska-Jasion and Mariusz Urba\'nski Identifying Efficient Abductive Hypotheses Using Multicriteria Dominance Relation . . . . . . . . . . . . . . . . 28:1--28:?? Achille Frigeri and Liliana Pasquale and Paola Spoletini Fuzzy Time in Linear Temporal Logic . . 30:1--30:?? Gerhard Schellhorn and John Derrick and Heike Wehrheim A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures . . . . . . . . . . . . . . . 31:1--31:?? Fabrizio Riguzzi and Terrance Swift Terminating Evaluation of Logic Programs with Finite Three-Valued Models . . . . 32:1--32:?? Damiano Zanardini and Samir Genaim Inference of Field-Sensitive Reachability and Cyclicity . . . . . . . 33:1--33:?? Fabio Mogavero and Aniello Murano and Giuseppe Perelli and Moshe Y. Vardi Reasoning About Strategies: On the Model-Checking Problem . . . . . . . . . 34:1--34:?? Filippo Bonchi and Fabio Gadducci and Giacoma Valentina Monreale A General Theory of Barbs, Contexts, and Labels . . . . . . . . . . . . . . . . . 35:1--35:??
Shulamit Halamish and Orna Kupferman Minimizing Deterministic Lattice Automata . . . . . . . . . . . . . . . . 1:1--1:?? Silvia Crafa and Francesco Ranzato Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions . . . . . . . 2:1--2:?? Jia Tao and Giora Slutzki and Vasant Honavar A Conceptual Framework for Secrecy-preserving Reasoning in Knowledge Bases . . . . . . . . . . . . 3:1--3:?? M. Biscaia and D. Henriques and P. Mateus Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains . . . . . . . . . . . . . 4:1--4:?? Agata Ciabattoni and Ori Lahav and Lara Spendier and Anna Zamansky Taming Paraconsistent (and Other) Logics: an Algorithmic Approach . . . . 5:1--5:?? Guy Avni and Orna Kupferman Parameterized Weighted Containment . . . 6:1--6:?? Gaëlle Fontaine Why Is It Hard to Obtain a Dichotomy for Consistent Query Answering? . . . . . . 7:1--7:?? Mauro Ferrari and Camillo Fiorentini and Guido Fiorino An Evaluation-Driven Decision Procedure for G3i . . . . . . . . . . . . . . . . 8:1--8:?? Stefan Göller and Jean-Christoph Jung and Markus Lohrey The Complexity of Decomposing Modal and First-Order Theories . . . . . . . . . . 9:1--9:??
Jakob Grue Simonsen A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy . . . . . . . . . . . . . . . . 10:1--10:?? Anastasios Skarlatidis and Georgios Paliouras and Alexander Artikis and George A. Vouros Probabilistic Event Calculus for Event Recognition . . . . . . . . . . . . . . 11:1--11:?? Roberto Sebastiani and Silvia Tomasi Optimization Modulo Theories with Linear Rational Costs . . . . . . . . . . . . . 12:1--12:?? Jean-Pierre Jouannaud and Albert Rubio Normal Higher-Order Termination . . . . 13:1--13:?? Bertram Felgenhauer and Aart Middeldorp and Harald Zankl and Vincent Van Oostrom Layer Systems for Proving Confluence . . 14:1--14:?? Stéphane Demri and Morgan Deters Two-Variable Separation Logic and Its Inner Circle . . . . . . . . . . . . . . 15:1--15:?? Pierre Genev\`es and Nabil Laya\"\ida and Alan Schmitt and Nils Gesbert Efficiently Deciding $ \mu $-Calculus with Converse over Finite Trees . . . . 16:1--16:?? Eryk Kopczy\'nski and Tony Tan On the Variable Hierarchy of First-Order Spectra . . . . . . . . . . . . . . . . 17:1--17:?? Nicolai Kraus and Christian Sattler Higher Homotopies in a Hierarchy of Univalent Universes . . . . . . . . . . 18:1--18:??
Novak Novakovi\'c and Lutz Straßburger On the Power of Substitution in the Calculus of Structures . . . . . . . . . 19:1--19:?? Ranko Lazi\'c and Sylvain Schmitz Nonelementary Complexities for Branching VASS, MELL, and Extensions . . . . . . . 20:1--20:?? Christoph Berkholz and Andreas Krebs and Oleg Verbitsky Bounds for the Quantifier Depth in Finite-Variable Logics: Alternation Hierarchy . . . . . . . . . . . . . . . 21:1--21:?? Bettina Fazzinga and Sergio Flesca and Francesco Parisi On the Complexity of Probabilistic Abstract Argumentation Frameworks . . . 22:1--22:?? Peter Lefanu Lumsdaine and Michael A. Warren The Local Universes Model: an Overlooked Coherence Construction for Dependent Type Theories . . . . . . . . . . . . . 23:1--23:?? Marijn J. H. Heule and Stefan Szeider A SAT Approach to Clique-Width . . . . . 24:1--24:?? Massimo Benerecetti and Fabio Mogavero and Aniello Murano Reasoning About Substructures and Games 25:1--25:?? Andrea Asperti Computational Complexity Via Finite Types . . . . . . . . . . . . . . . . . 26:1--26:?? Christopher Hampson and Agi Kurucz Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting . . . . . 27:1--27:??
Yuval Filmus and Massimo Lauria and Mladen Miksa and Jakob Nordström and Marc Vinyals From Small Space to Small Width in Resolution . . . . . . . . . . . . . . . 28:1--28:?? Sjoerd Cranen and Maciej Gazda and Wieger Wesselink and Tim A. C. Willemse Abstraction in Fixpoint Logic . . . . . 29:1--29:?? Hitoshi Furusawa and Georg Struth Concurrent Dynamic Algebra . . . . . . . 30:1--30:?? Zhe Wang and Kewen Wang and Rodney Topor DL-Lite Ontology Revision Based on An Alternative Semantic Characterization 31:1--31:?? Daniel G. Schwartz Dynamic Reasoning Systems . . . . . . . 32:1--32:?? Enrico Marchioni and Michael Wooldridge Lukasiewicz Games: a Logic-Based Approach to Quantitative Strategic Interactions . . . . . . . . . . . . . . 33:1--33:?? Oliver Friedmann and Felix Klaedtke and Martin Lange Ramsey-Based Inclusion Checking for Visibly Pushdown Automata . . . . . . . 34:1--34:?? Simon Kramer Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer) . . . . . . . . . . 35:1--35:?? Arnaud Carayol and Axel Haddad and Olivier Serre Erratum for ``Randomization in Automata on Infinite Trees'' . . . . . . . . . . 36:1--36:??
André Platzer Differential Game Logic . . . . . . . . 1:1--1:?? Jakub Michaliszyn and Jan Otop and Emanuel Kiero\'nski On the Decidability of Elementary Modal Logics . . . . . . . . . . . . . . . . . 2:1--2:?? Rémy Chrétien and Véronique Cortier and Stéphanie Delaune From Security Protocols to Pushdown Automata . . . . . . . . . . . . . . . . 3:1--3:?? Serenella Cerrito and Amélie David and Valentin Goranko Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL+ . . . . . . . . . . 4:1--4:?? Florian Rabe Lax Theory Morphisms . . . . . . . . . . 5:1--5:?? K. Rustan M. Leino and Paqui Lucio An Assertional Proof of the Stability and Correctness of Natural Mergesort . . 6:1--6:22 Johannes K. Fichte and Stefan Szeider Backdoors to Normality for Disjunctive Logic Programs . . . . . . . . . . . . . 7:1--7:??
Michael Benedikt and Balder Ten Cate and Michael Vanden Boom Effective Interpolation and Preservation in Guarded Logics . . . . . . . . . . . 8:1--8:?? Paolo Liberatore Belief Merging by Examples . . . . . . . 9:1--9:?? Simone Bova and Robert Ganian and Stefan Szeider Model Checking Existential Logic on Partially Ordered Sets . . . . . . . . . 10:1--10:?? Elvira Albert and Antonio Flores-Montoya and Samir Genaim and Enrique Martin-Martin May-Happen-in-Parallel Analysis for Actor-Based Concurrency . . . . . . . . 11:1--11:?? Stephane Demri and Morgan Deters Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction . . . . . . . . . 12:1--12:?? Konstantinos Mamouras The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes . . . . . . . . . . . . . . . . 13:1--13:?? Michael Benedikt and Clemens Ley Limiting Until in Ordered Tree Query Languages . . . . . . . . . . . . . . . 14:1--14:??
Brijesh Dongol and Ian J. Hayes and Georg Struth Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency . . . 15:1--15:?? Ranko Lazi\'c and Joël Ouaknine and James Worrell Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete . . . . . . . . . . . 16:1--16:?? Agata Ciabattoni and Revantha Ramanayake Power and Limits of Structural Display Rules . . . . . . . . . . . . . . . . . 17:1--17:?? Wlodzimierz Drabent Correctness and Completeness of Logic Programs . . . . . . . . . . . . . . . . 18:1--18:?? Albert Atserias and Massimo Lauria and Jakob Nordström Narrow Proofs May Be Maximally Long . . 19:1--19:?? Nadia Creignou and Odile Papini and Stefan Rümmele and Stefan Woltran Belief Merging within Fragments of Propositional Logic . . . . . . . . . . 20:1--20:?? Adam Trybus Rational Region-Based Affine Logic of the Real Plane . . . . . . . . . . . . . 21:1--21:?? Lian Wen and Kewen Wang and Yi-Dong Shen and Fangzhen Lin A Model for Phase Transition of Random Answer-Set Programs . . . . . . . . . . 22:1--22:??
Rohit Chadha and Vincent Cheval and Stefan Ciobâca and Steve Kremer Automated Verification of Equivalence Properties of Cryptographic Protocols 23:1--23:?? Alessandro Facchini and Filip Murlak and Michal Skrzypczak Index Problems for Game Automata . . . . 24:1--24:?? Michael Elberfeld and Martin Grohe and Till Tantau Where First-Order and Monadic Second-Order Logic Coincide . . . . . . 25:1--25:?? Lorenzo Carlucci and Nicola Galesi and Massimo Lauria On the Proof Complexity of Paris--Harrington and Off-Diagonal Ramsey Tautologies . . . . . . . . . . . 26:1--26:?? Bart Bogaerts and Joost Vennekens and Marc Denecker On Well-Founded Set-Inductions and Locally Monotone Operators . . . . . . . 27:1--27:?? Hitoshi Furusawa and Georg Struth Taming Multirelations . . . . . . . . . 28:1--28:?? Kristina Sojakova The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory . . . . . . . . . . . . . . . . . 29:1--29:?? Aleksy Schubert and Pawel Urzyczyn and Daria Walukiewicz-Chrzaszcz How Hard Is Positive Quantification? . . 30:1--30:?? Witold Charatonik and Piotr Witkowski Two-Variable Logic with Counting and Trees . . . . . . . . . . . . . . . . . 31:1--31:?? Saguy Benaim and Michael Benedikt and Witold Charatonik and Emanuel Kiero\'nski and Rastislav Lenhardt and Filip Mazowiecki and James Worrell Complexity of Two-Variable Logic on Finite Trees . . . . . . . . . . . . . . 32:1--32:??
Martin Lück and Arne Meier and Irena Schindler Parametrised Complexity of Satisfiability in Temporal Logic . . . . 1:1--1:?? Petar Dapi\'c and Petar Markovi\'c and Barnaby Martin Quantified Constraint Satisfaction Problem on Semicomplete Digraphs . . . . 2:1--2:?? Kensuke Kojima and Atsushi Igarashi A Hoare Logic for GPU Kernels . . . . . 3:1--3:?? Davide Sangiorgi Equations, Contractions, and Unique Solutions . . . . . . . . . . . . . . . 4:1--4:?? Tom J. Ameloot and Bas Ketsman and Frank Neven and Daniel Zinn Datalog Queries Distributing over Components . . . . . . . . . . . . . . . 5:1--5:?? Adrian Haret and Stefan Rümmele and Stefan Woltran Merging in the Horn Fragment . . . . . . 6:1--6:?? Isabella Mastroeni and Damiano Zanardini Abstract Program Slicing: an Abstract Interpretation-Based Approach to Program Slicing . . . . . . . . . . . . . . . . 7:1--7:??
Szymon Chlebowski and Maciej Komosinski and Adam Kups Automated Generation of Erotetic Search Scenarios: Classification, Optimization, and Knowledge Extraction . . . . . . . . 8:1--8:?? Heng Zhang and Yan Zhang Expressiveness of Logic Programs under the General Stable Model Semantics . . . 9:1--9:?? Pablo Barceló and Pablo Muñoz Graph Logics with Rational Relations: The Role of Word Combinatorics . . . . . 10:1--10:?? Arnold Beckmann and Sam Buss The NP Search Problems of Frege and Extended Frege Proofs . . . . . . . . . 11:1--11:?? Przemyslaw Daca and Thomas A. Henzinger and Jan Kretínský and Tatjana Petrov Faster Statistical Model Checking for Unbounded Temporal Properties . . . . . 12:1--12:?? Jan Friso Groote and David N. Jansen and Jeroen J. A. Keiren and Anton J. Wijs An $ O(m \log n) $ Algorithm for Computing Stuttering Equivalence and Branching Bisimulation . . . . . . . . . 13:1--13:?? Carsten Fuhs and Cynthia Kop and Naoki Nishida Verifying Procedural Programs via Constrained Rewriting Induction . . . . 14:1--14:?? Che-Ping Su and Tuan-Fang Fan and Churn-Jung Liau Possibilistic Justification Logic: Reasoning About Justified Uncertain Beliefs . . . . . . . . . . . . . . . . 15:1--15:?? Denis Ponomaryov and Mikhail Soutchanski Progression of Decomposed Local-Effect Action Theories . . . . . . . . . . . . 16:1--16:?? Nicholas R. Radcliffe and Luis F. T. Moraes and Rakesh M. Verma Uniqueness of Normal Forms for Shallow Term Rewrite Systems . . . . . . . . . . 17:1--17:??
George Barmpalias and Douglas Cenzer and Christopher P. Porter The Probability of a Computable Output from a Random Oracle . . . . . . . . . . 18:1--18:?? André Platzer Differential Hybrid Games . . . . . . . 19:1--19:?? Nathanaël Fijalkow and Charles Paperman Monadic Second-Order Logic with Arbitrary Monadic Predicates . . . . . . 20:1--20:?? Ronald De Haan and Iyad Kanj and Stefan Szeider On the Parameterized Complexity of Finding Small Unsatisfiable Subsets of CNF Formulas and CSP Instances . . . . . 21:1--21:?? Davide Bresolin and Agi Kurucz and Emilio Muñoz-Velasco and Vladislav Ryzhikov and Guido Sciavicco and Michael Zakharyaschev Horn Fragments of the Halpern--Shoham Interval Temporal Logic . . . . . . . . 22:1--22:?? Manuel Bodirsky and Peter Jonsson and Trung Van Pham The Complexity of Phylogeny Constraint Satisfaction Problems . . . . . . . . . 23:1--23:?? Michael Blondin and Alain Finkel and Christoph Haase and Serge Haddad The Logical View on Continuous Petri Nets . . . . . . . . . . . . . . . . . . 24:1--24:?? Matthew Hague and Andrzej S. Murawski and C.-H. Luke Ong and Olivier Serre Collapsible Pushdown Automata and Recursion Schemes . . . . . . . . . . . 25:1--25:??
Sebastian Eberhard and Gabriel Ebner and Stefan Hetzl Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars . . 26:1--26:?? Shqiponja Ahmetaj and Diego Calvanese and Magdalena Ortiz and Mantas Simkus Managing Change in Graph-Structured Data Using Description Logics . . . . . . . . 27:1--27:?? Marco Calautti and Sergio Greco and Irina Trubitsyna Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols . . . . . . . . . . . . . . . . 28:1--28:?? Hubie Chen and Moritz Müller One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries 29:1--29:?? Andreas Krebs and Howard Straubing An Effective Characterization of the Alternation Hierarchy in Two-Variable Logic . . . . . . . . . . . . . . . . . 30:1--30:?? Krishnendu Chatterjee and Thomas A. Henzinger and Jan Otop Nested Weighted Automata . . . . . . . . 31:1--31:?? Pavel Naumov and Jia Tao Information Flow under Budget Constraints . . . . . . . . . . . . . . 32:1--32:?? Kord Eickmeyer and Michael Elberfeld and Frederik Harwath Succinctness of Order-Invariant Logics on Depth-Bounded Structures . . . . . . 33:1--33:??
Olaf Beyersdorff and Leroy Chew and Meena Mahajan and Anil Shukla Are Short Proofs Narrow? QBF Resolution Is Not So Simple . . . . . . . . . . . . 1:1--1:?? Miika Hannula and Juha Kontinen and Jonni Virtema and Heribert Vollmer Complexity of Propositional Logics in Team Semantic . . . . . . . . . . . . . 2:1--2:?? Steffen Van Bakel Characterisation of Normalisation Properties for $ \lambda \mu $ using Strict Negated Intersection Types . . . 3:1--3:?? Lutz Schröder and Yde Venema Completeness of Flat Coalgebraic Fixpoint Logics . . . . . . . . . . . . 4:1--4:?? Andrea Aler Tubella and Alessio Guglielmi Subatomic Proof Systems: Splittable Systems . . . . . . . . . . . . . . . . 5:1--5:?? Elliot Fairweather and Maribel Fernández Typed Nominal Rewriting . . . . . . . . 6:1--6:??
Wied Pakusa and Svenja Schalthöfer and Erkal Selman Definability of Cai--Fürer--Immerman Problems in Choiceless Polynomial Time 7:1--7:?? Emanuel Kiero\'nski and Lidia Tendera Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants 8:1--8:?? Pierre Lescanne Quantitative Aspects of Linear and Affine Closed Lambda Terms . . . . . . . 9:1--9:?? Daniel Neider and Shambwaditya Saha and P. Madhusudan Compositional Synthesis of Piece-Wise Functions by Learning Classifiers . . . 10:1--10:?? Agata Ciabattoni and Francesco A. Genco Hypersequents and Systems of Rules: Embeddings and Applications . . . . . . 11:1--11:?? Sebastian Binnewies and Zhiqiang Zhuang and Kewen Wang and Bela Stantic Syntax-Preserving Belief Change Operators for Logic Programs . . . . . . 12:1--12:?? Zhé Hóu and Ranald Clouston and Rajeev Goré and Alwen Tiu Modular Labelled Sequent Calculi for Abstract Separation Logics . . . . . . . 13:1--13:?? Frank Neven and Nicole Schweikardt and Frederic Servais and Tony Tan Finite-State Map-Reduce Computation and Relational Algebra Queries . . . . . . . 14:1--14:?? Benno Van Den Berg Path Categories and Propositional Identity Types . . . . . . . . . . . . . 15:1--15:??