"Programming and automating mathematics in the Tarski-Kleene hierarchy."

Alasdair Armstrong, Georg Struth, Tjark Weber (2014)
a service of Schloss Dagstuhl - Leibniz Center for Informatics