LPAR-18 Accepted Papers

Grigoris Antoniou, Thomas Eiter and Kewen Wang. Forgetting for Defeasible Logic
Stefan Borgwardt and Barbara Morawska. Finding Finite Herbrand Models
Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner. The TPTP Typed First-order Form with Arithmetic
Dominik Klein and Nao Hirokawa. Confluence of Non-Left-Linear TRSs via Relative Termination
Friedrich Neurauter and Aart Middeldorp. On the Domain and Dimension Hierarchy of Matrix Interpretations
Martin Suda and Christoph Weidenbach. Labelled Superposition for PLTL
Stefan Hetzl, Alexander Leitsch and Daniel Weller. Towards Algorithmic Cut-Introduction
Francesca Scozzari and Gianluca Amato. Random: R-based Analyzer for Numerical DOMains
Jesse Alama, Daniel Kuehlwein and Josef Urban. Automated and Human Proofs in General Mathematics: An Initial Comparison
Andreas Morgenstern, Manuel Gesell and Klaus Schneider. Improving Accuracy of Runtime-Verification by the Temporal-Logic Hierarchy
Dulma Rodriguez and Martin Hofmann. Linear constraints over infinite trees.
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen and Amelie Stainer. Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina. Lazy Abstraction with Interpolants for Arrays
Franz Baader and Alexander Okhotin. Solving language equations and disequations with applications to disunification in description logics and
monadic set constraints
Stephan Merz and Hernán Vanzetto. Automatic verification of TLA+ proof obligations with SMT solvers
Ezequiel Orbe, Carlos Areces and Gabriel Infante-Lopez. iSat: Structure Visualization for SAT Problems
Arnaud Fietzke, Evgeny Kruglov and Christoph Weidenbach. Automatic Generation of  Inductive Invariants by SUP(LA)
Jakob Zwirchmayr, Laura Kovacs and Jens Knoop. r-TuBound: Loop Bounds for WCET Analysis (tool paper)
Sarah Winkler, Harald Zankl and Aart Middeldorp. Ordinals and Knuth-Bendix Orders
Leonid Libkin and Domagoj Vrgoc. Regular Expressions for Data Words
Beniamino Accattoli and Delia Kesner. The permutative lambda-calculus
Han The Anh, Ari Saptawijaya and Luís Moniz Pereira. Moral Reasoning Under Uncertainty
Lukas Bulwahn. Smart testing of functional programs in Isabelle
David Aspinall, Ewen Denney and Christoph Lüth. Querying Proofs
William Snell, Dirk Pattinson and Florian Widmann. Solving Graded/Probabilistic Modal Logic via Linear Inequalities (System Description)
Philipp Ruemmer. E-Matching with Free Variables
Amir Aavani, Xiongnan Newman Wu, Eugenia Ternovska and David Mitchell. Enfragmo:A System for Modelling and Solving Search Problems with Logic
Jose Luis Chacon and Ramon Pino Perez. Duality between merging operators and social contraction operators
Hadi Katebi, Karem A. Sakallah and Igor L. Markov. Conflict Anticipation in the Search for Graph Automorphisms
María Alpuente, Demis Ballis, Francisco Frechina and Daniel Romero. Backward Trace Slicing for Conditional Rewrite Theories
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Mikael H. Møller and Jiri Srba. Dual-Priced Modal Transition Systems with Time Durations
Boris Motik. Invited talk by Boris Motik
Aart Middeldorp. Invited talk by Aart Middeldorp
Kenneth McMillan. Invited talk by Kenneth McMillan
Elvira Albert. Invited talk by Elvira Albert