scientific article; zbMATH DE number 4009856

MaRDI QIDQ3759967zbMATH OpenFDO

Authors Ken Hirose

Publication date 1986

zbMATH Keywords

Computer Aided Proofintuitionistic logiclinear algebraNew Generation Computer Technologyproof checkersynthetic differential geometry

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4078854
• scientific article; zbMATH DE number 1254011
• Notes from the logbook of a proof-checker's project
• scientific article; zbMATH DE number 3907807
• The Proof Certifier Checkers

Cited in

(10)

• Abstract proof checking: An example motivated by an incompleteness theorem
• CalcCheck: a proof checker for teaching the ``Logical approach to discrete math
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• The Proof Certifier Checkers
• scientific article; zbMATH DE number 3907807 (Why is no real title available?)
• The use of machines to assist in rigorous proof
• scientific article; zbMATH DE number 4078854 (Why is no real title available?)
• A two-level approach towards lean proof-checking
• Notes from the logbook of a proof-checker's project
• On extensibility of proof checkers

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