Automated Reasoning 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Giesl, Jürgen (Επιμελητής έκδοσης), Hähnle, Reiner (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2010.
• Σειρά: Lecture Notes in Computer Science, 6173
• Θέματα: Computer science.; Logic design.; Architecture, Computer.; Computer programming.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Artificial Intelligence (incl. Robotics).; Computer System Implementation.; Programming Techniques.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Logic Design.

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 confere...

Πίνακας περιεχομένων:

• 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
• Verification
• 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
• Induction
• 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
• Arithmetic
• 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
• Applications
• 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
• Termination
• Decreasing Diagrams and Relative Termination
• Monotonicity Criteria for Polynomial Interpretations over the Naturals
• Termination Tools in Ordered Completion.