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

Better Paracoherent Answer Sets with Less Resources

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Amendola, Giovanni Dodaro, Carmine Ricca, Francesco University of Calabria Rende Italy

Answer Set programming (ASP) is a well-established formalism for logic programming. Problem solving in ASP requires to write an ASP program whose answers sets correspond to solutions. Albeit the nonexistence of answer sets for some ASP programs can be considered as a modeling feature, it turns out to be a weakness in many other cases, and especially for query answering. Paracoherent answer set semantics extend the classical semantics of ASP to draw meaningful conclusions also from incoherent programs, with the result of increasing the range of applications of ASP. State of the art implementations of paracoherent ASP adopt the semi-equilibrium semantics, but cannot be lifted straightforwardly to compute efficiently the (better) split semi-equilibrium semantics that discards undesirable semi-equilibrium models. In this paper an efficient evaluation technique for computing a split semi-equilibrium model is presented. An experiment on hard benchmarks shows that better paracoherent answer sets can be computed consuming less computational resources than existing methods. Under consideration for acceptance in TPLP. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

Control-flow refinement by partial evaluation, and its application to termination and cost analysis

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Doménech, Jesús J. Gallagher, John P. Genaim, Samir Universidad Complutense de Madrid Spain Roskilde University Denmark IMDEA Software Institute Spain

Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation;in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

Founded (auto)epistemic equilibrium logic satisfies epistemic splitting

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Fandinno, Jorge IRIT University of Toulouse CNRS France Universität Potsdam Germany

In a recent line of research, two familiar concepts from logic programming semantics (unfounded sets and splitting) were extrapolated to the case of epistemic logic programs. The property of epistemic splitting provides a natural and modular way to understand programs without epistemic cycles but, surprisingly, was only fulfilled by Gelfond’s original semantics (G91), among the many proposals in the literature. On the other hand, G91 may suffer from a kind of self-supported, unfounded derivations when epistemic cycles come into play. Recently, the absence of these derivations was also formalised as a property of epistemic semantics called foundedness. Moreover, a first semantics proved to satisfy foundedness was also proposed, the so-called Founded Autoepistemic Equilibrium logic (FAEEL). In this paper, we prove that FAEEL also satisfies the epistemic splitting property something that, together with foundedness, was not fulfilled by any other approach up to date. To prove this result, we provide an alternative characterisation of FAEEL as a combination of G91 with a simpler logic we called Founded Epistemic Equilibrium logic (FEEL), which is somehow an extrapolation of the stable model semantics to the modal logic S5. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

About epistemic negation and world views in Epistemic logic Programs

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Costantini, Stefania DISIM Università dell’Aquila Italy

In this paper we consider Epistemic logic Programs, which extend Answer Set programming (ASP) with "epistemic operators", and a recent approach to the semantics of such programs in terms of World Views. We propose some observations on the existence and number of world views. We exploit an extended ASP semantics in order to: (i) provide a novel characterization of world views;(ii) query world views and query the whole set of world views. This paper is under consideration for acceptance in TPLP Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

A rule-based system for explainable donor-patient matching in liver transplantation

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Aguado, Felicidad Muñiz, Brais Cabalar, Pedro Pérez, Gilberto Fandinno, Jorge Suárez, Francisco IRLab CITIC Research Center University of A Coruña Spain University of Potsdam Germany University of A Coruña Spain

In this paper we present web-liver, a rule-based system for decision support in the medical domain, focusing on its application in a liver transplantation unit for implementing policies for donor-patient matching. The rule-based system is built on top of an interpreter for logic programs with partial functions, called lppf, that extends the paradigm of Answer Set programming (ASP) adding two main features: (1) the inclusion of partial functions and (2) the computation of causal explanations for the obtained solutions. The final goal of web-liver is assisting the medical experts in the design of new donor-patient matching policies that take into account not only the patient severity but also the transplantation utility. As an example, we illustrate the tool behaviour with a set of rules that implement the utility index called SOFT. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

Discovering and proving invariants in answer set programming and planning

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Lühne, Patrick University of Potsdam Germany

Answer set programming (ASP) and planning are two widely used paradigms for solving logic programs with declarative programming. In both cases, the quality of the input programs has a major influence on the quality and performance of the solving or planning process. Hence, programmers need to understand how to make their programs efficient and still correct. In my PhD studies, I explore how input programs can be improved and verified automatically as a means to support programmers. One of my research directions consists in discovering invariants in planning programs without human support, which I implemented in a system called ginkgo. Studying dynamic systems in greater depth, I then developed plasp 3 with members of my research group, which is a significant step forward in effective planning in ASP. As a second research direction, I am concerned with automating the verification of ASP programs against formal specifications. For this joint work with Lifschitz’s group at the University of Texas, I developed a verification system called anthem. In my future PhD studies, I will extend my research concerning the discovery and verification of ASP and planning problems. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

Symbolic analysis of maude theories with narval

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Alpuente, María Escobar, Santiago Sapiña, Julia Ballis, Demis Universitat Politècnica de València DMIF University of Udine

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. This paper is under consideration for acceptance in TPLP. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

Investigating host-microbiota cooperation with gap-filling optimization problems

学校读者我要写书评

暂无评论

Investigating host-microbiota cooperation with gap-filling o...

作者： Clemence Frioux Universite de Rennes 1

学位级别：博士

Systems biology relies on computational biology to integrate knowledge and data, for a better understanding of organisms' physiology. Challenges reside in the applicability of methods and tools to non-model organisms, for instance in marine biology. Sequencing advances and the growing importance of elucidating microbiotas' roles, have led to an increased interest into these organisms. This thesis focuses on the modeling of the metabolism through networks, and of its functionality using graphs and constraints semantics. In particular, a first part presents work on gap-filling metabolic networks in the context of non-model organisms. A graph-based method is benchmarked and validated and a hybrid one is developed using Answer Set programming (ASP) and linear programming. Such gap-filling is applied on algae and extended to decipher putative interactions between Ectocarpus siliculosus and a symbiotic bacterium. In this direction, the second part of the thesis aims at proposing formalisms and implementation of a tool for selecting and screening communities of interest within microbiotas. It enables to scale to large microbiotas and, with a two-step approach, to suggest symbionts that fit the desired objective. The modeling supports the computation of exchanges, and solving can cover the whole solution space. Applications are presented on the human gut microbiota and the selection of bacterial communities for a brown alga. Altogether, this thesis proposes modeling, software and biological applications using graph-based semantics to support the elaboration of hypotheses for elucidating the metabolism of organisms.

关键词： logic programming metabolic networks microbiota ASP gap-filling modeling

Allen’s Interval Algebra makes the difference

学校读者我要写书评

暂无评论

arXiv 2019年

作者： Janhunen, Tomi Sioutis, Michael Department of Computer Science Aalto University Espoo Finland Computing Sciences Unit Tampere University Tampere Finland

Allen’s Interval Algebra constitutes a framework for reasoning about temporal information in a qualitative manner. In particular, it uses intervals, i.e., pairs of endpoints, on the timeline to represent entities corresponding to actions, events, or tasks, and binary relations such as precedes and overlaps to encode the possible configurations between those entities. Allen’s calculus has found its way in many academic and industrial applications that involve, most commonly, planning and scheduling, temporal databases, and healthcare. In this paper, we present a novel encoding of Interval Algebra using answer-set programming (ASP) extended by difference constraints, i.e., the fragment abbreviated as ASP(DL), and demonstrate its performance via a preliminary experimental evaluation. Although our ASP encoding is presented in the case of Allen’s calculus for the sake of clarity, we suggest that analogous encodings can be devised for other point-based calculi, too. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming