Please use this identifier to cite or link to this item: http://hdl.handle.net/1880/46524
Title: COMPLETION AS A DERIVED RULE OF INFERENCE
Authors: Slind, Konrad
Keywords: Computer Science
Issue Date: 1-Oct-1990
Abstract: A simple first step in the investigation of term rewriting systems in higher order logic is to just insert the first order completion algorithm unchanged into the more complicated logic. This paper presents the details of how this is done in Mike Gordon's HOL system, an implementation of Church's Simple Type Theory. We present completion as a derived rule of inference, not (as usual) as an ad hoc procedure. The completion rule presented here is easily adaptable to other natural deduction logics with equality.
URI: http://hdl.handle.net/1880/46524
Appears in Collections:Technical Reports

Files in This Item:
File Description SizeFormat 
1990-409-33.pdf1.02 MBAdobe PDFView/Open


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