"Quantifiers in logic and proof-search using permissive-nominal terms and sets."

Murdoch James Gabbay, Claus-Peter Wirth (2015)
a service of Schloss Dagstuhl - Leibniz Center for Informatics