• search hit 1 of 3
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

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Martin GebserORCiD, Torsten SchaubORCiDGND
DOI:https://doi.org/10.1145/2480759.2480767
ISSN:1529-3785 (print)
Parent Title (English):ACM transactions on computational logic
Publisher:Association for Computing Machinery
Place of publication:New York
Document Type:Article
Language:English
Year of first Publication:2013
Year of Completion:2013
Release Date:2017/03/26
Tag:Answer Set Programming; Theory; proof complexity; tableau calculi
Volume:14
Issue:2
Pagenumber:40
Funder: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 publication:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik