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

selp: A Single-Shot Epistemic logic Program Solver

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Bichler, Manuel Morak, Michael Woltran, Stefan TU Wien Vienna Austria

Epistemic logic Programs (ELPs) are an extension of Answer Set programming (ASP) with epistemic operators that allow for a form of meta-reasoning, that is, reasoning over multiple possible worlds. Existing ELP solving approaches generally rely on making multiple calls to an ASP solver in order to evaluate the ELP. However, in this paper, we show that there also exists a direct translation from ELPs into non-ground ASP with bounded arity. The resulting ASP program can thus be solved in a single shot. We then implement this encoding method, using recently proposed techniques to handle large, non-ground ASP rules, into the prototype ELP solving system "selp", which we present in this paper. This solver exhibits competitive performance on a set of ELP benchmark instances. Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming

ASP(AC): Answer set programming with algebraic constraints

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Eiter, Thomas Kiesel, Rafael Technical University Vienna Vienna Austria

Weighted logic is a powerful tool for the specification of calculations over semirings that depend on qualitative information. Using a novel combination of Weighted logic and Here-and-There (HT) logic, in which this dependence is based on intuitionistic grounds, we introduce Answer Set programming with Algebraic Constraints (ASP(A C )), where rules may contain constraints that compare semiring values to weighted formula evaluations. Such constraints provide streamlined access to a manifold of constructs available in ASP, like aggregates, choice constraints, and arithmetic operators. They extend some of them and provide a generic framework for defining programs with algebraic computation, which can be fruitfully used e.g. for provenance semantics of datalog programs. While undecidable in general, expressive fragments of ASP(A C ) can be exploited for effective problem solving in a rich framework. This work is under consideration for acceptance in Theory and Practice of logic programming. Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming

A generalised approach for encoding and reasoning with qualitative theories in answer set programming

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Baryannis, George Tachmazidis, Ilias Batsakis, Sotiris Antoniou, Grigoris Alviano, Mario Papadakis, Emmanuel University of Huddersfield United Kingdom University of Calabria Italy Center for Spatial Studies University of California Santa Barbara United States

Qualitative reasoning involves expressing and deriving knowledge based on qualitative terms such as natural language expressions, rather than strict mathematical quantities. Well over 40 qualitative calculi have been proposed so far, mostly in the spatial and temporal domains, with several practical applications such as naval traffic monitoring, warehouse process optimisation and robot manipulation. Even if a number of specialised qualitative reasoning tools have been developed so far, an important barrier to the wider adoption of these tools is that only qualitative reasoning is supported natively, when real-world problems most often require a combination of qualitative and other forms of reasoning. In this work, we propose to overcome this barrier by using ASP as a unifying formalism to tackle problems that require qualitative reasoning in addition to non-qualitative reasoning. A family of ASP encodings is proposed which can handle any qualitative calculus with binary relations. These encodings are experimentally evaluated using a real-world dataset based on a case study of determining optimal coverage of telecommunication antennas, and compared with the performance of two well-known dedicated reasoners. Experimental results show that the proposed encodings outperform one of the two reasoners, but fall behind the other, an acceptable trade-off given the added benefits of handling any type of reasoning as well as the interpretability of logic programs. This paper is under consideration for acceptance in TPLP. Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming

Context Delegation for Context-Based Access Control

学校读者我要写书评

暂无评论

Context Delegation for Context-Based Access Control

European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases, ECML PKDD 2018

作者： Al-Wahah, Mouiad Farkas, Csilla University of South Carolina ColumbiaSC29208 United States

ISBN: (纸本)9783030134525

The capability to delegate access privileges is an essential component of access control policies. We present an ontology-based context delegation approach for context-based access control. Our approach provides a dynamic and adaptive context delegation capability. The delegation does not cause any change to the underlying access control policy. We use Description logic (DL) and logic programming (LP) technologies for modeling contexts, delegation and CBAC privileges. We show how semantic-based techniques can be used to support adaptive and dynamic context delegation for CBAC policies. We provide the formal framework of the approach and show that it is decidable and consistent. © 2019, Springer Nature Switzerland AG.

关键词： logic programming

The blame game for property-based testing 34

学校读者我要写书评

暂无评论

The blame game for property-based testing

34th Italian Conference on Computational logic, CILC 2019

作者： Momigliano, Alberto Ornaghi, Mario DI Università di Milano Italy

We report on work in progress aiming to add blame features to property-based-testing in logic programming, in particular w.r.t. the mechanized meta-theory model checker αCheck. Once the latter reports a counterexample to a property stated in αProlog, a combination of abduction and proof explanation tries to help the user to locate the part of the program that is responsible for the unintended behavior. To evaluate whether these explanations are in fact useful, we need an unbiased collection of faulty programs, where the bugs location is unknown to us. We have thus implemented a mutation testing tool for αProlog that generates such a set. Preliminary experiments point to the usefulness of our blame allocator. The mutator is of independent interest, allowing us to gauge the effectiveness of the various strategies of αCheck in finding bugs in αProlog specifications. © 2019 CEUR-WS. All rights reserved.

关键词： logic programming

A system for explainable answer set programming

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Cabalar, Pedro Fandinno, Jorge Muñiz, Brais University of Corunna Spain University of Potsdam Germany

We present xclingo, a tool for generating explanations from ASP programs annotated with text and labels. These annotations allow tracing the application of rules or the atoms derived by them. The input of xclingo is a markup language written as ASP comment lines, so the programs annotated in this way can still be accepted by a standard ASP solver. xclingo translates the annotations into additional predicates and rules and uses the ASP solver clingo to obtain the extension of those auxiliary predicates. This information is used afterwards to construct derivation trees containing textual explanations. The language allows selecting which atoms to explain and, in its turn, which atoms or rules to include in those explanations. We illustrate the basic features through a diagnosis problem from the literature. Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming

A Modern Interpreter of Predicate Linear logic Formulas

学校读者我要写书评

暂无评论

A Modern Interpreter of Predicate Linear Logic Formulas

International Computer Sciences and Information Technologies (CSIT)

作者： Zuzana Bilanová Ján Perháč Michal Hulič Technical University of Košice Košice Slovakia

ISBN: (数字)9781728174433

ISBN: (纸本)9781728174440

This paper describes the design, implementation and possibilities of using a new interpreter of resource-oriented logical formulas. Predicate linear logic is an apparatus that captures the dynamics of a changing world uniquely -resources are consumed after their use. Although this logic system is quite well researched in the world due to its unique features, its most widespread computer implementations are woefully outdated and unsuitable for current research needs. The interpreter described in this article was created after a detailed study of the principles of predicate linear logic as well as existing interpreters of this logic. The new interpreter will be used not only in teaching the subject logic for Informatics at the Technical University in Košice, but we also plan to expand its possibilities and build on the ongoing (so far only) theoretical research at our university.

关键词： Phase locked loops Informatics logic programming Semantics Electrical engineering Computer science Syntactics

LP2PB: Translating answer set programs into pseudo-boolean theories

学校读者我要写书评

暂无评论

arXiv 2020年

作者： de Wulf, Wolf Bogaerts, Bart Vrije Universiteit Brussel Brussels Belgium

Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP programs into pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane–based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean solving. Our results are mixed: overall, traditional ASP solvers still outperform our translational approach, but several benchmark families are identified where the balance shifts the other way, thereby suggesting that further investigation into a stronger proof system for ASP is valuable. Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Chen, Taolue Hague, Matthew He, Jinlong Hu, Denghang Lin, Anthony Widjaja Rümmer, Philipp Wu, Zhilin University of Surrey United Kingdom Royal Holloway University of London United Kingdom State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China Technical University of Kaiserslautern Germany Uppsala University Sweden University of Chinese Academy of Sciences China Shanghai Key Laboratory of Trustworthy Computing East China Normal University China Institute of Intelligent Software Guangzhou China

Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths of, or positions in, strings. Analysis and testing of string-manipulating programs can be formulated as the path feasibility problem: given a symbolic execution path, does there exist an assignment to the inputs that yields a concrete execution that realizes this path? Such a problem can naturally be reformulated as a string constraint solving problem. Although state-of-the-art string constraint solvers usually provide support for both string and integer data types, they mainly resort to heuristics without completeness guarantees. In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers. Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming