Open Proofs and Open Terms: A Basis for Interactive Logic

In the process of interactive theorem proving one often works with incomplete higher order proofs. In this paper we address the problem of giving a correctness criterion for these incomplete proofs by presenting open higher order logic o-Pred as a conservative extension of Pred. We define a typing system o-Pred and show that the CurryHoward embedding extends to embedding into o-Pred. We show that the contexts of this typing system extended with definitions can represent the notion of proof state and allow for forward reasoning, proof reuse and free exploration of the given data ('stratch paper' mechanism).

• Type: Journal
• Year: 2002
• Where: CSL
• Authors: Herman Geuvers, Gueorgui I. Jojgov
• Keywords: Automated Reasoning, Conservative Extension, Correctness Criterion, CSL 2002, Incomplete Proofs