Proof terms for simply typed higher order logic

Stefan Berghofer, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

29 Scopus citations

Abstract

This paper presents proof terms for simply typed, intuitio-nistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and reconstruction of proof terms are described and have been implemented in the theorem prover Isabelle. Experimental results confirm the effectiveness of the compression scheme.

Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics - 13th International Conference, TPHOLs 2000, Proceedings
EditorsMark Aagaard, John Harrison
PublisherSpringer Verlag
Pages38-52
Number of pages15
ISBN (Print)9783540678632
DOIs
StatePublished - 2000
Event13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000 - Portland, United States
Duration: 14 Aug 200018 Aug 2000

Publication series

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

Conference

Conference13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000
Country/TerritoryUnited States
CityPortland
Period14/08/0018/08/00

Fingerprint

Dive into the research topics of 'Proof terms for simply typed higher order logic'. Together they form a unique fingerprint.

Cite this