Automated Reasoning

by Giesl, Jurgen; Hahnle, Reiner

• ISBN13: 9783642142024
• ISBN10: 3642142028
• Format: Paperback
• Copyright: 2010-07-30
• Publisher: Springer-Verlag New York Inc

Summary

This book constitutes the refereed proceedings of the 5th International Joint Conference on Automated Reasoning, IJCAR 2010, held in Edinburgh, UK, in July 2010 as part of the Federated Logic Conference, FLoC 2010.The 28 revised full research papers and 12 revised system descriptions presented together with 1 full paper and 2 abstracts of invited talks were carefully reviewed and selected from 63 full paper and 26 system description submissions. The papers address the entire spectrum of research in automated reasoning and are organized in topical sections on logical frameworks and combination of systems; description logic; higher-order logic; verification; first-order logic; non-classical logic; induction; decision procedures; arithmetic; applications; and termination.

Table of Contents

Logical Frameworks and Combination of Systems
Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus	p. 1
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)	p. 15
MCMT: A Model Checker Modulo Theories	p. 22
On Hierarchical Reasoning in Combinations of Theories	p. 30
Description Logic I
Global Caching for Coalgebraic Description Logics	p. 46
Tractable Extensions of the Description Logic $L with Numerical Datatypes	p. 61
Higher-Order Logic
Analytic Tableaux for Higher-Order Logic with Choice	p. 76
Monotonicity Inference for Higher-Order Formulas	p. 91
Sledgehammer: Judgement Day	p. 107
Invited Talk
Logic between Expressivity and Complexity	p. 122
Verification
Multi-Prover Verification of Floating-Point Programs	p. 127
Verifying Safety Properties with the TLA+ Proof System	p. 142
MUNCH - Automated Reasoner for Sets and Multisets	p. 149
A Slice-Based Decision Procedure for Type-Based Partial Orders	p. 156
Hierarchical Reasoning for the Verification of Parametric Systems	p. 171
First-Order Logic
Interpolation and Symbol Elimination in Vampire	p. 188
iProver-Eq: An Instantiation-Based Theorem Prover with Equality	p. 196
Classical Logic with Partial Functions	p. 203
Non-Classical Logic
Automated Reasoning for Relational Probabilistic Knowledge Representation	p. 218
Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse	p. 225
Terminating Tableaux for Hybrid Logic with Eventualities	p. 240
Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic	p. 255
Induction
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion	p. 263
Focused Inductive Theorem Proving	p. 278
Decision Procedures
A Decidable Class of Nested Iterated Schemata	p. 293
RegSTAB: A SAT Solver for Propositional Schemata	p. 309
Linear Quantifier Elimination as an Abstract Decision Procedure	p. 316
A Decision Procedure for CTL* Based on Tableaux and Automata	p. 331
URBiVA: Uniform Reduction to Bit-Vector Arithmetic	p. 346
Keynote Talk
Induction, Invariants, and Abstraction	p. 353
Arithmetic
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation	p. 354
Perfect Discrimination Graphs: Indexing Terms with Integer Exponents	p. 369
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic	p. 384
Invited Talk
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development	p. 400
Applications
Automating Security Analysis: Symbolic Equivalence of Constraint Systems	p. 412
System Description: The Proof Transformation System CERES	p. 427
Premise Selection in the Naproche System	p. 434
On the Saturation of YAGO	p. 441
Description Logic II
Optimized Description Logic Reasoning via Core Blocking	p. 457
An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ	p. 472
Termination
Decreasing Diagrams and Relative Termination	p. 487
Monotonicity Criteria for Polynomial Interpretations over the Naturals	p. 502
Termination Tools in Ordered Completion	p. 518
Author Index	p. 533
Table of Contents provided by Ingram. All Rights Reserved.