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

by Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles

• ISBN13: 9783540710691
• ISBN10: 3540710698
• Format: Paperback
• Copyright: 2008-08-01
• Publisher: Springer Verlag

Summary

"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."--BOOK JACKET.

Table of Contents

Invited Talk
Software Verification: Roles and Challenges for Automatic Decision Procedures	p. 1
Specific Theories
Proving Bounds on Real-Valued Functions with Computations	p. 2
Linear Quantifier Elimination	p. 18
Quantitative Separation Logic and Programs with Lists	p. 34
On Automating the Calculus of Relations	p. 50
Automated Verification
Towards SMT Model Checking of Array-Based Systems	p. 67
Preservation of Proof Obligations from Java to the Java Virtual Machine	p. 83
Efficient Well-Definedness Checking	p. 100
Protocol Verification
Proving Group Protocols Secure Against Eavesdroppers	p. 116
System Descriptions 1
Automated Implicit Computational Complexity Analysis	p. 132
LogAnswer - A Deduction-Based Question Answering System	p. 139
A High-Level Implementation of a System for Automated Reasoning with Default Rules	p. 147
The Abella Interactive Theorem Prover	p. 154
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic	p. 162
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems	p. 171
Invited Talk
The Complexity of Conjunctive Query Answering in Expressive Description Logics	p. 179
Modal Logics
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments	p. 194
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse	p. 210
Herbrand Award Ceremony
Description Logics
Automata-Based Axiom Pinpointing	p. 226
Individual Reuse in Description Logic Reasoning	p. 242
The Logical Difference Problem for Description Logic Terminologies	p. 259
System Descriptions 2
Aligator: A Mathematica Package for Invariant Generation	p. 275
IeanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic	p. 283
iProver - An Instantiation-Based Theorem Prover for First-Order Logic	p. 292
An Experimental Evaluation of Global Caching for ALC	p. 299
Multi-completion with Termination Tools	p. 306
MTT: The Maude Termination Tool	p. 313
Celf - A Logical Framework for Deductive and Concurrent Systems	p. 320
Invited Talk
Canonicity!	p. 327
Equational Theories
Unification and Matching Modulo Leaf-Permutative Equational Presentations	p. 332
Modularity of Confluence: Constructed	p. 348
Automated Complexity Analysis Based on the Dependency Pair Method	p. 364
Canonical Inference for Implicational Systems	p. 380
Invited Talk
Challenges in the Automated Verification of Security Protocols	p. 396
Theorem Proving 1
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets	p. 410
Proof Systems for Effectively Propositional Logic	p. 426
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance	p. 441
CASC
CASC-J4 - The 4th IJCAR ATP System Competition	p. 457
Theorem Proving 2
Labelled Splitting	p. 459
Engineering DPLL(T) + Saturation	p. 475
THF0 - The Core of the TPTP Language for Higher-Order Logic	p. 491
Logical Frameworks
Focusing in Linear Meta-logic	p. 507
Tree Automata
Certifying a Tree Automata Completion Checker	p. 523
Automated Induction with Constrained Tree Automata	p. 539
Author Index	p. 555
Table of Contents provided by Ingram. All Rights Reserved.