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

Functional ASP with Intensional Sets: Application to Gelfond-Zhang Aggregates

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

作者： Cabalar, Pedro Fadinno, Jorge Del Cerro, Luis Farinas Pearce, David Univ A Coruna Dept Comp Sci Corunna Spain Univ Toulouse CNRS IRIT Toulouse France Univ Politecn Madrid Madrid Spain

In this paper, we propose a variant of Answer Set programming (ASP) with evaluable functions that extends their application to sets of objects, something that allows a fully logical treatment of aggregates. Formally, we start from the syntax of First Order logic with equality and the semantics of Quantified Equilibrium logic with evaluable functions (QEL(F)(=)). Then, we proceed to incorporate a new kind of logical term, intensional set (a construct commonly used to denote the set of objects characterised by a given formula), and to extend QEL(F)(=) semantics for this new type of expression. In our extended approach, intensional sets can be arbitrarily used as predicate or function arguments or even nested inside other intensional sets, just as regular first-order logical terms. As a result, aggregates can be naturally formed by the application of some evaluable function (count, sum, maximum, etc) to a set of objects expressed as an intensional set. This approach has several advantages. First, while other semantics for aggregates depend on some syntactic transformation (either via a reduct or a formula translation), the QEL(F)(=) interpretation treats them as regular evaluable functions, providing a compositional semantics and avoiding any kind of syntactic restriction. Second, aggregates can be explicitly defined now within the logical language by the simple addition of formulas that fix their meaning in terms of multiple applications of some (commutative and associative) binary operation. For instance, we can use recursive rules to define sum in terms of integer addition. Last, but not least, we prove that the semantics we obtain for aggregates coincides with the one defined by Gelfond and Zhang for the Alog language, when we restrict to that syntactic fragment.

关键词： Answer Set programming Equilibrium logic Partial Functions Aggregates

来源：评论

学校读者我要写书评

暂无评论

Symbolic Execution for JavaScript 18

Symbolic Execution for JavaScript

引用

20th International Symposium on Principles and practice of Declarative programming (PPDP)

作者： Santos, Jose Fragoso Maksimovic, Petar Grohens, Theotime Dolby, Julian Gardner, Philippa Imperial Coll London London England ENS Paris Paris France IBM Res New York NY USA

ISBN: (纸本)9781450364416

We present a framework for trustworthy symbolic execution of JavaScripts programs, whose aim is to assist developers in the testing of their code: the developer writes symbolic tests for which the framework provides concrete counter-models. We create the framework following a new, general methodology for designing compositional program analyses for dynamic languages. We prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to whole-program symbolic testing of real-world JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs.

关键词： Symbolic execution Separation logic Formal semantics JavaScript

来源：评论

学校读者我要写书评

暂无评论

Solving the shifts and breaks design problem using integer linear programming 12

Solving the shifts and breaks design problem using integer l...

引用

12th International Conference on the practice and theory of Automated Timetabling, PATAT 2018

作者： Akkermans, Arjan Post, Gerhard Uetz, Marc Department of Applied Mathematics University of Twente P.O. Box 217 Enschede Netherlands ORTEC Optimization Technology Houtsingel 5 Zoetermeer Netherlands

ISBN: (纸本)9780992998424

In this paper we propose a two-phase approach to the shifts and breaks design problem using integer linear programming. In the first phase we create the shifts, while heuristically taking the breaks into account. In the second phase we assign breaks to each occurrence of any shift, one by one, repeating this until no improvement is found. This approach outperforms the current best known method for shifts and breaks design on a set of benchmark instances, as well as on real life instances. © PATAT 2018 Organizing Committee.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP

引用

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

作者： Dahlem, Marc Bhagyanath, Anoop Schneider, Klaus Insiders Technol GmbH Kaiserslautern Germany Univ Kaiserslautern Dept Comp Sci Kaiserslautern Germany

Conventional processor architectures are restricted in exploiting instruction level parallelism (ILP) due to the relatively low number of programmer-visible registers. Therefore, more recent processor architectures expose their datapaths so that the compiler (1) can schedule parallel instructions to different processing units and (2) can make effective use of local storage of the processing units. Among these architectures, the Synchronous Control Asynchronous Dataflow (SCAD) architecture is a new exposed datapath architecture whose processing units are equipped with first-in first-out (FIFO) buffers at their input and output ports. In contrast to register-based machines, the optimal code generation for SCAD is still a matter of research. In particular, SAT and SMT solvers were used to generate optimal resource constrained and optimal time constrained schedules for SCAD, respectively. As Answer Set programming (ASP) offers better flexibility in handling such scheduling problems, we focus in this paper on using an answer set solver for both resource and time constrained optimal SCAD code generation. As a major benefit of using ASP, we are able to generate all optimal schedules for a given program which allows one to study their properties. Furthermore, the experimental results of this paper demonstrate that the answer set solver can compete with SAT solvers and outperforms SMT solvers. This paper is under consideration for acceptance in TPLP.

关键词： Answer Set programming Exposed Datapath Architectures Optimal Scheduling Code Generation

来源：评论

学校读者我要写书评

暂无评论

Specifying and Verbalising Answer Set Programs in Controlled Natural Language

Specifying and Verbalising Answer Set Programs in Controlled...

引用

34th International Conference on logic programming (ICLP)

作者： Schwitter, Rolf Macquarie Univ Dept Comp Sydney NSW 2109 Australia

We show how a bi-directional grammar can be used to specify and verbalise answer set programs in controlled natural language. We start from a program specification in controlled natural language and translate this specification automatically into an executable answer set program. The resulting answer set program can be modified following certain naming conventions and the revised version of the program can then be verbalised in the same subset of natural language that was used as specification language. The bi-directional grammar is parametrised for processing and generation, deals with referring expressions, and exploits symmetries in the data structure of the grammar rules whenever these grammar rules need to be duplicated. We demonstrate that verbalisation requires sentence planning in order to aggregate similar structures with the aim to improve the readability of the generated specification. Without modifications, the generated specification is always semantically equivalent to the original one;our bi-directional grammar is the first one that allows for semantic round-tripping in the context of controlled natural language processing.

关键词： Bi-directional grammars controlled natural languages answer set programming sentence planning executable specifications

来源：评论

学校读者我要写书评

暂无评论

A Distributed Approach to LARS Stream Reasoning (System paper)

arXiv

引用

arXiv 2019年

作者： Eiter, Thomas Ogris, Paul Schekotihin, Konstantin Technische Universitt Wien Institut fr Logic and Computation KBS Group Alpen-Adria-Universitt Klagenfurt Austria

Stream reasoning systems are designed for complex decision-making from possibly infinite, dynamic streams of data. Modern approaches to stream reasoning are usually performing their computations using stand-alone solvers, which incrementally update their internal state and return results as the new portions of data streams are pushed. However, the performance of such approaches degrades quickly as the rates of the input data and the complexity of decision problems are growing. This problem was already recognized in the area of stream processing, where systems became distributed in order to allocate vast computing resources provided by clouds. In this paper we propose a distributed approach to stream reasoning that can efficiently split computations among different solvers communicating their results over data streams. Moreover, in order to increase the throughput of the distributed system, we suggest an interval-based semantics for the LARS language, which enables significant reductions of network traffic. Performed evaluations indicate that the distributed stream reasoning significantly outperforms existing stand-alone LARS solvers when the complexity of decision problems and the rate of incoming data are increasing. Under consideration for acceptance in theory and practice of logic programming. Copyright © 2019, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Periodic scheduling for MARTE/CCSL: theory and practice

引用

SCIENCE OF COMPUTER programming 2018年 154卷 42-60页

作者： Zhang, Min Dai, Feng Mallet, Frederic ECNU Shanghai Key Lab Trustworthy Comp Shanghai Peoples R China ECNU MoE Int Joint Lab Trustworthy Software Shanghai Peoples R China Univ Cote dAzur CNRS I3S Nice France INRIA Sophia Antipolis Mediterranee Valbonne France

The UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) is used to design and analyze real-time and embedded systems. The Clock Constraint Specification Language (CCSL) is a companion language for MARTE. It introduces logical clocks as first class citizens as a way to formally specify the expected behavior of models, thus allowing formal verification. CCSL describes the expected infinite behaviors of reactive embedded systems. In this paper we introduce and focus on the notion of periodic schedule to allow for a nice finite abstraction of these infinite behaviors. After studying the theoretical properties of those schedules we give a practical way to deal with them based on the executable operational semantics of CCSL in rewriting logic with Maude. We also propose an algorithm to find automatically periodic schedulers with the proposed sufficient condition, and to perform formal analysis of CCSL constraints by means of customized simulation and bounded LTL model checking. (C) 2017 Elsevier B.V. All rights reserved.

关键词： Periodic scheduling MARTE/CCSL Maude Rewriting logic Model checking

来源：评论

学校读者我要写书评

暂无评论

Constraint-Based Inference in Probabilistic logic Programs

Constraint-Based Inference in Probabilistic Logic Programs

引用

34th International Conference on logic programming (ICLP)

作者： Nampally, Arun Zhang, Timothy Ramakrishnan, C. R. SUNY Stony Brook Dept Comp Sci Stony Brook NY 11794 USA

Probabilistic logic Programs (PLPs) generalize traditional logic programs and allow the encoding of models combining logical structure and uncertainty. In PLP, inference is performed by summarizing the possible worlds which entail the query in a suitable data structure, and using this data structure to compute the answer probability. Systems such as ProbLog, PITA, etc., use propositional data structures like explanation graphs, BDDs, SDDs, etc., to represent the possible worlds. While this approach saves inference time due to substructure sharing, there are a number of problems where a more compact data structure is possible. We propose a data structure called Ordered Symbolic Derivation Diagram (OSDD) which captures the possible worlds by means of constraint formulas. We describe a program transformation technique to construct OSDDs via query evaluation, and give procedures to perform exact and approximate inference over OSDDs. Our approach has two key properties. Firstly, the exact inference procedure is a generalization of traditional inference, and results in speedup over the latter in certain settings. Secondly, the approximate technique is a generalization of likelihood weighting in Bayesian Networks, and allows us to perform sampling-based inference with lower rejection rate and variance. We evaluate the effectiveness of the proposed techniques through experiments on several problems.

关键词： Data structures

来源：评论

学校读者我要写书评

暂无评论

Stepwise debugging of answer-set programs

引用

theory and practice of logic programming 2018年第1期18卷 30-80页

作者： Oetsch, Johannes Puehrer, Joerg Tompits, Hans Tech Univ Wien Inst Informat Syst 184 3 Favoritenstr 9-11 A-1040 Vienna Austria Univ Leipzig Inst Informat Augustuspl 10 D-04109 Leipzig Germany

We introduce a stepping methodology for answer-set programming (ASP) that allows for debugging answer-set programs and is based on the stepwise application of rules. Similar to debugging in imperative languages, where the behaviour of a program is observed during a step-by-step execution, stepping for ASP allows for observing the effects that rule applications have in the computation of an answer set. While the approach is inspired from debugging in imperative programming, it is conceptually different to stepping in other paradigms due to non-determinism and declarativity that are inherent to ASP. In particular, unlike statements in an imperative program that are executed following a strict control flow, there is no predetermined order in which to consider rules in ASP during a computation. In our approach, the user is free to decide which rule to consider active in the next step following his or her intuition. This way, one can focus on interesting parts of the debugging search space. Bugs are detected during stepping by revealing differences between the actual semantics of the program and the expectations of the user. As a solid formal basis for stepping, we develop a framework of computations for answer-set programs. For fully supporting different solver languages, we build our framework on an abstract ASP language that is sufficiently general to capture different solver languages. To this end, we make use of abstract constraints as an established abstraction for popular language constructs such as aggregates. Stepping has been implemented in SeaLion, an integrated development environment for ASP. We illustrate stepping using an example scenario and discuss the stepping plugin of SeaLion. Moreover, we elaborate on methodological aspects and the embedding of stepping in the ASP development process.

关键词： answer-set programming debugging stepping program analysis

来源：评论

学校读者我要写书评

暂无评论

Constraint reformulation for nurse rostering problems 12

Constraint reformulation for nurse rostering problems

引用

12th International Conference on the practice and theory of Automated Timetabling, PATAT 2018

作者： Smet, Pieter KU Leuven Department of Computer Science CODeS and Imec Gebroeders De Smetstraat 1 Gent9000 Belgium

ISBN: (纸本)9780992998424

Various theoretical and empirical hardness studies have shown that constraints concerning the number of consecutive assignments make nurse rostering problems particularly difficult to solve. The present paper further explores this issue and builds upon recent computational insights by reformulating these constraints as subproblems which are known to have an efficient structure. By combining these subproblems together in a new integer programming formulation, the required calculation time to reach optimal solutions is significantly reduced using a standard integer programming solver. To gain a better understanding of these results, a characterization of problem instances for which the reformulation of challenging constraints works particularly well is provided. © PATAT 2018 Organizing Committee.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：