Please use this identifier to cite or link to this item: http://dspace.mediu.edu.my:8181/xmlui/handle/1721.1/6680
Full metadata record
DC FieldValueLanguage
dc.creatorArkoudas, Konstantine-
dc.date2004-10-08T20:37:19Z-
dc.date2004-10-08T20:37:19Z-
dc.date2001-11-13-
dc.date.accessioned2013-10-09T02:46:27Z-
dc.date.available2013-10-09T02:46:27Z-
dc.date.issued2013-10-09-
dc.identifierAIM-2001-031-
dc.identifierhttp://hdl.handle.net/1721.1/6680-
dc.identifier.urihttp://koha.mediu.edu.my:8181/xmlui/handle/1721-
dc.descriptionThis paper presents an algorithm for simplifying NDL deductions. An array of simplifying transformations are rigorously defined. They are shown to be terminating, and to respect the formal semantis of the language. We also show that the transformations never increase the size or complexity of a deduction---in the worst case, they produce deductions of the same size and complexity as the original. We present several examples of proofs containing various types of "detours", and explain how our procedure eliminates them, resulting in smaller and cleaner deductions. All of the given transformations are fully implemented in SML-NJ. The complete code listing is presented, along with explanatory comments. Finally, although the transformations given here are defined for NDL, we point out that they can be applied to any type-alpha DPL that satisfies a few simple conditions.-
dc.format45 p.-
dc.format2306816 bytes-
dc.format532283 bytes-
dc.formatapplication/postscript-
dc.formatapplication/pdf-
dc.languageen_US-
dc.relationAIM-2001-031-
dc.subjectAI-
dc.subjectdeduction-
dc.subjectproofs-
dc.subjectsimplifiation-
dc.subjectproof optimization-
dc.subjectdeduction complexity-
dc.titleSimplifying transformations for type-alpha certificates-
Appears in Collections:MIT Items

Files in This Item:
There are no files associated with this item.


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.