Automated Reasoning: 4th International Joint Conference, Ijcar 2008, Sydney, Nsw, Australia, August 12-15, 2008, Proceedings (lecture Notes In Computer Science)

Annotation This book constitutes the refereed proceedings of the 4th International Joint Conference on Automated Reasoning, IJCAR 2008, held in Sydney, Australia, in August 2008. The 26 revised full research papers and 13 revised system descriptions presented together with 4 invited papers and a summary of the CASC-J4 systems competition were carefully reviewed and selected from 80 full paper and 17 system description submissions. The papers address the entire spectrum of research in automated reasoning and are organized in topical sections on specific theories, automated verification, protocol verification, system descriptions, modal logics, description logics, equational theories, theorem proving, CASC, the 4th IJCAR ATP system competition, logical frameworks, and tree automata Front Matter....Pages - Software Verification: Roles and Challenges for Automatic Decision Procedures....Pages 1-1 Proving Bounds on Real-Valued Functions with Computations....Pages 2-17 Linear Quantifier Elimination....Pages 18-33 Quantitative Separation Logic and Programs with Lists....Pages 34-49 On Automating the Calculus of Relations....Pages 50-66 Towards SMT Model Checking of Array-Based Systems....Pages 67-82 Preservation of Proof Obligations from Java to the Java Virtual Machine....Pages 83-99 Efficient Well-Definedness Checking....Pages 100-115 Proving Group Protocols Secure Against Eavesdroppers....Pages 116-131 Automated Implicit Computational Complexity Analysis (System Description)....Pages 132-138 LogAnswer - A Deduction-Based Question Answering System (System Description)....Pages 139-146 A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description)....Pages 147-153 The Abella Interactive Theorem Prover (System Description)....Pages 154-161 LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)....Pages 162-170 KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)....Pages 171-178 The Complexity of Conjunctive Query Answering in Expressive Description Logics....Pages 179-193 A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments....Pages 194-209 Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse....Pages 210-225 Automata-Based Axiom Pinpointing....Pages 226-241 Individual Reuse in Description Logic Reasoning....Pages 242-258 The Logical Difference Problem for Description Logic Terminologies....Pages 259-274 Aligator: A Mathematica Package for Invariant Generation (System Description)....Pages 275-282 leanCoP 2.0 and ileanCoP 1.2 : High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)....Pages 283-291 iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)....Pages 292-298 An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description)....Pages 299-305 Multi-completion with Termination Tools (System Description)....Pages 306-312 MTT: The Maude Termination Tool (System Description)....Pages 313-319 Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)....Pages 320-326 Canonicity!....Pages 327-331 Unification and Matching Modulo Leaf-Permutative Equational Presentations....Pages 332-347 Modularity of Confluence....Pages 348-363 Automated Complexity Analysis Based on the Dependency Pair Method....Pages 364-379 Canonical Inference for Implicational Systems....Pages 380-395 Challenges in the Automated Verification of Security Protocols....Pages 396-409 Deciding Effectively Propositional Logic Using DPLL and Substitution Sets....Pages 410-425 Proof Systems for Effectively Propositional Logic....Pages 426-440 MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance....Pages 441-456 CASC-J4 The 4th IJCAR ATP System Competition....Pages 457-458 Labelled Splitting....Pages 459-474 Engineering DPLL(T) + Saturation....Pages 475-490 THF0 – The Core of the TPTP Language for Higher-Order Logic....Pages 491-506 Focusing in Linear Meta-logic....Pages 507-522 Certifying a Tree Automata Completion Checker....Pages 523-538 Automated Induction with Constrained Tree Automata....Pages 539-554 Back Matter....Pages -