scientific article; zbMATH DE number 1303348

MaRDI QIDQ4249901zbMATH OpenFDO

Authors Carsten Schürmann, Frank Pfenning

Publication date 7 November 1999

zbMATH Keywords

intuitionistic logicdeduction theoremlogical frameworkmeta-logictype preservationautomated theorem prover Twelfinductive reasoning over LF encodings

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Mechanizing metatheory in a logical framework
• Mechanizing the metatheory of LF
• scientific article; zbMATH DE number 65531
• A framework for defining logics

Cited in

(15)

• Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
• Mechanizing the metatheory of LF
• Harpoon: mechanizing metatheory interactively
• Cut-elimination for a logic with definitions and induction
• Nominal abstraction
• A linear logical framework
• Towards proof planning for \(\mathcal{M}_{\omega}^+\)
• Mechanized metatheory revisited
• Canonical HybridLF: extending Hybrid with dependent types
• scientific article; zbMATH DE number 4155932 (Why is no real title available?)
• Focused Inductive Theorem Proving
• A simplified account of the metatheory of linear LF
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF

Describes a project that uses

Uses Software

• Twelf
• ALF
• Elf

This page was built for publication:

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