Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

19

TPHOL
2000
IEEE

favoriteEmaildiscussreport

162views Automated Reasoning» more TPHOL 2000»

Proof Terms for Simply Typed Higher Order Logic

13 years 8 months ago

Proof Terms for Simply Typed Higher Order Logic

Download www4.in.tum.de

Abstract. This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Uniﬁcation-based algorithms for the compression and reconstruction of proof terms are described and have been implemented in the theorem prover Isabelle. Experimental results conﬁrm the eﬀectiveness of the compression scheme.

Stefan Berghofer, Tobias Nipkow

Real-time Traffic

Automated Reasoning | Popular Logical Framework | Proof Terms | Theorem Prover Isabelle | TPHOL 2000 |

claim paper

Related Content

» Open Proofs and Open Terms A Basis for Interactive Logic

» Eliminating Redundancy in HigherOrder Unification A Lightweight Approach

» A Relational Modal Logic for HigherOrder Stateful ADTs

» Eliminating Proofs from Programs

» HOL2P A System of Classical Higher Order Logic with Second Order Polymorphism

» Reflecting Proofs in FirstOrder Logic with Equality

» ProofTheoretic and HigherOrder Extensions of Logic Programming

» HigherOrder Lazy Narrowing Calculus A Solver for HigherOrder Equations

» The HigherOrder Recursive Path Ordering

Post Info
More Details (n/a)

Added	01 Aug 2010
Updated	01 Aug 2010
Type	Conference
Year	2000
Where	TPHOL
Authors	Stefan Berghofer, Tobias Nipkow

Comments (0)