R. A. Schmidt and U. Hustadt (2000): ``A resolution decision procedure for fluted logic.'' In D. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17) [Pittsburgh, USA, 17-20 June 2000], pp. 433-448. LNAI 1831, Springer.
Abstract, BibTeX PDF/A> (© Springer).

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.

[an error occurred while processing this directive]