- Treffer 1 von 1
Tableau calculi for logic programs under answer set semantics
- We introduce formal proof systems based on tableau methods for analyzing computations in Answer Set Programming (ASP). Our approach furnishes fine-grained instruments for characterizing operations as well as strategies of ASP solvers. The granularity is detailed enough to capture a variety of propagation and choice methods of algorithms used for ASP solving, also incorporating SAT-based and conflict-driven learning approaches to some extent. This provides us with a uniform setting for identifying and comparing fundamental properties of ASP solving approaches. In particular, we investigate their proof complexities and show that the run-times of best-case computations can vary exponentially between different existing ASP solvers. Apart from providing a framework for comparing ASP solving approaches, our characterizations also contribute to their understanding by pinning down the constitutive atomic operations. Furthermore, our framework is flexible enough to integrate new inference patterns, and so to study their relation to existingWe introduce formal proof systems based on tableau methods for analyzing computations in Answer Set Programming (ASP). Our approach furnishes fine-grained instruments for characterizing operations as well as strategies of ASP solvers. The granularity is detailed enough to capture a variety of propagation and choice methods of algorithms used for ASP solving, also incorporating SAT-based and conflict-driven learning approaches to some extent. This provides us with a uniform setting for identifying and comparing fundamental properties of ASP solving approaches. In particular, we investigate their proof complexities and show that the run-times of best-case computations can vary exponentially between different existing ASP solvers. Apart from providing a framework for comparing ASP solving approaches, our characterizations also contribute to their understanding by pinning down the constitutive atomic operations. Furthermore, our framework is flexible enough to integrate new inference patterns, and so to study their relation to existing ones. To this end, we generalize our approach and provide an extensible basis aiming at a modular incorporation of additional language constructs. This is exemplified by augmenting our basic tableau methods with cardinality constraints and disjunctions.…
Verfasserangaben: | Martin GebserORCiD, Torsten SchaubORCiDGND |
---|---|
DOI: | https://doi.org/10.1145/2480759.2480767 |
ISSN: | 1529-3785 |
Titel des übergeordneten Werks (Englisch): | ACM transactions on computational logic |
Verlag: | Association for Computing Machinery |
Verlagsort: | New York |
Publikationstyp: | Wissenschaftlicher Artikel |
Sprache: | Englisch |
Jahr der Erstveröffentlichung: | 2013 |
Erscheinungsjahr: | 2013 |
Datum der Freischaltung: | 26.03.2017 |
Freies Schlagwort / Tag: | Answer Set Programming; Theory; proof complexity; tableau calculi |
Band: | 14 |
Ausgabe: | 2 |
Seitenanzahl: | 40 |
Fördernde Institution: | German Science Foundation (DFG) [SCHA 550/8-1/2] |
Organisationseinheiten: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
Peer Review: | Referiert |
Name der Einrichtung zum Zeitpunkt der Publikation: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik |