| ชื่อเรื่อง | : | Coloured rippling: An extension of a theorem proving heuristic |
| นักวิจัย | : | Yoshida, Tetsuya , Bundy, Alan , Green, Ian , Walsh, Toby , Basin, David |
| คำค้น | : | - |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | - |
| ปีพิมพ์ | : | 2537 |
| อ้างอิง | : | http://dblp.uni-trier.de/db/conf/ecai/ecai94.html , http://hdl.handle.net/1842/4524 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | Rippling is a type of rewriting developed in inductive theorem proving for removing differences between terms; the induction conclusion is annotated to mark its differences from the induction hypothesis and rippling attempts to move these differences. Until now rippling has been primarily employed in proofs where there is a single induction hypothesis.This paper describes an extension to rippling to deal with theorems with multiple hypotheses.Such theorems arise, for instance, when reasoning about data-structures like trees with multiple recursive arguments. The essential idea is to colour the annotation, with each colour corresponding to a different hypothesis. The annotation of rewrite rules used in rippling is similarly generalized so that rules propagate colours through terms. This annotation guides search so that rewrite rules are only applied if they reduce the differences between the conclusion and some of the hypotheses.We have tested this implementation on a number of problems, including two of Bledsoe’s challenge limit theorems. |
| บรรณานุกรม | : |
Yoshida, Tetsuya , Bundy, Alan , Green, Ian , Walsh, Toby , Basin, David . (2537). Coloured rippling: An extension of a theorem proving heuristic.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Yoshida, Tetsuya , Bundy, Alan , Green, Ian , Walsh, Toby , Basin, David . 2537. "Coloured rippling: An extension of a theorem proving heuristic".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Yoshida, Tetsuya , Bundy, Alan , Green, Ian , Walsh, Toby , Basin, David . "Coloured rippling: An extension of a theorem proving heuristic."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2537. Print. Yoshida, Tetsuya , Bundy, Alan , Green, Ian , Walsh, Toby , Basin, David . Coloured rippling: An extension of a theorem proving heuristic. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2537.
|
