Proof Terms for Simply Typed Higher Order Logic

Abstract. This paper presents proof terms for simply typed, intuitionistic 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.

• Type: Conference
• Year: 2000
• Where: TPHOL
• Authors: Stefan Berghofer, Tobias Nipkow
• Keywords: Automated Reasoning, Popular Logical Framework, Proof Terms, Theorem Prover Isabelle, TPHOL 2000