@inproceedings{c811213ca3c74fdba7ec4f6a58a18d73,
title = "A resolution-based decision procedure for the two-variable fragment with equality",
abstract = "The two-variable-fragment L ≈ 2 of first order logic is the set of formulas that do not contain function symbols, that possibly contain equality, and that contain at most two variables. This paper shows how resolution theorem-proving techniques can be used to provide an algorithm for deciding whether any given formula in L ≈ 2 is satisfiable. Previous resolution-based techniques could deal only with the equality-free subset L 2 of the two-variable fragment. {\textcopyright} Springer-Verlag Berlin Heidelberg 2001.",
author = "{De Nivelle}, Hans and Ian Pratt-Hartmann",
year = "2001",
language = "English",
isbn = "3540422544",
volume = "2083",
series = "Lecture Notes in Artificial Intelligence",
publisher = "Springer Nature",
pages = "211--225",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",
address = "United States",
note = "1st International Joint Conference on Automated Reasoning, IJCAR 2001 ; Conference date: 01-07-2001",
}