Adding external decision procedures to HOL90 securely

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

Abstract

This paper describes a modest conservative extension of HOL90 that allows the results from external decision procedures to be used within HOL90 without compromising its logical consistency.

Original languageEnglish (US)
Title of host publicationTheorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings
EditorsJim Grundy, Malcolm Newey
PublisherSpringer
Pages143-152
Number of pages10
ISBN (Print)3540649875, 9783540649878
DOIs
StatePublished - 1998
Externally publishedYes
Event11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 - Canberra, Australia
Duration: Sep 27 1998Oct 1 1998

Publication series

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

Other

Other11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998
Country/TerritoryAustralia
CityCanberra
Period9/27/9810/1/98

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Adding external decision procedures to HOL90 securely'. Together they form a unique fingerprint.

Cite this