scientific article; zbMATH DE number 1303348

zbMATH Open0924.03024MaRDI QIDQ4249901FDOQ4249901

Authors: Carsten Schürmann, Frank Pfenning 

Publication date: 7 November 1999

Title of this publication is not available (Why is that?)

Recommendations

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

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)

Cited In (15)

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

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)