Characterization Results for d-Horn Formulas

C. Areces, V. Becher, and S. Ferro. Characterization Results for d-Horn Formulas. In L. Cavedon, P. Blackburn, N. Braisby, and A. Shimojima, editors, Logic, Language and Computation, pp. 49–66, CSLI Publications, 2000. Extended version of ``Characterization Results for d-Horn Formulas'' (Areces, Becher and Ferro).

Download

[pdf] 

Abstract

We provide two different model theoretic characterizations of a fragment of first-order logic which we call d-Horn formulas. This fragment is dual to the well known Horn fragment and has the same complexity for proving unsatisfiability. The method used in the characterization (syntactic translation functions between formulas which are mimicked by translation functions between models) might be applied to characterize other first-order restrictions. This paper is related to the work of Henschen and Wos \shortcitehens:unit74, but we study semantic translation together with syntactic renaming functions. We comment shortly on a number of applications of d-Horn formulas, one of which is the characterization of Context Free Grammars through a Horn $\cup$ d-Horn first-order theory.

BibTeX

@InCollection{Areces2000b,
  author =       "C. Areces and V. Becher and S. Ferro",
  booktitle =    "Logic, Language and Computation",
  publisher =    "CSLI Publications",
  title =        "Characterization Results for d-{H}orn Formulas",
  year =         "2000",
  editor =       "L. Cavedon and P. Blackburn and N. Braisby and A.
                 Shimojima",
  note =         "Extended version of ``Characterization Results for
                 d-{H}orn Formulas'' (Areces, Becher and Ferro).",
  pages =        "49--66",
  volume =       "3",
  abstract =     "We provide two different model theoretic
                 characterizations of a fragment of first-order logic
                 which we call d-Horn formulas. This fragment is dual to
                 the well known Horn fragment and has the same
                 complexity for proving unsatisfiability. The method
                 used in the characterization (syntactic translation
                 functions between formulas which are mimicked by
                 translation functions between models) might be applied
                 to characterize other first-order restrictions. This
                 paper is related to the work of Henschen and Wos
                 \shortcite{hens:unit74}, but we study semantic
                 translation together with syntactic renaming functions.
                 We comment shortly on a number of applications of
                 d-Horn formulas, one of which is the characterization
                 of Context Free Grammars through a Horn $\cup$ d-Horn
                 first-order theory.",
  ISBN =         "978-1-57586-268-2",
}