Tractable Combinations of Theories via Sampling

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

Abstract

For a first-order theory T, the Constraint Satisfaction Problem of T is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of T. In this article we develop sufficient conditions for polynomial-time tractability of the constraint satisfaction problem for the union of two theories with disjoint relational signatures. To this end, we introduce the concept of sampling for theories and show that samplings can be applied to examples which are not covered by the seminal result of Nelson and Oppen.

Details

Original languageEnglish
Title of host publicationLogics in Artificial Intelligence - 17th European Conference, JELIA 2021, Proceedings
EditorsWolfgang Faber, Gerhard Friedrich, Martin Gebser, Michael Morak
PublisherSpringer, Berlin [u. a.]
Pages133-146
Number of pages14
ISBN (print)9783030757748
Publication statusPublished - 2021
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 12678
ISSN0302-9743

Conference

Title17th European Conference on Logics in Artificial Intelligence
Abbreviated titleJELIA 2021
Conference number17
Duration17 - 20 May 2021
Locationonline
CityKlagenfurt
CountryAustria

External IDs

ORCID /0000-0001-8228-3611/work/142241056

Keywords