| ชื่อเรื่อง | : | Case-Analysis for Rippling and Inductive Proof |
| นักวิจัย | : | Bundy, Alan , Dixon, Lucas , Johansson, Moa |
| คำค้น | : | Computer Science , Rippling , Interactive Theorem Proving |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | Kaufmann, M , Paulson, L.C. |
| ปีพิมพ์ | : | 2553 |
| อ้างอิง | : | NA , http://hdl.handle.net/1842/3717 , 10.1007/978-3-642-14052-5_21 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements to be proved automatically. The new contribution is that our method also supports case-analysis on datatypes. By locating the case-analysis as a step within rippling we also maintain the termination. The work has been implemented in IsaPlanner and used to extend the existing inductive proof method. We evaluate this extended prover on a large set of examples from Isabelle’s theory library and from the inductive theorem proving literature. We find that this leads to a significant improvement in the coverage of inductive theorem proving. The main limitations of the extended prover are identified, highlight the need for advances in the treatment of assumptions during rippling and when conjecturing lemmas. |
| บรรณานุกรม | : |
Bundy, Alan , Dixon, Lucas , Johansson, Moa . (2553). Case-Analysis for Rippling and Inductive Proof.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Bundy, Alan , Dixon, Lucas , Johansson, Moa . 2553. "Case-Analysis for Rippling and Inductive Proof".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Bundy, Alan , Dixon, Lucas , Johansson, Moa . "Case-Analysis for Rippling and Inductive Proof."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2553. Print. Bundy, Alan , Dixon, Lucas , Johansson, Moa . Case-Analysis for Rippling and Inductive Proof. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2553.
|
