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

Predicate Pairing for program verification

theory and practice of logic programming 2018年第2期18卷 126-166页

作者： De Angelis, Emanuele Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio G dAnnunzio Univ Chieti Pescara DEC Pescara Italy Univ Roma Tor Vergata DICII Rome Italy CNR IASI Rome Italy

It is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for constrained Horn clauses (or CHC solvers) based on predicate abstraction are sometimes unable to verify satisfiability because they look for models that are definable in a given class A of constraints, called A-definable models. We introduce a transformation technique, called Predicate Pairing, which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an A-definable model, and hence can be effectively verified by a state-of-the-art CHC solver. In particular, we prove that, under very general conditions on A, the unfold/fold transformation rules preserve the existence of an A-definable model, that is, if the original clauses have an A-definable model, then the transformed clauses have an A-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an A-definable model if and only if the original ones have an A-definable model. Then, we present a strategy, called Predicate Pairing, which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability problem can be solved by looking for A-definable models. The Predicate Pairing (PP) strategy introduces a new predicate defined by the conjunction of two predicates occurring in the original set of clauses, together with a conjunction of constraints. We will show through some examples that an A-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We will also present some case studies showing that Predicate Pairing plays a crucial role in the verification of relational properties of programs, that is, properties relating two programs (such as

关键词： program verification constrained Horn clauses constraint logic programming program transformation relational properties of programs

来源：评论

学校读者我要写书评

暂无评论

Exploiting Answer Set programming with External Sources for Meta-Interpretive Learning

引用

theory and practice of logic programming 2018年第3-4期18卷 571-588页

作者： Kaminski, Tobias Eiter, Thomas Inoue, Katsumi Tech Univ Vienna TU Wien Vienna Austria Natl Inst Informat Tokyo Japan

Meta-Interpretive Learning (MIL) learns logic programs from examples by instantiating meta-rules, which is implemented by the Metagol system based on Prolog. Viewing MIL-problems as combinatorial search problems, they can alternatively be solved by employing Answer Set programming (ASP), which may result in performance gains as a result of efficient conflict propagation. However, a straightforward ASP-encoding of MIL results in a huge search space due to a lack of procedural bias and the need for grounding. To address these challenging issues, we encode MIL in the HEX-formalism, which is an extension of ASP that allows us to outsource the background knowledge, and we restrict the search space to compensate for a procedural bias in ASP. This way, the import of constants from the background knowledge can for a given type of meta-rules be limited to relevant ones. Moreover, by abstracting from term manipulations in the encoding and by exploiting the HEX interface mechanism, the import of such constants can be entirely avoided in order to mitigate the grounding bottleneck. An experimental evaluation shows promising results.

关键词： Inductive logic programming Meta-Interpretive Learning Answer Set programming

来源：评论

学校读者我要写书评

暂无评论

Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using logic programming

引用

theory and practice of logic programming 2018年第3-4期18卷 656-672页

作者： Thanh Hai Nguyen Pontelli, Enrico Tran Cao Son New Mexico State Univ Dept Comp Sci Las Cruces NM 88003 USA

Evolutionary Biologists have long struggled with the challenge of developing analysis workflows in a flexible manner, thus facilitating the reuse of phylogenetic knowledge. An evolutionary biology workflow can be viewed as a plan which composes web services that can retrieve, manipulate, and produce phylogenetic trees. The Phylotastic project was launched two years ago as a collaboration between evolutionary biologists and computer scientists, with the goal of developing an open architecture to facilitate the creation of such analysis workflows. While composition of web services is a problem that has been extensively explored in the literature, including within the logic programming domain, the incarnation of the problem in Phylotastic provides a number of additional challenges. Along with the need to integrate preferences and formal ontologies in the description of the desired workflow, evolutionary biologists tend to construct workflows in an incremental manner, by successively refining the workflow, by indicating desired changes (e.g., exclusion of certain services, modifications of the desired output). This leads to the need of successive iterations of incremental replanning, to develop a new workflow that integrates the requested changes while minimizing the changes to the original workflow. This paper illustrates how Phylotastic has addressed the challenges of creating and refining phylogenetic analysis workflows using logic programming technology and how such solutions have been used within the general framework of the Phylotastic project.

关键词： Bioinformatics workflows web services planning composition re-composition similarity quality of service

来源：评论

学校读者我要写书评

暂无评论

Incremental Answer Set programming with Overgrounding

arXiv

引用

arXiv 2019年

作者： Calimeri, Francesco Ianni, Giovambattista Pacenza, Francesco Perri, Simona Zangari, Jessica Department of Mathematics and Computer Science University of Calabria 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. This paper is under consideration in theory and practice of logic programming (TPLP). Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples

Incremental and Iterative Learning of Answer Set Programs fr...

引用

34th International Conference on logic programming (ICLP)

作者： Mitra, Arindam Baral, Chitta Arizona State Univ Tempe AZ 85287 USA

Over the years the Artificial Intelligence (AI) community has produced several datasets which have given the machine learning algorithms the opportunity to learn various skills across various domains. However, a subclass of these machine learning algorithms that aimed at learning logic programs, namely the Inductive logic programming algorithms, have often failed at the task due to the vastness of these datasets. This has impacted the usability of knowledge representation and reasoning techniques in the development of AI systems. In this research, we try to address this scalability issue for the algorithms that learn answer set programs. We present a sound and complete algorithm which takes the input in a slightly different manner and performs an efficient and more user controlled search for a solution. We show via experiments that our algorithm can learn from two popular datasets from machine learning community, namely bAbl (a question answering dataset) and MNIST (a dataset for handwritten digit recognition), whicYh to the best of our knowledge was not previously possible. The system is publicly available at https://***/KdWAcV.

关键词： Inductive logic programming Answer Set programming Question Answering Handwritten Digit Recognition Context Dependent Learning

来源：评论

学校读者我要写书评

暂无评论

Action-centered information retrieval

arXiv

引用

arXiv 2019年

作者： BALDUCCINI, MARCELLO LEBLANC, EMILY C. Saint Joseph's University Drexel University

Information Retrieval (IR) aims at retrieving documents that are most relevant to a query provided by a user. Traditional techniques rely mostly on syntactic methods. In some cases, however, links at a deeper semantic level must be considered. In this paper, we explore a type of IR task in which documents describe sequences of events, and queries are about the state of the world after such events. In this context, successfully matching documents and query requires considering the events' possibly implicit, uncertain effects and side-effects. We begin by analyzing the problem, then propose an action language based formalization, and finally automate the corresponding IR task using Answer Set programming. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

引用

theory and practice of logic programming 2018年第3-4期18卷 484-501页

作者： Farka, Frantisek Komendantskya, Ekaterina Hammond, Kevin Univ St Andrews St Andrews Fife Scotland Heriot Watt Univ Edinburgh Midlothian Scotland

First-order resolution has been used for type inference for many years, including in Hindley-Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method.

关键词： Proof-relevant logic Horn clauses Dependent types Type Inference Proof-relevant resolution

来源：评论

学校读者我要写书评

暂无评论

Relating two dialects of answer set programming

arXiv

引用

arXiv 2019年

作者： Harrison, Amelia Lifschitz, Vladimir Google Singapore University of Texas Austin Singapore

The input language of the answer set solver CLINGO is based on the definition of a stable model proposed by Paolo Ferraris. The semantics of the ASP-Core language, developed by the ASP Standardization Working Group, uses the approach to stable models due to Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. The two languages are based on different versions of the stable model semantics, and the ASP-Core document requires, "for the sake of an uncontroversial semantics," that programs avoid the use of recursion through aggregates. In this paper we prove that the absence of recursion through aggregates does indeed guarantee the equivalence between the two versions of the stable model semantics, and show how that requirement can be relaxed without violating the equivalence property. The paper is under consideration for publication in theory and practice of logic programming. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Exploiting Answer Set programming with External Sources for Meta-Interpretive Learning

Exploiting Answer Set Programming with External Sources for ...

引用

34th International Conference on logic programming (ICLP)

作者： Kaminski, Tobias Eiter, Thomas Inoue, Katsumi Tech Univ Vienna TU Wien Vienna Austria Natl Inst Informat Tokyo Japan