| ชื่อเรื่อง | : | Isacosy: Synthesis of Inductive Theorems |
| นักวิจัย | : | Dixon, Lucas , Bundy, Alan , Johansson, Moa |
| คำค้น | : | - |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | - |
| ปีพิมพ์ | : | 2552 |
| อ้างอิง | : | http://hdl.handle.net/1842/4751 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | We have implemented a program for inductive theory formation, called IsaCoSy, which synthesises conjectures about recursively defined datatypes and functions. Only irreducible terms are generated, which keeps the search space tractably small. The synthesised terms are filtered through counter-example checking and then passed on to the automatic inductive prover IsaPlanner. Experiments have given promising results, with high recall of 83% for natural numbers and 100% for lists when compared to libraries for the Isabelle theorem prover. However, precision is somewhat lower, 38-63%. |
| บรรณานุกรม | : |
Dixon, Lucas , Bundy, Alan , Johansson, Moa . (2552). Isacosy: Synthesis of Inductive Theorems.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Dixon, Lucas , Bundy, Alan , Johansson, Moa . 2552. "Isacosy: Synthesis of Inductive Theorems".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Dixon, Lucas , Bundy, Alan , Johansson, Moa . "Isacosy: Synthesis of Inductive Theorems."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2552. Print. Dixon, Lucas , Bundy, Alan , Johansson, Moa . Isacosy: Synthesis of Inductive Theorems. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2552.
|
ridm@nrct.go.th ระบบคลังข้อมูลงานวิจัยไทย รายการโปรดที่คุณเลือกไว้
