"Playing in the grey area of proofs."

Krystof Hoder, Laura Kovács, Andrei Voronkov (2012)
a service of Schloss Dagstuhl - Leibniz Center for Informatics