The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 100 of 1097
Back to Result List

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.show moreshow less

Export metadata

Additional Services

Search Google Scholar Statistics
Metadaten
Author details:Martin GebserORCiD, Torsten H. SchaubORCiDGND
DOI:https://doi.org/10.1145/2480759.2480767
ISSN:1529-3785
Title of parent work (English):ACM transactions on computational logic
Publisher:Association for Computing Machinery
Place of publishing:New York
Publication type:Article
Language:English
Year of first publication:2013
Publication year:2013
Release date:2017/03/26
Tag:Answer Set Programming; Theory; proof complexity; tableau calculi
Volume:14
Issue:2
Number of pages:40
Funding institution:German Science Foundation (DFG) [SCHA 550/8-1/2]
Organizational units:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science
Peer review:Referiert
Institution name at the time of the publication:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik
Accept ✔
This website uses technically necessary session cookies. By continuing to use the website, you agree to this. You can find our privacy policy here.