Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68525OpenAlexW2484880499MaRDI QIDQ5477667FDOQ5477667

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

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

Mathematics Subject Classification ID

Cited In (6)

• Decision Procedures for Automating Termination Proofs
• Title not available (Why is that?)
• Proof pearl: a formal proof of Higman's lemma in ACL2
• Programs from proofs using classical dependent choice
• A formal proof of Dickson's lemma in ACL2
• A formalization of Newman's and Yokouchi's lemmas in a higher-order language

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)