@INPROCEEDINGS{SchmidtHustadt00a,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
MONTH = jun # {~17--20,},
YEAR = {2000},
TITLE = {A Resolution Decision Procedure for Fluted Logic},
EDITOR = {McAllester, D.},
BOOKTITLE = {Automated Deduction---CADE-17},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1831},
PUBLISHER = {Springer},
PAGES = {433--448},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/SchmidtHustadt00a.html},
ABSTRACT = {Fluted logic is a fragment of first-order logic without function
symbols in which the arguments of atomic subformulae form ordered
sequences.
A consequence of this restriction is that, whereas first-order logic is only
semi-decidable, fluted logic is decidable.
In this paper we present a sound, complete and terminating inference
procedure for fluted logic.
Our characterisation of fluted logic is in terms
of a new class of so-called fluted clauses.
We show that this class is decidable by an ordering refinement of
first-order resolution and a new form of dynamic renaming, called
separation.
}
}