# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

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

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

de Nivelle, H., & Pratt-Hartmann, I. (2001). A Resolution-Based Decision Procedure
for the Two-Variable Fragment with Equality. In R. Goré, A. Leitsch, & T. Nipkow (*Automated reasoning: First International Joint Conference, IJCAR 2001* (pp. 211-225). Berlin,
Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-31DF-7

##### Abstract

The two-variable fragment 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 or not any given formula
in the two-variable fragment is satisfiable. Previous
resolution-based techniques could deal only with the
equality-free subset of the two-variable fragment.