6533b7d9fe1ef96bd126c512

RESEARCH PRODUCT

Decidability Frontier for Fragments of First-Order Logic with Transitivity

subject

description

Several decidable fragments of first-order logic have been identified in the past as a generalisation of the standard translation of modal logic. These include: the fluted fragment, the two-variable frag- ment, the guarded fragment and the unary negation fragment; some of them have been recently generalised or combined to yield even more expressive decidable logics (guarded negation fragment or uniform one- dimensional fragment). None of the fragments allows one to express tran- sitivity of a binary relation or related properties like being an equivalence, a linear or a partial order, that naturally appear in specifications or in verification. The question therefore arises what is the impact of adding transitivity to these fragments and, where the cost is too high, how can these languages be tamed . In this talk we survey results concerning the decidability frontier of the above-mentioned fragments extended with transitivity. We discuss both, general and finite satisfiability, as presence of transitivity axioms often allows one to express axioms of infinity. Simultaneously, we locate in the picture known description logics, discuss relevant technics, admire a few exotic results and state some open questions.