Accepted Papers
Full Papers
- Linear Quantifier Elimination
Tobias Nipkow
- The Logical Difference Problem for Description Logic Terminologies
Boris Konev, Dirk Walther and Frank Wolter
- MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance
Josef Urban, Geoff Sutcliffe, Petr Pudlák and Jiri Vyskocil
- Unification and Matching Modulo Leaf-Permutative Equational Presentations
Thierry Boy de la Tour, Mnacho Echenim and Paliath Narendran
- Quantitative Separation Logic and Programs with Lists
Radu Iosif, Marius Bozga and Swann Perarnau
- Focusing in Linear Meta-logic
Vivek Nigam and Dale Miller
- THF0 - The Core TPTP Language for Classical Higher-Order Logic
Christoph Benzmueller, Florian Rabe and Geoff Sutcliffe
- Individual Reuse in Description Logic Reasoning
Boris Motik and Ian Horrocks
- Automata-based Axiom Pinpointing
Franz Baader and Rafael Penaloza
- Certifying a Tree Automata Completion Checker
Benoit Boyer, Thomas Genet and Thomas Jensen
- Automated Complexity Analysis Based on the Dependency Pair Method
Nao Hirokawa and Georg Moser
- Modularity of Confluence, Constructed
Vincent van Oostrom
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
Mark Kaminski and Gert Smolka
- Preservation of Proof Obligations from Java to the Java Virtual Machine
Gilles Barthe, Benjamin Gregoire and mariela pavlova
- On Automating the Calculus of Relations
Peter Höfner and Georg Struth
- Efficient Well-definedness Checking
Adam Darvas, Farhad Mehta and Arsenii Rudich
- Proof Systems for Effectively Propositional Logic
Juan Antonio Navarro Perez and Andrei Voronkov
- Deciding EPR using DPLL and Substitution Sets
Leonardo de Moura and Nikolaj Bjorner
- On Integrating Saturation and DPLL(T) Proof Procedures.
Leonardo de Moura and Nikolaj Bjorner
- Automated Induction with Constrained Tree Automata
Adel bouhoula and Florent Jacquemard
- Proving Bounds on Real-valued Functions with Computations
Guillaume Melquiond
- Towards SMT Model Checking of Array-based Systems
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise and Daniele Zucchelli
- Proving Group Protocols Secure Against Eavesdroppers
Steve Kremer, Antoine Mercier and Ralf Treinen
- Canonical Inference for Implicational Systems
Maria Paola Bonacina and Nachum Dershowitz
- A General Tableau Approach for Deciding Modal Logics, Description Logics and Related First-Order Fragments
Renate Schmidt and Dmitry Tishkovsky
- Labelled Splitting
Arnaud Fietzke and Christoph Weidenbach
System Descriptions
- System Description: Aligator: A Mathematica Package for Invariant Generation
Laura Kovacs
- System Description: Abella - A System for Reasoning about Computations
Andrew Gacek
- System Description: LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic
Christoph Benzmueller, Lawrence Paulson, Frank Theiss and Arnaud Fietzke
- System Description: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems
Andre Platzer and Jan-David Quesel
- System Description: iProver - An Instantiation-based Theorem Prover for First-order Logic
Konstantin Korovin
- System Description: An Experimental Evaluation of Global Caching for ALC
Rajeev Gore and Linda Postniece
- System Description: Multi-Completion with Termination Tools
Haruhiko Sato, Sarah Winkler, Masahito Kurihara and Aart Middeldorp
- System Description: MTT: The Maude Termination Tool
Francisco Duran, Salvador Lucas and Jose Meseguer
- System Description: CELF - A Logical Framework for Deductive and Concurrent Systems
Anders Schack-Nielsen and Carsten Schürmann
- System Description: Automated Implicit Computational Complexity Analysis
Martin Avanzini, Georg Moser and Andreas Schnabl
- System Description: leanCoP 2.0 and ileanCoP 1.2
Jens Otten
- System Description: LogAnswer - A Deduction-Based Question Answering System
Ulrich Furbach, Ingo Glöckner, Hermann Helbig and Björn Pelzer
- System Description: A High-level Implementation of a System for Automated Reasoning with Default Rules
Christoph Beierle, Gabriele Kern-Isberner and Nicole Koch