Cantitate/Preț
Produs
Total produse
Vezi coșul
Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010, Proceedings de Jürgen Giesl

Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010, Proceedings: Lecture Notes in Computer Science, cartea 6173

Editat de Jürgen Giesl, Reiner Hähnle
en Limba Engleză Paperback – 30 iun 2010

Ecosistemul raționamentului automat prezentat în acest volum este unul vast, integrând instrumente și biblioteci esențiale pentru verificarea formală și demonstrarea teoremelor, precum Beluga, MCMT (Model Checker Modulo Theories) și Sledgehammer. Găsim în această carte o sinteză riguroasă a fuziunii dintre patru evenimente majore din domeniu: CADE, FroCoS, FTP și TABLEAUX, ceea ce conferă lucrării o autoritate deosebită în literatura de specialitate. Considerăm că această abordare integrată oferă o perspectivă panoramică asupra logicii computaționale, de la fundamentările teoretice la implementările practice în sisteme de calcul complexe.

Editorul Jürgen Giesl, cunoscut pentru coordonarea lucrării Term Rewriting and Applications, continuă aici explorarea tehnicilor de rescriere și a sistemelor deductive, însă extinde contextul către intersecția dintre expresivitate și complexitate. Structura volumului urmează o progresie logică, debutând cu cadrele logice și combinarea sistemelor, trecând prin logica descrierii și logica de ordin superior, pentru a culmina cu aplicații critice în verificare. Secțiunile dedicate verificării programelor cu virgulă mobilă și sistemului de demonstrare TLA+ indică o orientare clară către fiabilitatea software-ului și validarea sistemelor parametrice. Observăm un echilibru între contribuțiile teoretice și descrierile de sistem, oferind cititorului nu doar demonstrații matematice, ci și detalii despre arhitectura uneltelor software actuale.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 63445 lei

Preț vechi: 79307 lei
-20%

Puncte Express: 952

Carte disponibilă

Livrare economică 06-20 mai

 Adaugă în coș

Wish list
Gift list
Am citit!
Adaugă în listă

Specificații

ISBN-13: 9783642142024
ISBN-10: 3642142028
Pagini: 546
Ilustrații: XII, 536 p.
Dimensiuni: 155 x 235 x 30 mm
Greutate: 0.82 kg
Ediția:2010
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Lecture Notes in Artificial Intelligence

Locul publicării:Berlin, Heidelberg, Germany

Public țintă

Research

De ce să citești această carte

Recomandăm acest volum cercetătorilor care doresc să înțeleagă convergența dintre diferitele ramuri ale raționamentului automat. Cititorul câștigă acces la metodologii avansate de verificare formală și la detalii tehnice despre implementarea model checkerelor moderne. Este o resursă esențială pentru a înțelege cum logica de ordin superior și sistemele de tipuri pot fi aplicate în securitatea software și în demonstrarea automată a teoremelor.

Descriere scurtă

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.

Cuprins

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