Guarded Ord-Horn: A Tractable Fragment of Quantified Constraint Satisfaction
2012 (English)Conference paper (Other academic)
The first-order theory of dense linear orders without endpoints is well-known to be PSPACE-complete. We present polynomial-time tractability results for fragments of this theory which are defined by syntactic restriction, in particular, our fragments can be described using the framework of quantified constraint satisfaction over Ord-Horn clauses.
Place, publisher, year, edition, pages
IEEE , 2012. 99-106 p.
IdentifiersURN: urn:nbn:se:liu:diva-79512DOI: 10.1109/TIME.2012.19ISBN: 978-1-4673-2659-9OAI: oai:DiVA.org:liu-79512DiVA: diva2:543172
19th International Symposium on Temporal Representation and Reasoning (TIME-2012), 12-14 September, Leicester, UK