scientific article; zbMATH DE number 1303348
From MaRDI portal
Publication:4249901
zbMath0924.03024MaRDI QIDQ4249901
Carsten Schuermann, Frank Pfenning
Publication date: 7 November 1999
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
deduction theoremintuitionistic logiclogical frameworkmeta-logictype preservationautomated theorem prover Twelfinductive reasoning over LF encodings
Related Items
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Nominal abstraction, A linear logical framework, Canonical HybridLF: extending Hybrid with dependent types, Focused Inductive Theorem Proving, Harpoon: mechanizing metatheory interactively, Mechanized metatheory revisited, Cut-elimination for a logic with definitions and induction
Uses Software
