scientific article; zbMATH DE number 1303348

MaRDI QIDQ4249901zbMATH OpenFDO

Authors Carsten Schürmann, Frank Pfenning

Publication date 7 November 1999

zbMATH Keywords

automated theorem prover Twelfdeduction theoreminductive reasoning over LF encodingsintuitionistic logiclogical frameworkmeta-logictype preservation

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)

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

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)