دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Andreas Distler, Muhammad Shah, Volker Sorge (auth.), James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe (eds.) سری: Lecture Notes in Computer Science 6824 : Lecture Notes in Artificial Intelligence ISBN (شابک) : 9783642226724, 9783642226731 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2011 تعداد صفحات: 322 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 4 مگابایت
کلمات کلیدی مربوط به کتاب ریاضیات رایانه ای هوشمند: هجدهمین همایش ، Calculemus 2011 و دهمین کنفرانس بین المللی ، MKM 2011 ، برترینورو ، ایتالیا ، 18 تا 23 ژوئیه 2011. مجموعه مقالات: هوش مصنوعی (شامل رباتیک)، کاربردهای سیستم های اطلاعاتی (شامل اینترنت)، مدیریت پایگاه داده، ذخیره و بازیابی اطلاعات، منطق ریاضی و زبان های رسمی، داده کاوی و کشف دانش
در صورت تبدیل فایل کتاب Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب ریاضیات رایانه ای هوشمند: هجدهمین همایش ، Calculemus 2011 و دهمین کنفرانس بین المللی ، MKM 2011 ، برترینورو ، ایتالیا ، 18 تا 23 ژوئیه 2011. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب مجموعه مقالات داوری مشترک سه رویداد بینالمللی، یعنی
هجدهمین سمپوزیوم ادغام محاسبات نمادین و استدلال مکانیزه،
Calculemus 2011، دهمین کنفرانس بینالمللی مدیریت دانش ریاضی،
MKM 2011، و یک آهنگ جدید در مورد سیستمها است. و توضیحات
پروژههایی که هم مباحث Calculemus و هم MKM را در بر میگیرد،
همگی در برتینورو، ایتالیا، در ژوئیه 2011 برگزار شدند.
همه 51 مورد ارسالی از طریق یک فرآیند بررسی دقیق انجام شدند.
در مجموع 15 مقاله به Calculemus ارسال شد که 9 مورد آن پذیرفته
شد. سیستمها و پروژهها در سال 2011 از بین 14 مقاله ارسالی 12
مقاله انتخاب شدند در حالی که MKM 2011 22 مقاله ارسالی دریافت
کرد که 9 مورد برای ارائه و انتشار پذیرفته شد. این رویدادها بر
استفاده از تکنیکهای هوش مصنوعی در محاسبات نمادین و استفاده
از محاسبات نمادین برای حل مشکلات هوش مصنوعی متمرکز بودند.
ترکیبی از سیستم های جبر کامپیوتری و سیستم های کسر خودکار؛ و
مدیریت دانش ریاضی به ترتیب.
This book constitutes the joint refereed proceedings of three
international events, namely the 18th Symposium on the
Integration of Symbolic Computation and Mechanized Reasoning,
Calculemus 2011, the 10th International Conference on
Mathematical Knowledge Management, MKM 2011, and a new track
on Systems and Projects descriptions that span both the
Calculemus and MKM topics, all held in Bertinoro, Italy, in
July 2011.
All 51 submissions passed through a rigorous review process.
A total of 15 papers were submitted to Calculemus, of which 9
were accepted. Systems and Projects track 2011 there have
been 12 papers selected out of 14 submissions while MKM 2011
received 22 submissions, of which 9 were accepted for
presentation and publication. The events focused on the use
of AI techniques within symbolic computation and the
application of symbolic computation to AI problem solving;
the combination of computer algebra systems and automated
deduction systems; and mathematical knowledge management,
respectively.
Front Matter....Pages -
Enumeration of AG-Groupoids....Pages 1-14
Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework....Pages 15-29
Incidence Simplicial Matrices Formalized in Coq/SSReflect....Pages 30-44
Proof Assistant Decision Procedures for Formalizing Origami....Pages 45-57
Using Theorema in the Formalization of Theoretical Economics....Pages 58-73
View of Computer Algebra Data from Coq....Pages 74-89
Computer Certified Efficient Exact Reals in Coq ....Pages 90-106
A Foundational View on Integration Problems....Pages 107-122
Efficient Formal Verification of Bounds of Linear Programs....Pages 123-132
Large Formal Wikis: Issues and Solutions....Pages 133-148
Licensing the Mizar Mathematical Library....Pages 149-163
Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics....Pages 164-179
Parsing and Disambiguation of Symbolic Mathematics in the Naproche System....Pages 180-195
Interleaving Strategies....Pages 196-211
Combining Source, Content, Presentation, Narration, and Relational Representation....Pages 212-227
Indexing and Searching Mathematics in Digital Libraries....Pages 228-243
Isabelle as Document-Oriented Proof Assistant....Pages 244-259
Towards Formal Proof Script Refactoring....Pages 260-275
mizar-items : Exploring Fine-Grained Dependencies in the Mizar Mathematical Library....Pages 276-277
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita....Pages 278-280
Project EuDML – A First Year Demonstration....Pages 281-284
A Symbolic Companion for Interactive Geometric Systems....Pages 285-286
MathScheme: Project Description....Pages 287-288
Project Abstract: Logic Atlas and Integrator (LATIN)....Pages 289-291
The LaTeXML Daemon: Editable Math on the Collaborative Web....Pages 292-294
A System for Computing and Reasoning in Algebraic Topology....Pages 295-297
Learning2Reason....Pages 298-300
A Formal ization of the C99 Standard in HOL, Isabelle and Coq....Pages 301-303
Krextor - An Extensible Framework for Contributing Content Math to the Web of Data....Pages 304-306
System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org....Pages 307-309
Back Matter....Pages -