Automated Reasoning

Session 1: Invited Talk.- Software Verification: Roles and Challenges for Automatic Decision Procedures.- Session 2: Specific Theories.- Proving Bounds on Real-Valued Functions with Computations.- Linear Quantifier Elimination.- Quantitative Separation Logic and Programs with Lists.- On Automating the Calculus of Relations.- Session 3: Automated Verification.- Towards SMT Model Checking of Array-Based Systems.- Preservation of Proof Obligations from Java to the Java Virtual Machine.- Efficient Well-Definedness Checking.- Session 4: Protocol Verification.- Proving Group Protocols Secure Against Eavesdroppers.- Session 5: System Descriptions 1.- Automated Implicit Computational Complexity Analysis (System Description).- LogAnswer - A Deduction-Based Question Answering System (System Description).- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description).- The Abella Interactive Theorem Prover (System Description).- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).- The Complexity of Conjunctive Query Answering in Expressive Description Logics.- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments.- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse.- Session 8: Herbrand Award Ceremony.- Automata-Based Axiom Pinpointing.- Individual Reuse in Description Logic Reasoning.- The Logical Difference Problem for Description Logic Terminologies.- Session 10: System Descriptions 2.- Aligator: A Mathematica Package for Invariant Generation (System Description).- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions).- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description).- An Experimental Evaluation of Global Caching for (System Description).- Multi-completion with Termination Tools (System Description).- MTT: The Maude Termination Tool (System Description).- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description).- Canonicity!.- Unification and Matching Modulo Leaf-Permutative Equational Presentations.- Modularity of Confluence.- Automated Complexity Analysis Based on the Dependency Pair Method.- Canonical Inference for Implicational Systems.- Challenges in the Automated Verification of Security Protocols.- Session 14: Theorem Proving 1.- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.- Proof Systems for Effectively Propositional Logic.- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance.- CASC-J4 The 4th IJCAR ATP System Competition.- Session 16: Theorem Proving 2.- Labelled Splitting.- Engineering DPLL(T) + Saturation.- THF0 – The Core of the TPTP Language for Higher-Order Logic.- Focusing in Linear Meta-logic.- Certifying a Tree Automata Completion Checker.- Automated Induction with Constrained Tree Automata.