scientific article; zbMATH DE number 1303348

From MaRDI portal

Revision as of 16:28, 6 February 2024 by Import240129110113 (talk | contribs) (Created automatically from import240129110113)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:4249901

Jump to:navigation, search

zbMath0924.03024MaRDI QIDQ4249901

Carsten Schuermann, Frank Pfenning

Publication date: 7 November 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

deduction theorem intuitionistic logic logical framework meta-logic type preservation automated theorem prover Twelf inductive reasoning over LF encodings

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (8)

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

This page was built for publication:

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:4249901&oldid=18143543"