scientific article; zbMATH DE number 1301733

MaRDI QIDQ4246946zbMATH OpenFDO

Authors Daniel Fridlender

Publication date 13 December 1999

zbMATH Keywords

Ramsey theorembar inductionfan theoremHigman's lemmaMartin-Löf's type theoryproof editor ALFtype-theoretic proof

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Higman's lemma and its computational content
• Proof pearl: a formal proof of Higman's lemma in ACL2
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• scientific article; zbMATH DE number 2085177

Cited in

(10)

• Higman's lemma and its computational content
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Certified Kruskal's tree theorem
• A linear time algorithm for monadic querying of indefinite data over linearly ordered domains
• scientific article; zbMATH DE number 2085177 (Why is no real title available?)
• Proof pearl: a formal proof of Higman's lemma in ACL2
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Programs from proofs using classical dependent choice
• Helly's selection theorem and the principle of local reflexivity of ordered type

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