检索结果-内蒙古大学图书馆

FOLASP: FO(·) as input language for answer set solvers

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Dessel, Kylian Van Devriendt, Jo Vennekens, Joost KU Leuven Dept. of Computer Science De Nayer Campus Sint-Katelijne-Waver Belgium Leuven.AI – KU Leuven Institute for AI Leuven Belgium

Over the past decades, Answer Set programming (ASP) has emerged as an important paradigm for declarative problem solving. Technological progress in this area has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in non-monotonic reasoning, efforts have also been made to reconcile ASP with classical first-order logic (FO). This has resulted in the development of FO(·), an expressive extension of FO, which allows ASP-like problem solving in a purely classical setting. This language may be more accessible to domain experts already familiar with FO, and may be easier to combine with other formalisms that are based on classical logic. It is supported by the IDP inference system, which has successfully competed in a number of ASP competitions. Here, however, technological progress has been hampered by the limited number of systems that are available for FO(·). In this paper, we aim to address this gap by means of a translation tool that transforms an FO(·) specification into ASP-Core-2, thereby allowing ASP-Core-2 solvers to be used as solvers for FO(·) as well. We present experimental results to show that the resulting combination of our translation with an off-the-shelf ASP solver is competitive with the IDP system as a way of solving problems formulated in FO(·). © 2021, CC BY.

关键词： logic programming

The horn non-clausal class and its polynomiality

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Imaz, Gonzalo E. - CSIC Barcelona Spain

The expressiveness of propositional non-clausal (NC) formulas is exponentially richer than that of clausal formulas. Yet, clausal efficiency outperforms non-clausal efficiency. Indeed, a major weakness of the latter is that, while Horn clausal formulas, along with Horn algorithms, are crucial for the high efficiency of clausal reasoning, no Horn-like formulas in non-clausal form had been proposed. To overcome such weakness, we first define the hybrid class HNC of Horn Non-Clausal (Horn-NC) formulas by adequately lifting the Horn pattern to NC form, and argue that HNC, along with future Horn-NC algorithms shall increase non-clausal efficiency just as the Horn class has increased clausal efficiency. Secondly, we: (i) give the compact, inductive definition of HNC;(ii) prove that syntactically HNC subsumes the Horn class but semantically both classes are equivalent;and (iii) characterize the non-clausal formulas belonging to HNC. Thirdly, we define the Non-Clausal Unit-Resolution calculus, or URnc, and prove that it checks the satisfiability of HNC in polynomial time. This fact, to our knowledge, makes HNC the first characterized polynomial class in NC reasoning. Finally, we prove that HNC is linearly recognizable, and also that it is both strictly more succinct and exponentially richer than the Horn class. We discuss that in NC automated reasoning, e.g. satisfiability solving, theorem proving, logic programming, etc., can directly benefit from HNC and URnc and that, as a by-product of its proved properties, HNC arises as a new alternative to analyze Horn functions and implication systems. © 2021, CC BY.

关键词： logic programming

The possibilistic horn non-clausal knowledge bases

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Imaz, Gonzalo E. CSIC Barcelona Spain

Posibilistic logic is the most extended approach to handle uncertain and partially inconsistent information. Regarding normal forms, advances in possibilistic reasoning are mostly focused on clausal form. Yet, the encoding of real-world problems usually results in a non-clausal (NC) formula and NC-to-clausal translators produce severe drawbacks that heavily limit the practical performance of clausal reasoning. Thus, by computing formulas in its original NC form, we propose several contributions showing that notable advances are also possible in possibilistic non-clausal reasoning. Firstly, we define the class of Possibilistic Horn Non-Clausal Knowledge Bases, or HΣ, which subsumes the classes: possibilistic Horn and propositional Horn-NC. HΣ is shown to be a kind of NC analogous of the standard Horn class. Secondly, we define Possibilistic Non-Clausal Unit-Resolution, or URΣ, and prove that URΣ correctly computes the inconsistency degree of HΣ members. URΣ had not been proposed before and is formulated in a clausal-like manner, which eases its understanding, formal proofs and future extension towards non-clausal resolution. Thirdly, we prove that computing the inconsistency degree of HΣ members takes polynomial time. Although there already exist tractable classes in possibilistic logic, all of them are clausal, and thus, HΣ turns out to be the first characterized polynomial non-clausal class within possibilistic reasoning. We discuss that our approach serves as a starting point to developing uncertain non-clausal reasoning on the basis of both methodologies: DPLL and resolution. © 2021, CC BY.

关键词： logic programming

Generating explanations for answer set programming applications

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Trieu, Ly Ly Son, Tran Cao Pontelli, Enrico Balduccini, Marcello New Mexico State University MSC CS PO Box 30001 Las CrucesNM United States Saint Joseph’s University 5600 City Avenue PhiladelphiaPA United States

We present an explanation system for applications that leverage Answer Set programming (ASP). Given a program P, an answer set A of P, and an atom a in the program P, our system generates all explanation graphs of a which help explain why a is true (or false) given the program P and the answer set A. We illustrate the functionality of the system using some examples from the literature. © 2021, CC BY.

关键词： logic programming

Quantifiers on demand

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Gurfinkel, Arie Buchbinder, Sharon Shoham Vizel, Yakir University of Waterloo Tel Aviv University The Technion

Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this paper, we present a new algorithm, QUIC3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, QUIC3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While QUIC3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented QUIC3 within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying QUIC3 to verifying a variety of public benchmarks of array manipulating C programs. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming

Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained horn clauses

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Jochems, Jerome Department of Computer Science University of Bristol Bristol United Kingdom

Higher-order constrained Horn clauses (HoCHC) are a semantically-invariant system of higher-order logic modulo theories. With semi-decidable unsolvability over a semi-decidable background theory, HoCHC is suitable for safety verification. Less is known about its relation to larger classes of higher-order verification problems. Motivated by program equivalence, we introduce a coinductive version of HoCHC that enjoys a greatest model property. We define an encoding of higher-order recursion schemes (HoRS) into HoCHC logic programs. Correctness of this encoding reduces decidability of the open HoRS equivalence problem - and, thus, the λ Y-calculus Böhm tree equivalence problem - to semi-decidability of coinductive HoCHC over a complete and decidable theory of trees. © 2021, CC BY.

关键词： logic programming

A Brief History of Updates of Answer-Set Programs

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Leite, João Slota, Martin NOVA LINCS Universidade Nova de Lisboa Portugal

Over the last couple of decades there has been a considerable effort devoted to the problem of updating logic programs under the stable model semantics (a.k.a. answer-set programs) or, in other words, the problem of characterising the result of bringing up-to-date a logic program when the world it describes changes. Whereas the state-of-the-art approaches are guided by the same basic intuitions and aspirations as belief updates in the context of classical logic, they build upon fundamentally different principles and methods, which have prevented a unifying framework that could embrace both belief and rule updates. In this paper we will overview some of the main approaches and results related to answer-set programming updates, while pointing out some of the main challenges that research in this topic has faced. © 2021, CC BY-NC-SA.

关键词： logic programming

Online learning probabilistic event calculus theories in answer set programming

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Katzouris, Nikos Artikis, Alexander Paliouras, Georgios Demokritos Athens Greece Department of Maritime Studies University of Piraeus Piraeus Greece

Complex Event Recognition (CER) systems detect event occurrences in streaming time-stamped input using predefined event patterns. logic-based approaches are of special interest in CER, since, via Statistical Relational AI, they combine uncertainty-resilient reasoning with time and change, with machine learning, thus alleviating the cost of manual event pattern authoring. We present a system based on Answer Set programming (ASP), capable of probabilistic reasoning with complex event patterns in the form of weighted rules in the Event Calculus, whose structure and weights are learnt online. We compare our ASP-based implementation with a Markov logic-based one and with a number of state-of-the-art batch learning algorithms on CER datasets for activity recognition, maritime surveillance and fleet management. Our results demonstrate the superiority of our novel approach, both in terms of efficiency and predictive performance. This paper is under consideration for publication in Theory and Practice of logic programming (TPLP). © 2021, CC BY.

关键词： logic programming

Planning with incomplete information in quantified answer set programming

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Fandinno, Jorge Laferrière, François Romero, Javier Schaub, Torsten Son, Tran Cao New Mexico State University United States Omaha State University United States University of Potsdam Germany

We present a general approach to planning with incomplete information in Answer Set Program- ming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions to different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks. Under consideration for acceptance in TPLP. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming