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

Abstract Solvers for Computing Cautious Consequences of ASP programs

theory and practice of logic programming 2019年第5-6期19卷 740-756页

作者： Amendola, Giovanni Dodaro, Carmine Maratea, Marco Univ Calabria Commenda Di Rende Italy Univ Genoa Genoa Italy

A Abstract solvers are a method to formally analyze algorithms that have been profitably used for describing, comparing and composing solving techniques in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set programming (ASP), and Constraint ASP. In this paper, we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers for cautious reasoning in ASP with new techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. By doing so, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. We implement some of the new solutions in the ASP solver wasp and show that their performance are comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions.

关键词： Answer Set programming Abstract solvers Cautious reasoning

来源：评论

学校读者我要写书评

暂无评论

Incremental Answer Set programming with Overgrounding

引用

theory and practice of logic programming 2019年第5-6期19卷 957-973页

作者： Calimeri, Francesco Ianni, Giovambattista Pacenza, Francesco Perri, Simona Zangari, Jessica Univ Calabria Dept Math & Comp Sci Commenda Di Rende Italy

Repeated executions of reasoning tasks for varying inputs are necessary in many applicative settings, such as stream reasoning. In this context, we propose an incremental grounding approach for the answer set semantics. We focus on the possibility of generating incrementally larger ground logic programs equivalent to a given non-ground one;so called overgrounded programs can be reused in combination with deliberately many different sets of inputs. Updating overgrounded programs requires a small effort, thus making the instantiation of logic programs considerably faster when grounding is repeated on a series of inputs similar to each other. Notably, the proposed approach works "under the hood", relieving designers of logic programs from controlling technical aspects of grounding engines and answer set systems. In this work we present the theoretical basis of the proposed incremental grounding technique, we illustrate the consequent repeated evaluation strategy and report about our experiments.

关键词： Knowledge Representation Answer Set programming Stream Reasoning Grounding Instantiation of logic Programs Overgrounding

来源：评论

学校读者我要写书评

暂无评论

A Syntactic Operator for Forgetting that Satisfies Strong Persistence

引用

theory and practice of logic programming 2019年第5-6期19卷 1038-1055页

作者： Berthold, Matti Goncalves, Ricardo Knorr, Matthias Leite, Joao Tech Univ Dresden Dresden Germany Univ Leipzig Leipzig Germany Univ Nova Lisboa Dept Informat NOVA LINCS Lisbon Portugal

Whereas the operation of forgetting has recently seen a considerable amount of attention in the context of Answer Set programming (ASP), most of it has focused on theoretical aspects, leaving the practical issues largely untouched. Recent studies include results about what sets of properties operators should satisfy, as well as the abstract characterization of several operators and their theoretical limits. However, no concrete operators have been investigated. In this paper, we address this issue by presenting the first concrete operator that satisfies strong persistence - a property that seems to best capture the essence of forgetting in the context of ASP - whenever this is possible, and many other important properties. The operator is syntactic, limiting the computation of the forgetting result to manipulating the rules in which the atoms to be forgotten occur, naturally yielding a forgetting result that is close to the original program.

关键词： Answer Set programming Forgetting Strong Persistence Syntactic Operator

来源：评论

学校读者我要写书评

暂无评论

On the Equivalence Between Abstract Dialectical Frameworks and logic Programs

引用

theory and practice of logic programming 2019年第5-6期19卷 941-956页

作者： Alcantara, Joao Sa, Samy Acosta-Guadarrama, Juan Univ Fed Ceara Fortaleza Ceara Brazil Autonomous Univ Juarez Ciudad Juarez Mexico

A Abstract Dialectical Frameworks (ADFs) are argumentation frameworks where each node is associated with an acceptance condition. This allows us to model different types of dependencies as supports and attacks. Previous studies provided a translation from Normal logic Programs (NLPs) to ADFs and proved the stable models semantics for a normal logic program has an equivalent semantics to that of the corresponding ADF. However, these studies failed in identifying a semantics for ADFs equivalent to a three-valued semantics (as partial stable models and well-founded models) for NLPs. In this work, we focus on a fragment of ADFs, called Attacking Dialectical Frameworks (ADF(+) s), and provide a translation from NLPs to ADF(+) s robust enough to guarantee the equivalence between partial stable models, well-founded models, regular models, stable models semantics for NLPs and respectively complete models, grounded models, preferred models, stable models for ADFs. In addition, we define a new semantics for ADF(+) s, called L-stable, and show it is equivalent to the L-stable semantics for NLPs.

关键词： Abstract Dialectical Frameworks Normal logic Programs Argumentation Instantiations of Argumentation Frameworks

来源：评论

学校读者我要写书评

暂无评论

Symbolic Analysis of Maude Theories with Narval

引用

theory and practice of logic programming 2019年第5-6期19卷 874-890页

作者： Alpuente, Maria Escobar, Santiago Sapina, Julia Ballis, Demis Univ Politecn Valencia VRAIN Valencian Res Inst Artificial Intelligence Valencia Spain Univ Udine DMIF Udine Italy

Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude's symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading;(ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity;and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.

关键词： Symbolic reachability analysis narrowing equational unification Maude rewriting logic

来源：评论

学校读者我要写书评

暂无评论

Constraint answer set programming: Integrational and translational (or SMT-based) approaches

arXiv

引用

arXiv 2021年

作者： Lierler, Yuliya University of Nebraska Omaha United States

Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. Constraint answer set programming demonstrates promising results, including the development of a multitude of solvers: ACSOLVER, CLINGCON, EZCSP, IDP, INCA, DINGO, MINGO, ASPMT2SMT, CLINGO[L,DL], and EZSMT. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Travelling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP. Under consideration in theory and practice of logic programming (TPLP). © 2021, CC BY.

关键词： Traveling salesman problem

来源：评论

学校读者我要写书评

暂无评论

Enabling Reasoning with LegalRuleML

引用

theory and practice of logic programming 2019年第1期19卷 1-26页

作者： Lam, Ho-Pun Hashmi, Mustafa CSIRO Data61 Sydney NSW Australia CSIRO Data61 Brisbane Qld Australia

In order to automate verification process, regulatory rules written in natural language need to be translated into a format that machines can understand. However, none of the existing formalisms can fully represent the elements that appear in legal norms. For instance, most of these formalisms do not provide features to capture the behavior of deontic effects, which is an important aspect in automated compliance checking. This paper presents an approach for transforming legal norms represented using legalruleml to a variant of modal defeasible logic (and vice versa) such that a legal statement represented using LegalRuleML can be transformed into a machine-readable format that can be understood and reasoned about depending upon the client's preferences.

关键词： Deontic logic modal defeasible logic legal reasoning LegalRuleML business contracts

来源：评论

学校读者我要写书评

暂无评论

Inconsistency Proofs for ASP: The ASP-DRUPE Format

引用

theory and practice of logic programming 2019年第5-6期19卷 891-907页

作者： Alviano, Mario Dodaro, Carmine Fichte, Johannes K. Hecher, Markus Philipp, Tobias Rath, Jakob Univ Calabria Commenda Di Rende Italy Tech Univ Dresden Dresden Germany TU Wien Vienna Austria Secunet Secur Networks AG Essen Germany

Answer Set programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs.

关键词： Answer Set programming Reverse Unit Propagation proofs inconsistency proofs

来源：评论

学校读者我要写书评

暂无评论

Temporal minimal-World semantics for sparse ABoxes

arXiv

引用

arXiv 2021年

作者： Borgwardt, Stefan Forkel, Walter Kovtunova, Alisa Chair for Automata Theory Technische Universität Dresden Germany

Ontology-mediated query answering is a popular paradigm for enriching answers to user queries with background knowledge. For querying the absence of information, however, there exist only few ontology-based approaches. Moreover, these proposals conflate the closed-domain and closed-world assumption, and therefore are not suited to deal with the anonymous objects that are common in ontological reasoning. Many real-world applications, like processing electronic health records (EHRs), also contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. Our contribution consists of two main parts: In the first part we introduce a new closed-world semantics for answering conjunctive queries with negation over ontologies formulated in the description logic 'ELH⊥, which is based on the minimal canonical model. We propose a rewriting strategy for dealing with negated query atoms, which shows that query answering is possible in polynomial time in data complexity. In the second part, we extend this minimal-world semantics for answering metric temporal conjunctive queries with negation over the lightweight temporal logic 'Equation Presented' and obtain similar rewritability and complexity results. This paper is under consideration in theory and practice of logic programming (TPLP). Copyright © 2021, The Authors. All rights reserved.

关键词： Ontology

来源：评论

学校读者我要写书评

暂无评论

Operating room (Re)scheduling with bed management via ASP

arXiv

引用

arXiv 2021年

作者： Dodaro, Carmine Galatà, Giuseppe Khan, Muhammad Kamran Maratea, Marco Porro, Ivan University of Calabria Italy SurgiQ srl Italy University of Genoa Italy

The Operating Room Scheduling (ORS) problem is the task of assigning patients to operating rooms, taking into account different specialties, lengths and priority scores of each planned surgery, operating room session durations, and the availability of beds for the entire length of stay both in the Intensive Care Unit and in the wards. A proper solution to the ORS problem is of primary importance for the healthcare service quality and the satisfaction of patients in hospital environments. In this paper we first present a solution to the problem based on Answer Set programming (ASP). The solution is tested on benchmarks with realistic sizes and parameters, on three scenarios for the target length on 5-day scheduling, common in small-medium sized hospitals, and results show that ASP is a suitable solving methodology for the ORS problem in such setting. Then, we also performed a scalability analysis on the schedule length up to 15 days, which still shows the suitability of our solution also on longer plan horizons. Moreover, we also present an ASP solution for the rescheduling problem, i.e. when the off-line schedule cannot be completed for some reason. Finally, we introduce a web framework for managing ORS problems via ASP that allows a user to insert the main parameters of the problem, solve a specific instance, and show results graphically in real-time. Under consideration in theory and practice of logic programming (TPLP).12. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：