 | From the Series از مجموعه : -
Produced by تهيه كننده : Microsoft Research
Date تاريخ : 2004-10-06
Toolkit for Construction and Maintenance of Extensible Proof Search Tacticsdownload دانلود ,ويدئو و اسلايد Video & Slide , از گروه Computer Sience & Engineering كامپيوتر و مهندسی كتابخانه اينترنتي دانش گستران جوان You Research Description توضيح : Theorem provers for higher-order logics often use tactics to implement automated proof search. Often some basic tactics are designed to behave very differently in different contexts. As new axioms, definitions and theorems are added to the system, such tactics may need to be dynamically updated. In a logical framework with multiple (perhaps conflicting) logics, this has the added complexity that definitions and theorems should only be used for automation only in the logic in which they are defined or proved.
In my talk I will describe a very general and flexible mechanism for extensible hierarchical tactic construction and maintenance in a logical framework. I will also provide an overview of how this reflective mechanism can be implemented efficiently while requiring little effort from its users.
The approaches presented form the core of the tactic construction methodology in the MetaPRL theorem prover, where they have been developed and successfully used for several years. These mechanisms turned out to be very helpful not only in developing automated and interactive proof search techniques, but also in other applications, including development of a reliable extensible compiler.
Related Links لينك‌های مرتبط : -
Toolkit for Construction and Maintenance of Extensible Proof Search Tacticsdownload دانلود ,ويدئو و اسلايد Video & Slide , از گروه Computer Sience & Engineering كامپيوتر و مهندسی كتابخانه اينترنتي دانش گستران جوان You Research Speaker(s) اجرا : Aleksey Nogin, postdoc, California Institute of Technology
Runtime مدت زمان : 01:03:41
Video Size حجم ويدئو : 71 MB
Number of Slides تعداد اسلايد‌ها : 21 (2 MB)
Toolkit for Construction and Maintenance of Extensible Proof Search Tacticsdownload دانلود ,ويدئو و اسلايد Video & Slide , از گروه Computer Sience & Engineering كامپيوتر و مهندسی كتابخانه اينترنتي دانش گستران جوان You Research
|
