A Resolution Decision Procedure for Fluted Logic

Schmidt, R. A. and Hustadt, U. (2000)

In McAllester, D. (eds), Automated Deduction-CADE-17. Lecture Notes in Artificial Intelligence 1831, Springer, 433-448. BiBTeX (Copyright © 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.

The long version is Technical Report UMCS-00-3-1, University of Manchester.
Abstract. BiBTeX, PostScript.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 27 Nov 15
Copyright © 2000 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk