Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable
- Submitting institution
-
The University of Manchester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 64301718
- Type
- D - Journal article
- DOI
-
10.1002/malq.201700055
- Title of journal
- Mathematical Logic Quarterly
- Article number
- -
- First page
- 218
- Volume
- 64
- Issue
- 3
- ISSN
- 0942-5616
- Open access status
- Compliant
- Month of publication
- July
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
0
- Research group(s)
-
A - Computer Science
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- "This paper considers the problem of recognising (finite) entailments in first-order logic with just two logical variables, but where several binary relations can be declared to be transitive. In 1999, Ganzinger, Meyer and Veanes showed this problem to be undecidable (in fact, just two transitive relations suffice for undecidability).
The paper shows that, in contrast, when only a single transitive relation is available, the finite entailment problem becomes decidable, thus resolving a problem left open by Ganzinger et al''s paper.
Enabled a 3-year grant from the Polish national funding council NCN (2018/31/B/ST6/03662, PLN548,900)."
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
