دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: [1 ed.] نویسندگان: Koen Claessen (auth.), Nikolaj Bjørner, Viorica Sofronie-Stokkermans (eds.) سری: Lecture Notes in Computer Science 6803 Lecture Notes in Artificial Intelligence ISBN (شابک) : 3642224377, 9783642224379 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2011 تعداد صفحات: 508 [523] زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 5 Mb
در صورت تبدیل فایل کتاب Automated Deduction – CADE-23: 23rd International Conference on Automated Deduction, Wrocław, Poland, July 31 - August 5, 2011. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب کسر خودکار – CADE-23: بیست و سومین کنفرانس بین المللی کسر خودکار، وروتسواو، لهستان، 31 ژوئیه تا 5 آگوست 2011. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب مجموعه مقالات داوری بیست و سومین کنفرانس بینالمللی کسر خودکار، CADE-23 است که در وروتسواو، لهستان، در ژوئیه/آگوست 2011 برگزار شد. علاوه بر این، چهار سخنرانی دعوت شده توسط کارشناسان برجسته در این منطقه شامل شد. از جمله موضوعات مورد بحث، سیستم ها و ابزارهایی برای استدلال خودکار، منطق های بازنویسی، تأیید پروتکل امنیتی، یکسان سازی، اثبات قضیه، حذف بند، SAT، رضایت پذیری، اثبات قضیه تعاملی، استدلال نظریه، تجزیه و تحلیل ایستا، رویه های تصمیم گیری و غیره است.
This book constitutes the refereed proceedings of the 23rd International Conference on Automated Deduction, CADE-23, held in Wrocław, Poland, in July/August 2011. The 28 revised full papers and 7 system descriptions presented were carefully reviewed and selected from 80 submissions. Furthermore, four invited lectures by distinguished experts in the area were included. Among the topics addressed are systems and tools for automated reasoning, rewriting logics, security protocol verification, unification, theorem proving, clause elimination, SAT, satifiability, interactive theorem proving, theory reasoning, static analysis, decision procedures, etc.
Front Matter....Pages -
The Anatomy of Equinox – An Extensible Automated Reasoning Tool for First-Order Logic and Beyond....Pages 1-3
Advances in Proving Program Termination and Liveness....Pages 4-4
Translating between Language and Logic: What Is Easy and What Is Difficult....Pages 5-25
ASASP: Automated Symbolic Analysis of Security Policies....Pages 26-33
Backward Trace Slicing for Rewriting Logic Theories....Pages 34-48
Deciding Security for Protocols with Recursive Tests....Pages 49-63
The Matita Interactive Theorem Prover....Pages 64-69
Unification in the Description Logic $\mathcal{EL}$ without the Top Concept....Pages 70-84
Model Evolution with Equality Modulo Built-in Theories....Pages 85-100
Blocked Clause Elimination for QBF....Pages 101-115
Extending Sledgehammer with SMT Solvers....Pages 116-130
Automated Cyclic Entailment Proofs in Separation Logic....Pages 131-146
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems....Pages 147-161
Experimenting with Deduction Modulo....Pages 162-176
Heaps and Data Structures: A Challenge for Automated Provers....Pages 177-191
Optimized Query Rewriting for OWL 2 QL....Pages 192-206
Sort It Out with Monotonicity....Pages 207-221
Exploiting Symmetry in SMT Problems....Pages 222-236
Compression of Propositional Resolution Proofs via Partial Regularization....Pages 237-251
Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms....Pages 252-267
A Connection-Based Characterization of Bi-intuitionistic Validity....Pages 268-282
Automated Reasoning in $\mathcal{ALCQ}$ via SMT....Pages 283-298
Sine Qua Non for Large Theory Reasoning....Pages 299-314
Predicate Completion for non-Horn Clause Sets....Pages 315-330
System Description: SPASS-FD....Pages 331-337
Cutting to the Chase Solving Linear Integer Arithmetic....Pages 338-353
A Hybrid Method for Probabilistic Satisfiability....Pages 354-368
Solving Systems of Linear Inequalities by Bound Propagation....Pages 369-383
On Transfinite Knuth-Bendix Orders....Pages 384-399
Scala to the Power of Z3: Integrating SMT and Programming....Pages 400-406
Efficient General Unification for XOR with Homomorphism....Pages 407-421
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems....Pages 422-438
Static Analysis of Android Programs....Pages 439-445
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs....Pages 446-460
Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving....Pages 461-475
An Efficient Decision Procedure for Imperative Tree Data Structures....Pages 476-491
AC Completion with Termination Tools....Pages 492-498
CSI – A Confluence Tool....Pages 499-505
Back Matter....Pages -