Automated Reasoning [electronic resource] : 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010, Proceedings / edited by Jürgen Giesl, Reiner Hähnle.

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2010.
1 online resource (XII, 534 pages) : 85 illustrations
1st ed. 2010.
Computer Science (Springer-11645)
Lecture notes in computer science. Lecture notes in artificial intelligence 6173
Lecture Notes in Artificial Intelligence ; 6173
Contained In:
Springer eBooks

Location Notes Your Loan Policy


Artificial intelligence.
Computer architecture.
Computer programming.
Logic, Symbolic and mathematical.
Computer logic.
Logic design.
Local subjects:
Artificial Intelligence. (search)
Computer System Implementation. (search)
Programming Techniques. (search)
Mathematical Logic and Formal Languages. (search)
Logics and Meanings of Programs. (search)
Logic Design. (search)
System Details:
text file PDF
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 Incorporated , 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.
Logical Frameworks and Combination of Systems
Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
MCMT: A Model Checker Modulo Theories
On Hierarchical Reasoning in Combinations of Theories
Description Logic I
Global Caching for Coalgebraic Description Logics
Tractable Extensions of the Description Logic with Numerical Datatypes
Higher-Order Logic
Analytic Tableaux for Higher-Order Logic with Choice
Monotonicity Inference for Higher-Order Formulas
Sledgehammer: Judgement Day
Invited Talk
Logic between Expressivity and Complexity
Multi-Prover Verification of Floating-Point Programs
Verifying Safety Properties with the TLA?+? Proof System
MUNCH - Automated Reasoner for Sets and Multisets
A Slice-Based Decision Procedure for Type-Based Partial Orders
Hierarchical Reasoning for the Verification of Parametric Systems
First-Order Logic
Interpolation and Symbol Elimination in Vampire
iProver-Eq: An Instantiation-Based Theorem Prover with Equality
Classical Logic with Partial Functions
Non-Classical Logic
Automated Reasoning for Relational Probabilistic Knowledge Representation
Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
Terminating Tableaux for Hybrid Logic with Eventualities
Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion
Focused Inductive Theorem Proving
Decision Procedures
A Decidable Class of Nested Iterated Schemata
RegSTAB: A SAT Solver for Propositional Schemata
Linear Quantifier Elimination as an Abstract Decision Procedure
A Decision Procedure for CTL* Based on Tableaux and Automata
URBiVA: Uniform Reduction to Bit-Vector Arithmetic
Keynote Talk
Induction, Invariants, and Abstraction
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation
Perfect Discrimination Graphs: Indexing Terms with Integer Exponents
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
Invited Talk
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
Automating Security Analysis: Symbolic Equivalence of Constraint Systems
System Description: The Proof Transformation System CERES
Premise Selection in the Naproche System
On the Saturation of YAGO
Description Logic II
Optimized Description Logic Reasoning via Core Blocking
An Extension of Complex Role Inclusion Axioms in the Description Logic
Decreasing Diagrams and Relative Termination
Monotonicity Criteria for Polynomial Interpretations over the Naturals
Termination Tools in Ordered Completion.
Giesl, Jürgen. editor., Editor,
Hähnle, Reiner. editor., Editor,
SpringerLink (Online service)
Other format:
Printed edition:
Printed edition:
Publisher Number:
10.1007/978-3-642-14203-1 doi
Access Restriction:
Restricted for use by site license.