scientific article; zbMATH DE number 1301733

zbMATH Open0927.03080MaRDI QIDQ4246946FDOQ4246946

Authors: Daniel Fridlender 

Publication date: 13 December 1999

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

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

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)

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
• Title not available (Why is that?)
• A linear time algorithm for monadic querying of indefinite data over linearly ordered domains
• 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)