scientific article; zbMATH DE number 5872266

zbMATH Open1226.03026MaRDI QIDQ3086786FDOQ3086786

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

Publication date: 30 March 2011

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

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)

• Title not available (Why is that?)
• What holds in a context?
• Decidable higher-order unification problems
• On sets, types, fixed points, and checkerboards

Uses Software

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

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)