Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477667zbMATH OpenOpenAlexFDO

Authors Francisco Jesús Martín-Mateos, José Luis Ruiz-Reina, Jose Antonio Alonso, María José Hidalgo

Publication date 6 July 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Recommendations

• Proof pearl: a formal proof of Higman's lemma in ACL2
• scientific article; zbMATH DE number 1301733
• Certified Kruskal's tree theorem
• Higman's lemma and its computational content
• Types for Proofs and Programs

Cited in

(8)

• Programs from proofs using classical dependent choice
• Decision Procedures for Automating Termination Proofs
• A formal proof of Dickson's lemma in ACL2
• A formalization of Newman's and Yokouchi's lemmas in a higher-order language
• scientific article; zbMATH DE number 1301733 (Why is no real title available?)
• Proof pearl: a formal proof of Higman's lemma in ACL2
• scientific article; zbMATH DE number 2085177 (Why is no real title available?)
• Proving Matijasevich's lemma with a default arithmetic strategy

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Theorem Proving in Higher Order Logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5477667)