Tree-width for first order formulae

We introduce tree-width for first order formulae \phi, fotw(\phi). We show that computing fotw is fixed-parameter tractable with parameter fotw. Moreover, we show that on classes of formulae of bounded fotw, model checking is fixed parameter tractable, with parameter the length of the formula. This...

Full description

Bibliographic Details
Main Authors: Isolde Adler, Mark Weyer
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2012-03-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/786/pdf