Please use this identifier to cite or link to this item: http://hdl.handle.net/1880/46514
Title: DEALING WITH THE CHOICE OPERATOR IN HOL88
Authors: Graham, Brian
Keywords: Computer Science
Issue Date: 1-Apr-1990
Abstract: This paper discusses the choice operator @ in HOL88. It gives an intuitive interpretation, as well as the definition, and presents proof strategies for goals that contain this operator, broken down into cases based on the number of values which satisfy the predicate argument. A working knowledge of the HOL system is assumed.
URI: http://hdl.handle.net/1880/46514
Appears in Collections:Technical Reports

Files in This Item:
File Description SizeFormat 
1990-382-06.pdf1.65 MBAdobe PDFView/Open


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