@TECHREPORT{SchmidtHustadt00b,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
YEAR = {2000},
TITLE = {A Resolution Decision Procedure for Fluted Logic},
TYPE = {Technical Report},
NUMBER = {UMCS-00-3-1},
INSTITUTION = {University of Manchester},
ADDRESS = {UK},
NOTE = {Long version of~\cite{SchmidtHustadt00a}} ,
ISSN = {1361-6161},
URL = {http://www.cs.man.ac.uk/cstechrep/Abstracts/UMCS-00-3-1.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.
}}