| ชื่อเรื่อง | : | Formalising Term Synthesis for Isacosy |
| นักวิจัย | : | Johansson, Moa , Dixon, Lucas , Bundy, Alan |
| คำค้น | : | - |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | - |
| ปีพิมพ์ | : | 2553 |
| อ้างอิง | : | http://dream.inf.ed.ac.uk/events/automatheo-2010/ , http://hdl.handle.net/1842/4745 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | IsaCoSy is a theory formation system for inductive theories. It synthesises conjectures and uses the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a formal account of the algorithms implemented in the system, and prove their correctness. In particular, we show that IsaCoSy only produces irreducible terms, using constraints generated from the left-hand sides of a set of rewrite rules. |
| บรรณานุกรม | : |
Johansson, Moa , Dixon, Lucas , Bundy, Alan . (2553). Formalising Term Synthesis for Isacosy.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Johansson, Moa , Dixon, Lucas , Bundy, Alan . 2553. "Formalising Term Synthesis for Isacosy".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Johansson, Moa , Dixon, Lucas , Bundy, Alan . "Formalising Term Synthesis for Isacosy."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2553. Print. Johansson, Moa , Dixon, Lucas , Bundy, Alan . Formalising Term Synthesis for Isacosy. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2553.
|
ridm@nrct.go.th ระบบคลังข้อมูลงานวิจัยไทย รายการโปรดที่คุณเลือกไว้
