Open proofs and open terms: A basis for interactive logic

DOI10.1007/3-540-45793-3_36MaRDI QIDQ4411846zbMATH OpenFDO

Authors Herman Geuvers, G. I. Jojgov

Publication date 10 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2471/24710537.htm

zbMATH Keywords

formulas-as-typesinteractive theorem provingmeta-variablesopen termstype theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Holes with binding power
• Logic representation in LF
• A calculus of tactics and its operational semantics
• Tactic theorem proving with refinement-tree proofs and metavariables
• The foundation of a generic theorem prover

Cited in

(14)

• A compact kernel for the calculus of inductive constructions
• The lambda-context calculus (extended version)
• Tinycals: step by step tacticals
• MikiBeta : A General GUI Library for Visualizing Proof Trees
• Holes with binding power
• Tactics and parameters
• Two-level lambda-calculus
• Implementing type theory in higher order constraint logic programming
• scientific article; zbMATH DE number 6297875 (Why is no real title available?)
• An open formalism against incompleteness
• Partial proof terms in the study of idealized proof search
• Proof search in classical propositional logic with partial proof terms
• Multi-level contextual type theory
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

Describes a project that uses

Uses Software

• Automath
• ALF

This page was built for publication: Open proofs and open terms: A basis for interactive logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4411846)