scientific article; zbMATH DE number 1552510

zbMATH Open0970.68150MaRDI QIDQ4524768FDOQ4524768

Authors: Martin Strecker, Marko Luther, Friedrich W. von Henke 

Publication date: 15 January 2001

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

Recommendations

• scientific article; zbMATH DE number 1614692
• scientific article; zbMATH DE number 65530
• Tactic theorem proving with refinement-tree proofs and metavariables
• Automated proof construction in type theory using resolution
• Tactics and parameters

zbMATH Keywords

proof searchTYPELAB system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cited In (6)

• Title not available (Why is that?)
• Dependently Typed Programming Based on Automated Theorem Proving
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Tactic theorem proving with refinement-tree proofs and metavariables
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Tools and Algorithms for the Construction and Analysis of Systems

Uses Software

• PVS
• ALF
• KIV

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 Q4524768)