"A second-order system for polytime reasoning based on Grädel's theorem."

Stephen A. Cook, Antonina Kolokolova (2003)
a service of  Schloss Dagstuhl - Leibniz Center for Informatics