Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

Ian Pratt-Hartmann

doi:10.1002/malq.201700055

Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

Ian Pratt-Hartmann

Formal Methods

Research output: Contribution to journal › Article › peer-review

Abstract

We consider two-variable, first-order logic in which a single distinguished predicate is required to be interpreted as a transitive relation. We show that the finite satisfiability problem for this logic is decidable in triply exponential non-deterministic time. Complexity falls to doubly exponential non-deterministic time if the transitive relation is constrained to be a partial order.

Original language	English
Pages (from-to)	218–248
Number of pages	31
Journal	Mathematical Logic Quarterly
Volume	64
Issue number	3
Early online date	24 Jul 2018
DOIs	https://doi.org/10.1002/malq.201700055
Publication status	Published - 3 Aug 2018

Keywords

Two-variable fragment
Finite satisfiability
Transitivity complexity

Access to Document

10.1002/malq.201700055Licence: CC BY

Cite this

@article{249684799c46457d9e196502c6e67c3f,

title = "Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable",

abstract = "We consider two-variable, first-order logic in which a single distinguished predicate is required to be interpreted as a transitive relation. We show that the finite satisfiability problem for this logic is decidable in triply exponential non-deterministic time. Complexity falls to doubly exponential non-deterministic time if the transitive relation is constrained to be a partial order.",

keywords = "Two-variable fragment, Finite satisfiability, Transitivity complexity",

author = "Ian Pratt-Hartmann",

year = "2018",

month = aug,

day = "3",

doi = "10.1002/malq.201700055",

language = "English",

volume = "64",

pages = "218{\textendash}248",

journal = "Mathematical Logic Quarterly",

issn = "0942-5616",

publisher = "John Wiley \& Sons Ltd",

number = "3",

}

TY - JOUR

T1 - Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

AU - Pratt-Hartmann, Ian

PY - 2018/8/3

Y1 - 2018/8/3

N2 - We consider two-variable, first-order logic in which a single distinguished predicate is required to be interpreted as a transitive relation. We show that the finite satisfiability problem for this logic is decidable in triply exponential non-deterministic time. Complexity falls to doubly exponential non-deterministic time if the transitive relation is constrained to be a partial order.

AB - We consider two-variable, first-order logic in which a single distinguished predicate is required to be interpreted as a transitive relation. We show that the finite satisfiability problem for this logic is decidable in triply exponential non-deterministic time. Complexity falls to doubly exponential non-deterministic time if the transitive relation is constrained to be a partial order.

KW - Two-variable fragment

KW - Finite satisfiability

KW - Transitivity complexity

UR - https://www.scopus.com/pages/publications/85050969189

U2 - 10.1002/malq.201700055

DO - 10.1002/malq.201700055

M3 - Article

SN - 0942-5616

VL - 64

SP - 218

EP - 248

JO - Mathematical Logic Quarterly

JF - Mathematical Logic Quarterly

IS - 3

ER -

Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this