2014/03/04 by Jesse Alama, Alama, Jesse
Computer Science · #68T15 #Advanced Algebra and Logic #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #acm:68T15 #cs.LO #msc:68T15
paper · pdf · doi:10.48550/arxiv.1403.0641
10 pages. Submitted to the Mark Stickel Festschrift
arxiv created 2014/03/04 · openalex publication_date 2014/03/04 · arxiv updated 2014/03/05 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/31
The proof identity problem asks: When are two proofs the same? The question naturally occurs when one reflects on mathematical practice. The problem understandably can be seen as a challenge for mathematical logic, and indeed various perspectives on the problem can be found in the proof theory literature. From the proof theory perspective, the challenge is met by laying down new calculi that eliminate ``bureaucracy''; techniques such as normalization and cut-elimination, as well as proof compression, are employed. In this note a new perspective on the proof identity problem is outlined. The new approach employs the concepts and tools of automated theorem proving and complements the rather more theoretical perspectives coming from pure proof theory. The practical approach is illustrated with experiments coming from the TPTP Problem Library.