Characterization Results for d-Horn Formulas, or On formulas that are true on Dual Reduced Products

CARLOS ARECES; VERÓNICA BECHER; SEBASTIÁN FERRO

Logic, Language and Computation, Volume 3, , Cavedon, P.Blackburn, N.Braisby and A. Shimoji.(eds),

University of Chicago Press

Año: 2001; p. 49 - 66

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 know 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 (1974), 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 Grammar through a Horn/d-Horn first-order theory.