scientific article; zbMATH DE number 5872266

MaRDI QIDQ3086786zbMATH OpenFDO

Authors Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Hongwei Xi, Frank Pfenning

Publication date 30 March 2011

zbMATH Keywords

natural deductionhigher-order logicproof checkingtheorem-provingautomated theorem proverinteractive proof checkersystem TPS for classical type theory

Mathematics Subject Classification ID

Collected or selected works; reprintings or translations of classics (01A75) Mechanization of proofs and logical operations (03B35)

Cited in

(4)

• scientific article; zbMATH DE number 1809864 (Why is no real title available?)
• What holds in a context?
• Decidable higher-order unification problems
• On sets, types, fixed points, and checkerboards

Describes a project that uses

Uses Software

• IMPS
• Nuprl
• ETPS
• HOL
• TPTP
• TPS

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