Description 
1 online resource (xii, 534 pages) : illustrations 
Series 
Lecture notes in computer science, 03029743 ; 6173. Lecture notes in artificial intelligence 

LNCS sublibrary. SL 7, Artificial intelligence 

Lecture notes in computer science ; 6173. 03029743


Lecture notes in computer science. Lecture notes in artificial intelligence


LNCS sublibrary. SL 7, Artificial intelligence.

Contents 
Logical Frameworks and Combination of Systems  CurryStyle 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  HigherOrder Logic  Analytic Tableaux for HigherOrder Logic with Choice  Monotonicity Inference for HigherOrder Formulas  Sledgehammer: Judgement Day  Invited Talk  Logic between Expressivity and Complexity  Verification  MultiProver Verification of FloatingPoint Programs  Verifying Safety Properties with the TLA?+? Proof System  MUNCH  Automated Reasoner for Sets and Multisets  A SliceBased Decision Procedure for TypeBased Partial Orders  Hierarchical Reasoning for the Verification of Parametric Systems  FirstOrder Logic  Interpolation and Symbol Elimination in Vampire  iProverEq: An InstantiationBased Theorem Prover with Equality  Classical Logic with Partial Functions  NonClassical Logic  Automated Reasoning for Relational Probabilistic Knowledge Representation  Optimal and CutFree 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 SecondOrder 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 BitVector Arithmetic  Keynote Talk  Induction, Invariants, and Abstraction  Arithmetic  A SingleSignificantDigit Calculus for SemiAutomated Guesstimation  Perfect Discrimination Graphs: Indexing Terms with Integer Exponents  An Interpolating Sequent Calculus for QuantifierFree 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 
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; higherorder logic; verification; firstorder logic; nonclassical logic; induction; decision procedures; arithmetic; applications; and termination 
Analysis 
wiskunde 

mathematics 

ontwerp 

design 

computerwetenschappen 

computer sciences 

kunstmatige intelligentie 

artificial intelligence 

logica 

logic 

computerwiskunde 

computational mathematics 

Information and Communication Technology (General) 

Informatie en communicatietechnologie (algemeen) 
Bibliography 
Includes bibliographical references and author index 
Subject 
Automatic theorem proving  Congresses


Computer logic  Congresses


Artificial intelligence.


Logic.


Artificial Intelligence


Logic


artificial intelligence.


logic.


Informatique.


Logic.


Artificial intelligence.


Automatic theorem proving.


Computer logic.

Genre/Form 
Electronic books


Conference papers and proceedings.


Conference papers and proceedings.


Actes de congrès.

Form 
Electronic book

Author 
Giesl, Jürgen.


Hähnle, Reiner.

ISBN 
9783642142031 

3642142036 
