[isabelle] New AFP entry: A Complete Proof of the Robbins Conjecture



In 1996, Bill McCune's solved the Robbins Conjecture with the help of an
automatic theorem prover http://www.cs.unm.edu/~mccune/papers/robbins/.
Matthew Wampler-Doty has formalized the complete proof (not the proof
search!) in Isabelle/HOL:

A Complete Proof of the Robbins Conjecture
Matthew Wampler-Doty

This document gives a formalization of the proof of the Robbins
conjecture, following A. Mann, A Complete Proof of the Robbins
Conjecture, 2003.

http://afp.sourceforge.net/entries/Robbins-Conjecture.shtml





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.