A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality.

Hans de Nivelle, Ian Pratt-Hartmann

Browse the full CADE paper archive.