A resolution decision procedure for fluted logic

R.A. Schmidt, Ullrich Hustadt

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.
Original languageEnglish
Title of host publicationAutomated Deduction - CADE-17
Subtitle of host publication17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings
EditorsDavid McAllester
Place of PublicationHeidelberg
PublisherSpringer Berlin
Pages433-448
Number of pages16
ISBN (Electronic)9783540451013
ISBN (Print)9783540676645
DOIs
Publication statusPublished - 5 Jun 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1831
NameLecture Notes in Artificial Intelligence
PublisherSpringer

Keywords

  • Modal Logic
  • Decision Procedure
  • Theorem Prover
  • Predicate Symbol
  • Empty Clause

Fingerprint

Dive into the research topics of 'A resolution decision procedure for fluted logic'. Together they form a unique fingerprint.

Cite this