ridm@nrct.go.th   ระบบคลังข้อมูลงานวิจัยไทย   รายการโปรดที่คุณเลือกไว้

System Description: an Interface Between CLAM and HOL

หน่วยงาน Edinburgh Research Archive, United Kingdom

รายละเอียด

ชื่อเรื่อง : System Description: an Interface Between CLAM and HOL
นักวิจัย : Alan, Bundy , Slind, K. , Gordon, M. , Boulton, R.
คำค้น : -
หน่วยงาน : Edinburgh Research Archive, United Kingdom
ผู้ร่วมงาน : -
ปีพิมพ์ : 2541
อ้างอิง : http://www.springerlink.com/content/buu51mnptynaquuy/ , http://hdl.handle.net/1842/4708
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : -
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

The CLAM proof planner has been interfaced to the HOL interactive theorem prover to provide the power of proof planning to people using HOL for formal verification, etc. The interface sends HOL goals to CLAM for planning and translates plans back into HOL tactics that solve the initial goals. The project homepage can be found at http://www.cl.cam.ac.uk/Research/HVG/Clam.HOL/intro.html.

บรรณานุกรม :
Alan, Bundy , Slind, K. , Gordon, M. , Boulton, R. . (2541). System Description: an Interface Between CLAM and HOL.
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Alan, Bundy , Slind, K. , Gordon, M. , Boulton, R. . 2541. "System Description: an Interface Between CLAM and HOL".
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Alan, Bundy , Slind, K. , Gordon, M. , Boulton, R. . "System Description: an Interface Between CLAM and HOL."
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2541. Print.
Alan, Bundy , Slind, K. , Gordon, M. , Boulton, R. . System Description: an Interface Between CLAM and HOL. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2541.