Abstract is missing.
- Software Verification: Roles and Challenges for Automatic Decision ProceduresAarti Gupta. 1 [doi]
- Proving Bounds on Real-Valued Functions with ComputationsGuillaume Melquiond. 2-17 [doi]
- Linear Quantifier EliminationTobias Nipkow. 18-33 [doi]
- Quantitative Separation Logic and Programs with ListsMarius Bozga, Radu Iosif, Swann Perarnau. 34-49 [doi]
- On Automating the Calculus of RelationsPeter Höfner, Georg Struth. 50-66 [doi]
- Towards SMT Model Checking of Array-Based SystemsSilvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. 67-82 [doi]
- Preservation of Proof Obligations from Java to the Java Virtual MachineGilles Barthe, Benjamin Grégoire, Mariela Pavlova. 83-99 [doi]
- Efficient Well-Definedness CheckingÁdám Darvas, Farhad Mehta, Arsenii Rudich. 100-115 [doi]
- Proving Group Protocols Secure Against EavesdroppersSteve Kremer, Antoine Mercier 0002, Ralf Treinen. 116-131 [doi]
- Automated Implicit Computational Complexity Analysis (System Description)Martin Avanzini, Georg Moser, Andreas Schnabl. 132-138 [doi]
- LogAnswer - A Deduction-Based Question Answering System (System Description)Ulrich Furbach, Ingo Glöckner, Hermann Helbig, Björn Pelzer. 139-146 [doi]
- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description)Christoph Beierle, Gabriele Kern-Isberner, Nicole Koch. 147-153 [doi]
- The Abella Interactive Theorem Prover (System Description)Andrew Gacek. 154-161 [doi]
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke. 162-170 [doi]
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)André Platzer, Jan-David Quesel. 171-178 [doi]
- The Complexity of Conjunctive Query Answering in Expressive Description LogicsCarsten Lutz. 179-193 [doi]
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order FragmentsRenate A. Schmidt, Dmitry Tishkovsky. 194-209 [doi]
- Terminating Tableaux for Hybrid Logic with the Difference Modality and ConverseMark Kaminski, Gert Smolka. 210-225 [doi]
- Automata-Based Axiom PinpointingFranz Baader, Rafael Peñaloza. 226-241 [doi]
- Individual Reuse in Description Logic ReasoningBoris Motik, Ian Horrocks. 242-258 [doi]
- The Logical Difference Problem for Description Logic TerminologiesBoris Konev, Dirk Walther, Frank Wolter. 259-274 [doi]
- Aligator: A Mathematica Package for Invariant Generation (System Description)Laura Kovács. 275-282 [doi]
- leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)Jens Otten. 283-291 [doi]
- iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description)Konstantin Korovin. 292-298 [doi]
- An Experimental Evaluation of Global Caching for (System Description)Rajeev Goré, Linda Postniece. 299-305 [doi]
- Multi-completion with Termination Tools (System Description)Haruhiko Sato, Sarah Winkler, Masahito Kurihara, Aart Middeldorp. 306-312 [doi]
- MTT: The Maude Termination Tool (System Description)Francisco Durán, Salvador Lucas, José Meseguer. 313-319 [doi]
- Celf - A Logical Framework for Deductive and Concurrent Systems (System Description)Anders Schack-Nielsen, Carsten Schürmann. 320-326 [doi]
- Canonicity!Nachum Dershowitz. 327-331 [doi]
- Unification and Matching Modulo Leaf-Permutative Equational PresentationsThierry Boy de la Tour, Mnacho Echenim, Paliath Narendran. 332-347 [doi]
- Modularity of ConfluenceVincent van Oostrom. 348-363 [doi]
- Automated Complexity Analysis Based on the Dependency Pair MethodNao Hirokawa, Georg Moser. 364-379 [doi]
- Canonical Inference for Implicational SystemsMaria Paola Bonacina, Nachum Dershowitz. 380-395 [doi]
- Challenges in the Automated Verification of Security ProtocolsHubert Comon-Lundh. 396-409 [doi]
- Deciding Effectively Propositional Logic Using DPLL and Substitution SetsLeonardo Mendonça de Moura, Nikolaj Bjørner. 410-425 [doi]
- Proof Systems for Effectively Propositional LogicJuan Antonio Navarro Pérez, Andrei Voronkov. 426-440 [doi]
- MaLARea SG1- Machine Learner for Automated Reasoning with Semantic GuidanceJosef Urban, Geoff Sutcliffe, Petr Pudlák, Jirí Vyskocil. 441-456 [doi]
- CASC-J4 The 4th IJCAR ATP System CompetitionGeoff Sutcliffe. 457-458 [doi]
- Labelled SplittingArnaud Fietzke, Christoph Weidenbach. 459-474 [doi]
- Engineering DPLL(T) + SaturationLeonardo Mendonça de Moura, Nikolaj Bjørner. 475-490 [doi]
- THF0 - The Core of the TPTP Language for Higher-Order LogicChristoph Benzmüller, Florian Rabe, Geoff Sutcliffe. 491-506 [doi]
- Focusing in Linear Meta-logicVivek Nigam, Dale Miller. 507-522 [doi]
- Certifying a Tree Automata Completion CheckerBenoît Boyer, Thomas Genet, Thomas P. Jensen. 523-538 [doi]
- Automated Induction with Constrained Tree AutomataAdel Bouhoula, Florent Jacquemard. 539-554 [doi]