FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Unary negation fragment with equivalence relations has the finite model property

Authors: Daniel Danielski and Emanuel Kieronski

Paper Information

Title:Unary negation fragment with equivalence relations has the finite model property
Authors:Daniel Danielski and Emanuel Kieronski
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:unary negation fragment, equivalence relations, satisfiability, finite model property
Abstract:

ABSTRACT. We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More specifically, we show that every satisfiable formula has a model of at most doubly exponential size. We argue that the satisfiability (= finite satisfiability) problem for this logic is \TwoExpTime-complete. We also transfer our results to a restricted variant of the guarded negation fragment with equivalence relations.

Pages:10
Talk:Jul 11 11:40 (Session 64D)
Paper: