Over the years, the stable-model semantics has gained a position of the correct (two-valued) interpretation of default negation in programs. However, for programs with aggregates (constraints), the stable-model semant...
详细信息
ISBN:
(纸本)9783642028458
Over the years, the stable-model semantics has gained a position of the correct (two-valued) interpretation of default negation in programs. However, for programs with aggregates (constraints), the stable-model semantics, in its broadly accepted generalization stemming from the work by Pearce, Ferraris and Lifschitz, has a competitor: the semantics proposed by Faber, Leone and Pfeifer, which seems to be essentially different. Our goal is to explain the relationship between the two semantics. Pearce, Ferraris and Lifschitz's extension of the stable-model semantics is best viewed in the setting of arbitrary propositional theories. We propose an extension of the Faber-Leone-Pfeifer semantics, or FLP semantics, for short, to the full propositional language, which reveals both common threads and differences between the FLP and stable-model semantics. We establish several properties of the FLP semantics. We apply a similar approach to define supported models for arbitrary propositional theories.
作者：
Geibinger, TobiasTompits, HansTech Univ Wien
Christian Doppler Lab Artificial Intelligence & O Databases & Artificial Intelligence Grp Inst Log & Computat Favoritenstr 9-11 A-1040 Vienna Austria Tech Univ Wien
Inst Log & Computat Knowledge Based Syst Grp Favoritenstr 9-11 A-1040 Vienna Austria
Starting with the seminal work on strong equivalence by Lifschitz, Pearce, and Valverde, many different advanced notions of program equivalence have been studied in the area of answer-set programming (ASP). In particu...
详细信息
ISBN:
(纸本)9783030195700;9783030195694
Starting with the seminal work on strong equivalence by Lifschitz, Pearce, and Valverde, many different advanced notions of program equivalence have been studied in the area of answer-set programming (ASP). In particular, relativised strong equivalence with projection has been introduced as a generalisation of strong equivalence by parameterising, on the one hand, the alphabet of the context programs used for checking program equivalence as well as, on the other hand, allowing the filtering of auxiliary atoms. Like many other advanced equivalence notions, it was introduced originally for propositional programs, along with model-theoretic concepts providing characterisations when equivalence between two programs hold. In this paper, we extend these concepts and characterisations to the general case of non-ground programs.
answer-set programming (ASP) is a powerful and expressive knowledge representation paradigm with a significant number of applications in logic-based AI. The traditional ground-and-solve approach, however, requires ASP...
详细信息
answer-set programming (ASP) is a powerful and expressive knowledge representation paradigm with a significant number of applications in logic-based AI. The traditional ground-and-solve approach, however, requires ASP programs to be grounded upfront and thus suffers from the so-called grounding bottleneck (i.e., ASP programs easily exhaust all available memory and thus become unsolvable). As a remedy, lazy-grounding ASP solvers have been developed, but many state-of-the-art techniques for grounded ASP solving have not been available to them yet. In this work we present, for the first time, adaptions to the lazy-grounding setting for many important techniques, like restarts, phase saving, domain-independent heuristics, and learned-clause deletion. Furthermore, we investigate their effects and in general observe a large improvement in solving capabilities and also uncover negative effects in certain cases, indicating the need for portfolio solving as known from other solvers.
In the last decade, answersetprogramming (ASP) and Satisfiability (SAT) have been used to solve combinatorial search problems and practical applications in which they arise. In each of these formalisms, a tool calle...
详细信息
In the last decade, answersetprogramming (ASP) and Satisfiability (SAT) have been used to solve combinatorial search problems and practical applications in which they arise. In each of these formalisms, a tool called a solver is used to solve problems. A solver takes as input a specification of the problem – a logic program in the case of ASP, and a CNF theory for SAT – and produces as output a solution to the problem. Designing fast solvers is important for the success of this general-purpose approach to solving search problems. Classes of instances that pose challenges to solvers can help in this task. In this dissertation we create challenging yet simple benchmarks for existing solvers in ASP and SAT. We do so by providing models of simple logic programs as well as models of simple CNF theories. We then randomly generate logic programs as well as CNF theories from these models. Our experimental results show that computing answersets of random logic programs as well as models of random CNF theories with carefully chosen parameters is hard for existing solvers. We generate random logic programs with 2-literals, and our experiments show that it is hard for ASP solvers to obtain answersets of purely negative and constraint-free programs, indicating the importance of these programs in the development of ASP solvers. An easy-hard-easy pattern emerges as we compute the average number of choice points generated by ASP solvers on randomly generated 2-literal programs with an increasing number of rules. We provide an explanation for the emergence of this pattern in these programs. We also theoretically study the probability of existence of an answerset for sparse and dense 2-literal programs. We consider simple classes of mixed Horn formulas with purely positive 2- literal clauses and purely negated Horn clauses. First we consider a class of mixed Horn formulas wherein each formula has m 2-literal clauses and k-literal negated Horn clauses. We show that formulas that
The term Participatory Guarantee Systems (PGS) refers to quality certification systems based on the active participation of stakeholders, i.e., producers, consumers, and experts. Unlike to the more common Third Party ...
详细信息
ISBN:
(纸本)9781450375184
The term Participatory Guarantee Systems (PGS) refers to quality certification systems based on the active participation of stakeholders, i.e., producers, consumers, and experts. Unlike to the more common Third Party Certification system, quality standards are guaranteed by peer review: visits of production sites by producers themselves. A critical issue in PGS is the assignment of the peers carrying each review visit, in a way that incentivizes participation. This paper explores algorithmic aspects of this peer assignment, so as to better address challenges faced by PGS. First, we propose a mathematical model of this task that can express diverse local PGS situations, as well as possible extensions. Then, we show that this model leads to computationally challenging problems and identify restrictions that are easy to handle. Finally, we develop an encoding of the model in answersetprogramming and use it to solve realistic scenarios of PGS.
Preference elicitation is a serious bottleneck in many decision support applications and agent specification tasks. Ceteris paribus (CP)-nets were designed to make the process of preference elicitation simpler and mor...
详细信息
Preference elicitation is a serious bottleneck in many decision support applications and agent specification tasks. Ceteris paribus (CP)-nets were designed to make the process of preference elicitation simpler and more intuitive for lay users by graphically structuring a set of CP preference statements-preference statements that most people find natural and intuitive. Beside their usefulness in the process of preference elicitation, CP-nets support efficient optimization algorithms that are crucial in most applications (e. g., the selection of the best action to execute or the best product configuration). In various contexts, CP-nets with an underlying cyclic structure emerge naturally. Often, they are inconsistent according to the current semantics, and the user is required to revise them. In this paper, we show how optimization queries can be meaningfully answered in many "inconsistent" networks without troubling the user with requests for revisions. In addition, we describe a method for focusing the user's revision process when revisions are truly needed. In the process, we provide a formal semantics that justifies our approach and new techniques for computing optimal outcomes. Some of the methods we use are based on a reduction to the problem of computing stable models for nonmonotonic logic programs, and we explore this relationship closely.
暂无评论