Automated Reasoning

1. Front Matter

   PDF

2. Logical Frameworks and Combination of Systems

   1. Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus

      • Anders Schack-Nielsen, Carsten Schürmann

      Pages 1-14

   2. Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

      • Brigitte Pientka, Jana Dunfield

      Pages 15-21

   3. MCMT: A Model Checker Modulo Theories

      • Silvio Ghilardi, Silvio Ranise

      Pages 22-29

   4. On Hierarchical Reasoning in Combinations of Theories

      • Carsten Ihlemann, Viorica Sofronie-Stokkermans

      Pages 30-45

3. Description Logic I

   1. Global Caching for Coalgebraic Description Logics

      • Rajeev Goré, Clemens Kupke, Dirk Pattinson, Lutz Schröder

      Pages 46-60

   2. Tractable Extensions of the Description Logic \(\cal EL\) with Numerical Datatypes

      • Despoina Magka, Yevgeny Kazakov, Ian Horrocks

      Pages 61-75

4. Higher-Order Logic

   1. Analytic Tableaux for Higher-Order Logic with Choice

      • Julian Backes, Chad E. Brown

      Pages 76-90

   2. Monotonicity Inference for Higher-Order Formulas

      • Jasmin Christian Blanchette, Alexander Krauss

      Pages 91-106

   3. Sledgehammer: Judgement Day

      • Sascha Böhme, Tobias Nipkow

      Pages 107-121

5. Invited Talk

   1. Logic between Expressivity and Complexity

      • Johan van Benthem

      Pages 122-126

6. Verification

   1. Multi-Prover Verification of Floating-Point Programs

      • Ali Ayad, Claude Marché

      Pages 127-141

   2. Verifying Safety Properties with the TLA +  Proof System

      • Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz

      Pages 142-148

   3. MUNCH - Automated Reasoner for Sets and Multisets

      • Ruzica Piskac, Viktor Kuncak

      Pages 149-155

   4. A Slice-Based Decision Procedure for Type-Based Partial Orders

      • Elena Sherman, Brady J. Garvin, Matthew B. Dwyer

      Pages 156-170

   5. Hierarchical Reasoning for the Verification of Parametric Systems

      • Viorica Sofronie-Stokkermans

      Pages 171-187

7. First-Order Logic

   1. Interpolation and Symbol Elimination in Vampire

      • Kryštof Hoder, Laura Kovács, Andrei Voronkov

      Pages 188-195

   2. iProver-Eq: An Instantiation-Based Theorem Prover with Equality

      • Konstantin Korovin, Christoph Sticksel

      Pages 196-202

   3. Classical Logic with Partial Functions

      • Hans de Nivelle

      Pages 203-217

8. Non-Classical Logic

   1. Automated Reasoning for Relational Probabilistic Knowledge Representation

      • Christoph Beierle, Marc Finthammer, Gabriele Kern-Isberner, Matthias Thimm

      Pages 218-224

This volume contains the proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010). IJCAR 2010 was held during July 16-19 as part of the 2010 Federated Logic Conference, hosted by the School of Informatics at the University ofEdinburgh,Scotland. Support by the conference sponsors – EPSRC, NSF, Microsoft Research, Association for Symbolic Logic, CADE Inc. , Google, Hewlett-Packard, Intel – is gratefully acknowledged. IJCARisthepremierinternationaljointconferenceonalltopicsinautomated reasoning, including foundations, implementations, and applications. Previous IJCAR conferences were held at Siena (Italy) in 2001, Cork (Ireland) in 2004, Seattle (USA) in 2006, and Sydney (Australia) in 2008. IJCAR comprises s- eral leading conferences and workshops. In 2010, IJCAR was the fusion of the following events: –CADE: International Conference on Automated Deduction –FroCoS: International Symposium on Frontiers of Combining Systems –FTP: International Workshop on First-Order Theorem Proving – TABLEAUX: InternationalConferenceonAutomatedReasoningwith- alytic Tableaux and Related Methods There were 89 submissions (63 regular papers and 26 system descriptions) of which 40 were accepted (28 regular papers and 12 system descriptions). Each submission was assigned to at least three Program Committee members, who carefully reviewed the papers, with the help of 92 external referees. Afterwards, the submissions were discussed by the ProgramCommittee during two weeks by means of Andrei Voronkov’s EasyChair system. We want to thank Andrei very much for providing his system, which was very helpful for the management of the submissions and reviews and for the discussion of the Program Committee.

• analytic tableaux
• automated deduction
• automated reasoning
• computer aided verification
• datalog
• logic
• logic programming
• policy monitoring
• query languages
• rewriting techniques
• satisfiability testing
• temporal logic
• theorem proving
• verification

• RWTH Aachen, LuFG Informatik, Aachen, Germany

  Jürgen Giesl

• Department of Computer Science, Chalmers University of Technology, Gothenburg, Sweden

  Reiner Hähnle

Policies and ethics