scientific article; zbMATH DE number 1301733
From MaRDI portal
Publication:4246946
zbMath0927.03080MaRDI QIDQ4246946
Publication date: 13 December 1999
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Ramsey theoremMartin-Löf's type theorybar inductionfan theoremHigman's lemmaproof editor ALFtype-theoretic proof
Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)
Related Items (6)
A linear time algorithm for monadic querying of indefinite data over linearly ordered domains ⋮ Certified Kruskal’s Tree Theorem ⋮ Proof pearl: a formal proof of Higman's lemma in ACL2 ⋮ A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ Higman’s Lemma and Its Computational Content ⋮ Programs from proofs using classical dependent choice
This page was built for publication: