Last update:
Wed Oct 18 11:14:12 MDT 2023
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:??
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:??