COMPLETION AS A DERIVED RULE OF INFERENCE
Date
1990-10-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Description
Keywords
Computer Science