LPAR21: Volume InformationLPAR21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning31 articles•522 pages•Published: May 4, 2017 PapersJeffrey Fischer and Rupak Majumdar 113  Tobias Gleißner, Alexander Steen and Christoph Benzmüller 1430  Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits and Armin Biere 3148  Laura Kovács and Andrei Voronkov 4964  Tobias Philipp and Adrián RebolaPardo 6584  Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk 85105  Ozan Kahramanogullari 106124  Thibault Gauthier, Cezary Kaliszyk and Josef Urban 125143  Hamza Bourbouh, PierreLoic Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai and Xavier Thirioux 144161  Josef Lindsberger, Alexander Maringele and Georg Moser 162170  Nicholas Hollingum and Bernhard Scholz 171180  Sabine Bauer and Martin Hofmann 181199  Dimas Melo Filho, Fred Freitas and Jens Otten 200211  Miika Hannula, Juha Kontinen and Sebastian Link 212226  Bart Bogaerts, Eugenia Ternovska and David Mitchell 227248  Florian Frohn and Jürgen Giesl 249268  Emmanuel Hainry and Romain Péchoux 269285  Yazid Boumarafi, Lakhdar Sais and Yakoub Salhi 286299  Rachid Echahed and Aude Maignan 300318  Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci and Francesco Santini 319337  Dmitry Mordvinov and Grigory Fedyukovich 338355  František Blahoudek, Alexandre DuretLutz, Mikuláš Klokočka, Mojmír Křetínský and Jan Strejček 356367  Temesghen Kahsai, Rody Kersten, Philipp Rümmer and Martin Schäf 368384  Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu and PierreYves Strub 385403  Matthias Baaz and Norbert Preining 404416  Agata Ciabattoni and Revantha Ramanayake 417434  Bjoern Lellmann, Carlos Olarte and Elaine Pimentel 435455  Nicola Gigante, Angelo Montanari and Mark Reynolds 456473  JeanPierre Jouannaud and PierreYves Strub 474489  Hira Syeda and Gerwin Klein 490508  Luís CruzFilipe and Peter SchneiderKamp 509522 
KeyphrasesA* proof search, ALC, algebra, automated complexity analysis, automated reasoning^{3}, automated theorem proving^{2}, axiomatization, basic feasible functionals, BBI, blocked clauses^{2}, Boolean Pythagorean Triples problem, bunched calculi, clause elimination, complexity, computational complexity, Confluent Rewrite Relations, connection method, Constrained Horn Clauses, constraint satisfaction, contextfree languages, continuationpassing style, Coq, cut elimination, deep inference, deep learning, Description Logic, distributive substructural logics, DRAT proofs, DunnMints calculi, educational logic software, evaluation strategies, firstorder logic^{2}, firstorder theory, formal proofs, graph reachability, graph rewriting, Gödel logic, Higherorder complexity, higherorder logic^{2}, HigherOrder Modal Logic, Horn Clause Solving, hypersequents, implication problem, inclusion dependency, independence, Independence atom, inductive invariant, infinite lists, interactive theorem proving, interpolation, interpretations, Isabelle/HOL, linear arithmetic, linear logic^{2}, linear nested sequents, Linear Temporal Logic, linearization, logic of bunched implications, logical frameworks, LTL, LTL to automata translation, machine learning, maximum independent set, MELL, Memory Management Unit, memory models, model checking, model expansion, modular systems, monadic fragment, multimodalities, nondeterminism, omegaautomata, Operating Systems, Overlapping Rewrite Systems, Parallel Rewriting, Partial Model Checking, Past Operators, Preprocessing, probabilistic programs, program analysis, program verification^{2}, proof assistant, proof automation, proof search, proof theory, propagators, propositional satisfiability, quantitative reasoning, Reasoner, relational logic, relational verification, Resolution Calculus, resource types, SAT, SAT solving, Semantical Embedding, semideterministic automata, semiring, separation logic, serious games, software model checking, solvers, soundness, Stateflow, structural rules, superposition, tableaux, term rewriting, theorem proving^{2}, Tractable classes, Translation Lookaside Buffer, type theory, Unbounded Model Checking, uniformity. 
