A broader class of trees for recursive type definitions for HOL

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this paper we describe the construction in HOL of the inductive type of arbitrarily branching labeled trees. Such a type is characterized by an initiality theorem similar to that for finitely branching labeled trees. We discuss how to use this type to extend the system of simple recursive type specifications automatically definable in HOL to ones including a limited class of functional arguments. The work discussed here is a part of a larger project to expand the recursive types package of HOL which is nearing completion. All work described in this paper has been completed.

Original languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings
EditorsJeffrey J. Joyce, Carl-Johan H. Seger
PublisherSpringer
Pages141-154
Number of pages14
ISBN (Print)9783540578260
DOIs
StatePublished - 1994
Externally publishedYes
Event6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993 - Vancouver, Canada
Duration: Aug 11 1993Aug 13 1993

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume780 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993
Country/TerritoryCanada
CityVancouver
Period8/11/938/13/93

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A broader class of trees for recursive type definitions for HOL'. Together they form a unique fingerprint.

Cite this