LPAR-21 Volume Information
Volume:Thomas Eiter and David Sands (editors)
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning

LPAR-21 Volume Information

Title:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Editors:Thomas Eiter and David Sands
Series:EPiC Series in Computing
Volume:46
Publication date:May 4, 2017

Papers

AuthorsTitlePagesPDF
Jeffrey Fischer and Rupak MajumdarProgramming by Composing Filters1-13
Tobias Gleißner, Alexander Steen and Christoph BenzmüllerTheorem Provers For Every Normal Modal Logic14-30
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits and Armin BiereBlocked Clauses in First-Order Logic31-48
Laura Kovács and Andrei VoronkovFirst-Order Interpolation and Interpolating Proof Systems49-64
Tobias Philipp and Adrián Rebola-PardoTowards a Semantics of Unsatisfiability Proofs with Inprocessing65-84
Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary KaliszykDeep Network Guided Proof Search85-105
Ozan KahramanogullariDeep Proof Search in MELL106-124
Thibault Gauthier, Cezary Kaliszyk and Josef UrbanTacticToe: Learning to Reason with HOL4 Tactics125-143
Hamza Bourbouh, Pierre-Loic Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai and Xavier ThiriouxAutomated analysis of Stateflow models144-161
Josef Lindsberger, Alexander Maringele and Georg MoserQuantified Boolean Formulas: Call the Plumber!162-170
Nicholas Hollingum and Bernhard ScholzCauliflower: a Solver Generator for Context-Free Language Reachability171-180
Sabine Bauer and Martin HofmannDecidable linear list constraints181-199
Dimas Melo Filho, Fred Freitas and Jens OttenRACCOON: A Connection Reasoner for the Description Logic ALC200-211
Miika Hannula, Juha Kontinen and Sebastian LinkOn the Interaction of Inclusion Dependencies with Independence Atoms212-226
Bart Bogaerts, Eugenia Ternovska and David MitchellPropagators and Solvers for the Algebra of Modular Systems227-248
Florian Frohn and Jürgen GieslAnalyzing Runtime Complexity via Innermost Runtime Complexity249-268
Emmanuel Hainry and Romain PéchouxHigher order interpretation for higher order complexity269-285
Yazid Boumarafi, Lakhdar Sais and Yakoub SalhiFrom SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes286-299
Rachid Echahed and Aude MaignanParallel Graph Rewriting with Overlapping Rules300-318
Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci and Francesco SantiniA Quantitative Partial Model-Checking Function and Its Optimisation319-337
Dmitry Mordvinov and Grigory FedyukovichSynchronizing Constrained Horn Clauses338-355
František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský and Jan StrejčekSeminator: A Tool for Semi-Determinization of Omega-Automata356-367
Temesghen Kahsai, Rody Kersten, Philipp Rümmer and Martin SchäfQuantified Heap Invariants for Object-Oriented Programs368-384
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu and Pierre-Yves StrubProving uniformity and independence by self-composition and coupling385-403
Matthias Baaz and Norbert PreiningGödel logics and the fully boxed fragment of LTL404-416
Agata Ciabattoni and Revantha RamanayakeBunched Hypersequent Calculi for Distributive Substructural Logics417-434
Bjoern Lellmann, Carlos Olarte and Elaine PimentelA uniform framework for substructural logics with modalities435-455
Nicola Gigante, Angelo Montanari and Mark ReynoldsA One-Pass Tree-Shaped Tableau for LTL+Past456-473
Jean-Pierre Jouannaud and Pierre-Yves StrubCoq without Type Casts: A Complete Proof of Coq Modulo Theory474-489
Hira Syeda and Gerwin KleinReasoning about Translation Lookaside Buffers490-508
Luís Cruz-Filipe and Peter Schneider-KampFormally Proving the Boolean Pythagorean Triples Conjecture509-522

Keyphrases

CountKeyphrase
3automated reasoning
2automated theorem proving, blocked clauses, first order logic, higher order logic, linear logic, program verification, theorem proving
1a* 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