Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney, Australia, August 12-15, 2008 Proceedings

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 -