LPAR21 Volume Information LPAR21 Volume InformationPapersAuthors  Title  Pages  PDF 

Jeffrey Fischer and Rupak Majumdar  Programming by Composing Filters  113   Tobias Gleißner, Alexander Steen and Christoph Benzmüller  Theorem Provers For Every Normal Modal Logic  1430   Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits and Armin Biere  Blocked Clauses in FirstOrder Logic  3148   Laura Kovács and Andrei Voronkov  FirstOrder Interpolation and Interpolating Proof Systems  4964   Tobias Philipp and Adrián RebolaPardo  Towards a Semantics of Unsatisfiability Proofs with Inprocessing  6584   Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk  Deep Network Guided Proof Search  85105   Ozan Kahramanogullari  Deep Proof Search in MELL  106124   Thibault Gauthier, Cezary Kaliszyk and Josef Urban  TacticToe: Learning to Reason with HOL4 Tactics  125143   Hamza Bourbouh, PierreLoic Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai and Xavier Thirioux  Automated analysis of Stateflow models  144161   Josef Lindsberger, Alexander Maringele and Georg Moser  Quantified Boolean Formulas: Call the Plumber!  162170   Nicholas Hollingum and Bernhard Scholz  Cauliflower: a Solver Generator for ContextFree Language Reachability  171180   Sabine Bauer and Martin Hofmann  Decidable linear list constraints  181199   Dimas Melo Filho, Fred Freitas and Jens Otten  RACCOON: A Connection Reasoner for the Description Logic ALC  200211   Miika Hannula, Juha Kontinen and Sebastian Link  On the Interaction of Inclusion Dependencies with Independence Atoms  212226   Bart Bogaerts, Eugenia Ternovska and David Mitchell  Propagators and Solvers for the Algebra of Modular Systems  227248   Florian Frohn and Jürgen Giesl  Analyzing Runtime Complexity via Innermost Runtime Complexity  249268   Emmanuel Hainry and Romain Péchoux  Higher order interpretation for higher order complexity  269285   Yazid Boumarafi, Lakhdar Sais and Yakoub Salhi  From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes  286299   Rachid Echahed and Aude Maignan  Parallel Graph Rewriting with Overlapping Rules  300318   Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci and Francesco Santini  A Quantitative Partial ModelChecking Function and Its Optimisation  319337   Dmitry Mordvinov and Grigory Fedyukovich  Synchronizing Constrained Horn Clauses  338355   František Blahoudek, Alexandre DuretLutz, Mikuláš Klokočka, Mojmír Křetínský and Jan Strejček  Seminator: A Tool for SemiDeterminization of OmegaAutomata  356367   Temesghen Kahsai, Rody Kersten, Philipp Rümmer and Martin Schäf  Quantified Heap Invariants for ObjectOriented Programs  368384   Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu and PierreYves Strub  Proving uniformity and independence by selfcomposition and coupling  385403   Matthias Baaz and Norbert Preining  Gödel logics and the fully boxed fragment of LTL  404416   Agata Ciabattoni and Revantha Ramanayake  Bunched Hypersequent Calculi for Distributive Substructural Logics  417434   Bjoern Lellmann, Carlos Olarte and Elaine Pimentel  A uniform framework for substructural logics with modalities  435455   Nicola Gigante, Angelo Montanari and Mark Reynolds  A OnePass TreeShaped Tableau for LTL+Past  456473   JeanPierre Jouannaud and PierreYves Strub  Coq without Type Casts: A Complete Proof of Coq Modulo Theory  474489   Hira Syeda and Gerwin Klein  Reasoning about Translation Lookaside Buffers  490508   Luís CruzFilipe and Peter SchneiderKamp  Formally Proving the Boolean Pythagorean Triples Conjecture  509522  
KeyphrasesCount  Keyphrase 

3  automated reasoning  2  automated theorem proving, blocked clauses, first order logic, higher order logic, linear logic, program verification, theorem proving  1  a* proof search, alc, algebra, automated complexity analysis, axiomatization, basic feasible functionals, bbi, boolean pythagorean triples problem, bunched calculi, clause elimination, complexity, computational complexity, confluent rewrite relations, connection method, constrained horn clauses, constraint satisfaction, context free languages, continuation passing style, coq, cut elimination, deep inference, deep learning, description logic, distributive substructural logics, drat proofs, dunn mints calculi, educational logic software, evaluation strategies, first order theory, formal proofs, graph reachability, graph rewriting, gödel logic, higher order complexity, higher order 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 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, omega automata, operating systems, overlapping rewrite systems, parallel rewriting, partial model checking, past operators, preprocessing, probabilistic programs, program analysis, 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, semi deterministic automata, semiring, separation logic, serious games, software model checking, solvers, soundness, stateflow, structural rules, superposition, tableaux, term rewriting, tractable classes, translation lookaside buffer, type theory, unbounded model checking, uniformity 
