Last update: Wed Oct 18 11:14:12 MDT 2023
Volume 1, Number 1, July, 2000Lawrence 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:??
Miika Hannula Hierarchies in Inclusion Logic with Lax Semantics . . . . . . . . . . . . . . . 16:1--16:?? Valentin Goranko and Antti Kuusisto and Raine Rönnholm Game-Theoretic Semantics for Alternating-Time Temporal Logic . . . . 17:1--17:?? Dusan Guller Automated Deduction in Gödel Logic . . . 18:1--18:?? Alessandro Cimatti and Alberto Griggio and Ahmed Irfan and Marco Roveri and Roberto Sebastiani Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions . . . . . . . . . . . . . . . 19:1--19:?? Stéphane Le Roux and Arno Pauly and Jean-François Raskin Minkowski Games . . . . . . . . . . . . 20:1--20:?? Thomas Seiller Interaction Graphs: Non-Deterministic Automata . . . . . . . . . . . . . . . . 21:1--21:?? Daniel Gall and Thom Frühwirth An Operational Semantics for the Cognitive Architecture ACT-R and Its Translation to Constraint Handling Rules 22:1--22:?? Catalin Dima and Bastien Maubert and Sophie Pinchinat Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus . . . 23:1--23:??
Florian Rabe A Modular Type Reconstruction Algorithm 24:1--24:?? Masahiro Hamano Geometry of Interaction for MALL via Hughes--Van Glabbeek Proof-Nets . . . . 25:1--25:?? Xiaowei Huang and Ron Van Der Meyden An Epistemic Strategy Logic . . . . . . 26:1--26:?? Yongjian Li and Kaiqiang Duan and David N. Jansen and Jun Pang and Lijun Zhang and Yi Lv and Shaowei Cai An Automatic Proving Approach to Parameterized Verification . . . . . . . 27:1--27:?? Ebrahim Ardeshir-Larijani and Simon J. Gay and Rajagopal Nagarajan Automated Equivalence Checking of Concurrent Quantum Systems . . . . . . . 28:1--28:?? Michal Garlík and Leszek Aleksander Ko\lodziejczyk Some Subsystems of Constant-Depth Frege with Parity . . . . . . . . . . . . . . 29:1--29:?? Md. Aquil Khan and Vineeta Singh Patel A Simple Modal Logic for Reasoning in Multigranulation Rough Set Model . . . . 30:1--30:?? Elvira Albert and Jesús Correas and Einar Broch Johnsen and Ka I. Pun and Guillermo Román-Díez Parallel Cost Analysis . . . . . . . . . 31:1--31:??
Albert Atserias and Joanna Ochremiak Proof Complexity Meets Algebra . . . . . 1:1--1:?? Leonardo M. Cabrer and Benjamin Freisberg and George Metcalfe and Hilary A. Priestley Checking Admissibility Using Natural Dualities . . . . . . . . . . . . . . . 2:1--2:?? Jirí Adámek and Stefan Milius and Robert S. R. Myers and Henning Urbat Generalized Eilenberg Theorem: Varieties of Languages in a Category . . . . . . . 3:1--3:?? Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison 4:1--4:?? Giorgio Audrito and Mirko Viroli and Ferruccio Damiani and Danilo Pianini and Jacob Beal A Higher-Order Calculus of Computational Fields . . . . . . . . . . . . . . . . . 5:1--5:?? Jim Newton and Didier Verna A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams . . . . . . . . 6:1--6:??
Björn Lellmann and Elaine Pimentel Modularisation of Sequent Calculi for Normal and Non-normal Modalities . . . . 7:1--7:?? Micha\l Wrona The Complexity of Minimal Inference Problem for Conservative Constraint Languages . . . . . . . . . . . . . . . 8:1--8:?? Oleg Verbitsky and Maksim Zhukovskii Tight Bounds on the Asymptotic Descriptive Complexity of Subgraph Isomorphism . . . . . . . . . . . . . . 9:1--9:?? Nils Bulling and Wojciech Jamroga and Matei Popovici Reasoning about Strategic Abilities: Agents with Truly Perfect Recall . . . . 10:1--10:?? Karin Quaas and Mahsa Shirmohammadi Synchronizing Data Words for Register Automata . . . . . . . . . . . . . . . . 11:1--11:?? Nicola Leone and Marco Manna and Giorgio Terracina and Pierfrancesco Veltri Fast Query Answering over Existential Rules . . . . . . . . . . . . . . . . . 12:1--12:??
Ori Lahav and Yoni Zohar Pure Sequent Calculi: Analyticity and Decision Procedure . . . . . . . . . . . 13:1--13:?? Lorenzo Clemente and S\lawomir Lasota and Ranko Lazi\'c and Filip Mazowiecki Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems . . . . . . . . . . . . 14:1--14:?? Neha Lodha and Sebastian Ordyniak and Stefan Szeider A SAT Approach to Branchwidth . . . . . 15:1--15:?? Alex Klinkhamer and Ali Ebnenasir On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings . . . . . . . . . . . . . . . . . 16:1--16:?? Jérémie Chalopin and Victor Chepoi $1$-Safe Petri Nets and Special Cube Complexes: Equivalence and Applications 17:1--17:?? Gaetano Geck and Bas Ketsman and Frank Neven and Thomas Schwentick Parallel-Correctness and Containment for Conjunctive Queries with Union and Negation . . . . . . . . . . . . . . . . 18:1--18:??
Luca Bortolussi and Luca Cardelli and Marta Kwiatkowska and Luca Laurenti Central Limit Model Checking . . . . . . 19:1--19:?? Bahar Aameri and Michael Grüninger A Representation Theorem for Change through Composition of Activities . . . 20:1--20:?? Xiaowei Huang and Marta Kwiatkowska and Maciej Olejnik Reasoning about Cognitive Trust in Stochastic Multiagent Systems . . . . . 21:1--21:?? Ross Horne and Alwen Tiu and Bogdan Aman and Gabriel Ciobanu De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic . . . . . . . . . 22:1--22:?? Cláudia Nalon and Clare Dixon and Ullrich Hustadt Modal Resolution: Proofs, Layers, and Refinements . . . . . . . . . . . . . . 23:1--23:?? Willem Conradie and Sabine Frittella and Alessandra Palmigiano and Apostolos Tzimoulis and Nachoem Wijnberg Probabilistic Epistemic Updates on Algebras . . . . . . . . . . . . . . . . 24:1--24:?? Cristina Borralleras and Daniel Larraz and Enric Rodríguez-Carbonell and Albert Oliveras and Albert Rubio Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers 25:1--25:??
Rémy Chrétien and Véronique Cortier and Antoine Dallon and Stéphanie Delaune Typing Messages for Free in Security Protocols . . . . . . . . . . . . . . . 1:1--1:52 Gergei Bana and Rohit Chadha and Ajay Kumar Eeralla and Mitsuhiro Okada Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability 2:1--2:44 Tuan-Fang Fan and Churn-Jung Liau Reason-maintenance Belief Logic with Uncertain Information . . . . . . . . . 3:1--3:32 Silvio Ghilardi and Maria João Gouveia and Luigi Santocanale Fixed-point Elimination in the Intuitionistic Propositional Calculus 4:1--4:37 David Basin and Felix Klaedtke and Eugen Zalinescu Runtime Verification over Out-of-order Streams . . . . . . . . . . . . . . . . 5:1--5:43 Michael Benedikt and Pierre Bourhis and Georg Gottlob and Pierre Senellart Monadic Datalog, Tree Validity, and Limited Access Containment . . . . . . . 6:1--6:45 Lauri Hella and Antti Kuusisto and Arne Meier and Heribert Vollmer Satisfiability of Modal Inclusion Logic: Lax and Strict Semantics . . . . . . . . 7:1--7:18
Olaf Beyersdorff and Joshua Blinkhorn Dynamic QBF Dependencies in Reduction and Expansion . . . . . . . . . . . . . 8:1--8:27 Thomas Place and Marc Zeitoun Adding Successor: a Transfer Theorem for Separation and Covering . . . . . . . . 9:1--9:45 David Cerna and Temur Kutsia Idempotent Anti-unification . . . . . . 10:1--10:32 Kord Eickmeyer and Jan van den Heuvel and Ken-Ichi Kawarabayashi and Stephan Kreutzer and Patrice Ossona De Mendez and Micha\l Pilipczuk and Daniel A. Quiroz and Roman Rabinovich and Sebastian Siebertz Model-Checking on Ordered Structures . . 11:1--11:28 Shiguang Feng and Claudia Carapelle and Oliver Fernández Gil and Karin Quaas MTL and TPTL for One-Counter Machines: Expressiveness, Model Checking, and Satisfiability . . . . . . . . . . . . . 12:1--12:34 Manuel Montenegro and Susana Nieva and Ricardo Peña and Clara Segura Extending Liquid Types to Arrays . . . . 13:1--13:41 Philippe Balbiani and Joseph Boudou and Martín Diéguez and David Fernández-Duque Intuitionistic Linear Temporal Logics 14:1--14:32 Facundo Carreiro and Alessandro Facchini and Yde Venema and Fabio Zanasi The Power of the Weak . . . . . . . . . 15:1--15:47 S. Tomovi\'c and Z. Ognjanovi\'c and D. Doder A First-order Logic for Reasoning about Knowledge and Probability . . . . . . . 16:1--16:30
Frédéric Herbreteau and B. Srivathsan and Thanh-Tung Tran and Igor Walukiewicz Why Liveness for Timed Automata Is Hard, and What We Can Do About It . . . . . . 17:1--17:28 Guillaume Burel Linking Focusing and Resolution with Selection . . . . . . . . . . . . . . . 18:1--18:30 Mnacho Echenim and Radu Iosif and Nicolas Peltier The Bernays--Schönfinkel--Ramsey Class of Separation Logic with Uninterpreted Predicates . . . . . . . . . . . . . . . 19:1--19:46 André Hernich and Carsten Lutz and Fabio Papacchini and Frank Wolter Dichotomies in Ontology-Mediated Querying with the Guarded Fragment . . . 20:1--20:47 Arnaud Carayol and Olivier Serre How Good Is a Strategy in a Game with Nature? . . . . . . . . . . . . . . . . 21:1--21:39 Camillo Fiorentini and Mauro Ferrari Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic 22:1--22:47 Sergey Goncharov and Stefan Milius and Alexandra Silva Toward a Uniform Theory of Effectful State Machines . . . . . . . . . . . . . 23:1--23:63 Ana Cavalcanti and Robert M. Hierons and Sidney Nogueira Inputs and Outputs in CSP: a Model and a Testing Theory . . . . . . . . . . . . . 24:1--24:53 Andrew M. Pitts Typal Heterogeneous Equality Types . . . 25:1--25:10 Claudio Menghi and Marcello M. Bersani and Matteo Rossi and Pierluigi San Pietro Model Checking MITL Formulae on Timed Automata: a Logic-based Approach . . . . 26:1--26:44
Antoine Amarilli and Michael Benedikt Finite Open-world Query Answering with Number Restrictions . . . . . . . . . . 27:1--27:73 Jakub Gajarský and Petr Hlinený and Jan Obdrzálek and Daniel Lokshtanov and M. S. Ramanujan A New Perspective on FO Model Checking of Dense Graph Classes . . . . . . . . . 28:1--28:23 Jakub Gajarský and Stephan Kreutzer and Jaroslav NesETril and Patrice Ossona De Mendez and Micha\l Pilipczuk and Sebastian Siebertz and Szymon Toru\'nczyk First-Order Interpretations of Bounded Expansion Classes . . . . . . . . . . . 29:1--29:41 Franz Baader and Stefan Borgwardt and Patrick Koopmann and Ana Ozaki and Veronika Thost Metric Temporal Description Logics with Interval-Rigid Names . . . . . . . . . . 30:1--30:46 Liron Cohen and Reuben N. S. Rowe Non-well-founded Proof Theory of Transitive Closure Logic . . . . . . . . 31:1--31:31 Ron Van Der Meyden and Manas K. Patra Undecidable Cases of Model Checking Probabilistic Temporal--Epistemic Logic 32:1--32:26 Jori Bomanson and Tomi Janhunen and Ilkka Niemelä Applying Visible Strong Equivalence in Answer-Set Program Transformations . . . 33:1--33:41 Paolo Baldan and Tommaso Padoan Model Checking a Logic for True Concurrency . . . . . . . . . . . . . . 34:1--34:49
Katarina Britz and Giovanni Casini and Thomas Meyer and Kody Moodley and Uli Sattler and Ivan Varzinczak Principles of KLM-style Defeasible Description Logics . . . . . . . . . . . 1:1--1:46 Johannes Oetsch and Martina Seidl and Hans Tompits and Stefan Woltran Beyond Uniform Equivalence between Answer-set Programs . . . . . . . . . . 2:1--2:46 Adrien Koutsos Decidability of a Sound Set of Inference Rules for Computational Indistinguishability . . . . . . . . . . 3:1--3:44 Michele Basaldella $ \alpha \beta $-Relations and the Actual Meaning of $ \alpha $-Renaming 4:1--4:32 Raphaël Berthon and Bastien Maubert and Aniello Murano and Sasha Rubin and Moshe Y. Vardi Strategy Logic with Imperfect Information . . . . . . . . . . . . . . 5:1--5:51 Bart Bogaerts and Luís Cruz-Filipe Stratification in Approximation Fixpoint Theory and Its Application to Active Integrity Constraints . . . . . . . . . 6:1--6:19 Raphaël Berthon and Nathanaël Fijalkow and Emmanuel Filiot and Shibashis Guha and Bastien Maubert and Aniello Murano and Laureline Pinault and Sophie Pinchinat and Sasha Rubin and Olivier Serre Alternating Tree Automata with Qualitative Semantics . . . . . . . . . 7:1--7:24
Julian Gutierrez and Paul Harrenstein and Giuseppe Perelli and Michael Wooldridge Expressiveness and Nash Equilibrium in Iterated Boolean Games . . . . . . . . . 8:1--8:38 Bruno Lopes and Cláudia Nalon and Edward Hermann Haeusler Reasoning about Petri Nets: a Calculus Based on Resolution and Dynamic Logic 9:1--9:22 Stepan Kuznetsov Action Logic is Undecidable . . . . . . 10:1--10:26 Jan Krajícek Small Circuits and Dual Weak PHP in the Universal Theory of $p$-time Algorithms 11:1--11:4 Christopher H. Broadbent and Arnaud Carayol and C.-H. Luke Ong and Olivier Serre Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties . . . . . . . . . . . . . . . 12:1--12:37 Michael Benedikt and Pierre Bourhis and Balder Ten Cate and Gabrieled Puppis and Michael Vanden Boom Inference from Visible Information and Background Knowledge . . . . . . . . . . 13:1--13:69 Stéphane Demri and Etienne Lozes and Alessio Mansutti The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic . . . . . . . . . . . . . . . . . 14:1--14:56
Andrej Dudenhefner and Pawe\l Urzyczyn Kripke Semantics for Intersection Formulas . . . . . . . . . . . . . . . . 15:1--15:16 Christopher H. Broadbent and Arnaud Carayol and Matthew Hague and Andrzej S. Murawski and C.-H. Luke Ong and Olivier Serre Collapsible Pushdown Parity Games . . . 16:1--16:51 Kaya Deuser and Pavel Naumov Strategic Knowledge Acquisition . . . . 17:1--17:18 Simone Martini and Andrea Masini and Margherita Zorzi From $2$-Sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics . . . . . . . . . . . . . . 19:1--19:29 Agata Ciabattoni and Tim S. Lyon and Revantha Ramanayake and Alwen Tiu Display to Labeled Proofs and Back Again for Tense Logics . . . . . . . . . . . . 20:1--20:31
Marcelo Arenas and Pablo Barceló and Mikaël Monet The Complexity of Counting Problems Over Incomplete Databases . . . . . . . . . . 21:1--21:52 Pierre Ganty and Francesco Ranzato and Pedro Valero Complete Abstractions for Checking Language Inclusion . . . . . . . . . . . 22:1--22:40 Jirí Adámek and Liang-Ting Chen and Stefan Milius and Henning Urbat Reiterman's Theorem on Finite Algebras for a Monad . . . . . . . . . . . . . . 23:1--23:48 Peter Hertling and Gisela Krommes EXPSPACE-Completeness of the Logics K4 $ \times $ S5 and S4 $ \times $ S5 and the Logic of Subset Spaces . . . . . . . . . 24:1--24:71 Aleksandr Yu. Konovalov Generalized Realizability and Basic Logic . . . . . . . . . . . . . . . . . 25:1--25:23 Sam Buss and Dmitry Itsykson and Alexander Knop and Artur Riazanov and Dmitry Sokolov Lower Bounds on OBDD Proofs with Several Orders . . . . . . . . . . . . . . . . . 26:1--26:30
Sandra Kiefer and Pascal Schweitzer and Erkal Selman Graphs Identified by Logics with Counting . . . . . . . . . . . . . . . . 1:1--1:31 Ferruccio Guidi A Formal System for the Universal Quantification of Schematic Variables 2:1--2:37 Arnaud Durand and Juha Kontinen and Nicolas De Rugy-Altherre and Jouko Väänänen Tractability Frontier of Data Complexity in Team Semantics . . . . . . . . . . . 3:1--3:21 Fabio R. Gallo and Gerardo I. Simari and Maria Vanina Martinez and Natalia Abad Santos and Marcelo A. Falappa Local Belief Dynamics in Network Knowledge Bases . . . . . . . . . . . . 4:1--4:36 Gilles Barthe and Charlie Jacomme and Steve Kremer Universal Equivalence and Majority of Probabilistic Programs over Finite Fields . . . . . . . . . . . . . . . . . 5:1--5:42 Anuj Dawar and Gregory Wilsenach Symmetric Circuits for Rank Logic . . . 6:1--6:35 Manuel Bodirsky and Marcello Mamino and Caterina Viola Piecewise Linear Valued CSPs Solvable by Linear Programming Relaxation . . . . . 7:1--7:35
Tzanis Anevlavis and Matthew Philippe and Daniel Neider and Paulo Tabuada Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic . . . . . . . . . . . . . 8:1--8:39 Shaull Almagor and Dmitry Chistikov and Joël Ouaknine and James Worrell $O$-Minimal Invariants for Discrete-Time Dynamical Systems . . . . . . . . . . . 9:1--9:20 Philippe Balbiani and Hans van Ditmarsch and Saúl Fernández González Asynchronous Announcements . . . . . . . 10:1--10:38 Clemens Kupke and Dirk Pattinson and Lutz Schröder Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics 11:1--11:34 Moumanti Podder and Maksim Zhukovskii Zero--One Laws for Existential First-Order Sentences of Bounded Quantifier Depth . . . . . . . . . . . . 12:1--12:27 Erich Grädel and Richard Wilke Logics with Multiteam Semantics . . . . 13:1--13:30
Beno\^\it Larose and Barnaby Martin and Petar Markovi\'c and Daniël Paulusma and Siani Smith and Stanislav Zivný QCSP on Reflexive Tournaments . . . . . 14:1--14:22 Ilya Shapirovsky Satisfiability Problems on Sums of Kripke Frames . . . . . . . . . . . . . 15:1--15:25 Erfan Khaniki On Proof Complexity of Resolution over Polynomial Calculus . . . . . . . . . . 16:1--16:24 Fedor V. Fomin and Petr A. Golovach and Dimitrios M. Thilikos Parameterized Complexity of Elimination Distance to First-Order Logic Properties 17:1--17:35 Daniel Gratzer and Evan Cavallo and G. A. Kavvos and Adrien Guatto and Lars Birkedal Modalities and Parametric Adjoints . . . 18:1--18:29 Yuan Feng and Sanjiang Li and Mingsheng Ying Verification of Distributed Quantum Programs . . . . . . . . . . . . . . . . 19:1--19:40 Francesco Dagnino A Meta-theory for Big-step Semantics . . 20:1--20:50
Sebastian Enqvist and Valentin Goranko The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games . . . . . . . . . . . . . . . . . 21:1--21:?? Luca Aceto and Valentina Castiglioni and Wan Fokkink and Anna Ingólfsdóttir and Bas Luttik Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition? . . . . . . . . . 22:1--22:?? Jinsheng Chen and Giuseppe Greco and Alessandra Palmigiano and Apostolos Tzimoulis Syntactic Completeness of Proper Display Calculi . . . . . . . . . . . . . . . . 23:1--23:?? Adam Case and Christopher P. Porter The Intersection of Algorithmically Random Closed Sets and Effective Dimension . . . . . . . . . . . . . . . 24:1--24:?? Jason Z. S. Hu and Brigitte Pientka and Ulrich Schöpp A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types . . . . . . . . . . . . . . . . . 25:1--25:?? Chris Barrett and Alessio Guglielmi A Subatomic Proof System for Decision Trees . . . . . . . . . . . . . . . . . 26:1--26:?? Simon Doherty and Sadegh Dalvandi and Brijesh Dongol and Heike Wehrheim Unifying Operational Weak Memory Verification: an Axiomatic Approach . . 27:1--27:??
Christoph Matheja and Jens Pagel and Florian Zuleger A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions . . . . . . . . . 1:1--1:?? Md. Aquil Khan and Mohua Banerjee and Sibsankar Panda Logics for Temporal Information Systems in Rough Set Theory . . . . . . . . . . 2:1--2:?? Michael Blondin and Tim Leys and Filip Mazowiecki and Philip Offtermatt and Guillermo Pérez Continuous One-counter Automata . . . . 3:1--3:?? Dylan Bellier and Massimo Benerecetti and Dario Della Monica and Fabio Mogavero Good-for-Game QPTL: an Alternating Hodges Semantics . . . . . . . . . . . . 4:1--4:?? Catarina Carvalho and Florent Madelaine and Barnaby Martin and Dmitriy Zhuk The Complexity of Quantified Constraints: Collapsibility, Switchability, and the Algebraic Formulation . . . . . . . . . . . . . . 5:1--5:?? Martin Grohe and Daniel Neuen Canonisation and Definability for Graphs of Bounded Rank Width . . . . . . . . . 6:1--6:?? Petar Vukmirovi\'c and Jasmin Blanchette and Marijn J. H. Heule SAT-Inspired Eliminations for Superposition . . . . . . . . . . . . . 7:1--7:?? Yuval Filmus and Meena Mahajan and Gaurav Sood and Marc Vinyals MaxSAT Resolution and Subcube Sums . . . 8:1--8:?? Bahar Aameri and Michael Grüninger Reducible Theories and Amalgamations of Models . . . . . . . . . . . . . . . . . 9:1--9:??
Olaf Beyersdorff and Joshua Blinkhorn and Meena Mahajan and Tomás Peitl Hardness Characterisations and Size-width Lower Bounds for QBF Resolution . . . . . . . . . . . . . . . 10:1--10:?? Aleksandr Konovalov A Generalized Realizability and Intuitionistic Logic . . . . . . . . . . 11:1--11:?? Bartosz Bednarczyk and Stéphane Demri and Raul Fervari and Alessio Mansutti On Composing Finite Forests with Modal Logics . . . . . . . . . . . . . . . . . 12:1--12:?? Giuseppe Greco and Alessandra Palmigiano Linear Logic Properly Displayed . . . . 13:1--13:?? Yisong Wang and Thomas Eiter and Yuanlin Zhang and Fangzhen Lin Witnesses for Answer Sets of Logic Programs . . . . . . . . . . . . . . . . 15:1--15:?? Michael Benedikt and Stanislav Kikot and Piotr Ostropolski-Nalewaja and Miguel Romero On Monotonic Determinacy and Rewritability for Recursive Queries and Views . . . . . . . . . . . . . . . . . 16:1--16:?? James Baxter and Ana Cavalcanti and Maciej Gazda and Robert M. Hierons Testing using CSP Models: Time, Inputs, and Outputs . . . . . . . . . . . . . . 17:1--17:?? Theofanis Aravanis Generalizing Parikh's Criterion for Relevance-Sensitive Belief Revision . . 18:1--18:??
Tsubasa Takagi Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect . . . . . . . . . . . . . 19:1--19:?? Albert Atserias and Massimo Lauria Circular (Yet Sound) Proofs in Propositional Logic . . . . . . . . . . 20:1--20:?? Patricia Bouyer and Orna Kupferman and Nicolas Markey and Bastien Maubert and Aniello Murano and Giuseppe Perelli Reasoning about Quality and Fuzziness of Strategic Behaviors . . . . . . . . . . 21:1--21:?? Jan A. Bergstra and John V. Tucker Eager Equality for Rational Number Arithmetic . . . . . . . . . . . . . . . 22:1--22:?? Jacobo Torán and Florian Wörz Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas . . . . . . . 23:1--23:?? Laura Bozzelli and Angelo Montanari and Adriano Peron Interval Temporal Logic for Visibly Pushdown Systems . . . . . . . . . . . . 24:1--24:?? Isolde Adler and Polly Fahey Faster Property Testers in a Variation of the Bounded Degree Model . . . . . . 25:1--25:?? Yasir Mahmood and Arne Meier and Johannes Schmidt Parameterized Complexity of Logic-based Argumentation in Schaefer's Framework 26:1--26:?? Paolo Liberatore Mixed Iterated Revisions: Rationale, Algorithms, and Complexity . . . . . . . 27:1--27:??
Silvio Ghilardi and Alessandro Gianola and Deepak Kapur and Chiara Naso Interpolation Results for Arrays with Length and MaxDiff . . . . . . . . . . . 28:1--28:?? Anantha Padmanabha and R. Ramanujam A Decidable Fragment of First Order Modal Logic: Two Variable Term Modal Logic . . . . . . . . . . . . . . . . . 29:1--29:?? Nicole Schirrmacher and Sebastian Siebertz and Alexandre Vigny First-order Logic with Connectivity Operators . . . . . . . . . . . . . . . 30:1--30:?? Randal E. Bryant and Marijn J. H. Heule Generating Extended Resolution Proofs with a BDD-Based SAT Solver . . . . . . 31:1--31:?? Shaowei Cai and Bohan Li and Xindi Zhang Local Search For Satisfiability Modulo Integer Arithmetic Theories . . . . . . 32:1--32:?? Heba Aamer and Bart Bogaerts and Dimitri Surinx and Eugenia Ternovska and Jan Van den Bussche Inputs, Outputs, and Composition in the Logic of Information Flows . . . . . . . 33:1--33:?? Alessandro Artale and Jean Christoph Jung and Andrea Mazzullo and Ana Ozaki and Frank Wolter Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions . . . . . . 34:1--34:??