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

33rd international conference on Logic programming colocated with the 23rd international conference on principles and practice of constraint programming / 20th international conference on theory and Applications of Satisfiability Testing

作者： Lee, Joohyung Loney, Nikhil Meng, Yunsong Arizona State Univ Sch Comp Informat & Decis Syst Engn Tempe AZ 85281 USA Houzz Inc Palo Alto CA USA

Both hybrid automata and action languages are formalisms for describing the evolution of dynamic systems. this paper establishes a formal relationship between them. We show how to succinctly represent hybrid automata in an action language which in turn is defined as a high-level notation for answer set programming modulo theories-an extension of answer set programs to the firstorder level similar to the way satisfiability modulo theories (SMT) extends propositional satisfiability (SAT). We first show how to represent linear hybrid automata with convex invariants by an action language modulo theories. A further translation into SMT allows for computing them using SMT solvers that support arithmetic over reals. Next, we extend the representation to the general class of non-linear hybrid automata allowing even non-convex invariants. We represent them by an action language modulo ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present a prototype system CPLUS2ASPMT based on these translations, which allows for a succinct representation of hybrid transition systems that can be computed effectively by the state-of-the-art SMT solver dReal.

关键词： Answer set programming Action languages Hybrid automata

来源：评论

学校读者我要写书评

暂无评论

Productive corecursion in logic programming

引用

thEORY AND practice OF LOGIC programming 2017年第5-6期17卷 906-923页

作者： Komendantskaya, Ekaterina Li, Yue Heriot Watt Univ Edinburgh Midlothian Scotland

Logic programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/ coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. this intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing. Recently, an algorithm was presented that semi-decides a weaker property -of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper, we strengthen these recent results. We propose a method that semi-decides productivity of individual derivations for regular formulae. thus, we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. this is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.

关键词： Horn clauses (co) recursion (co) induction infinite term trees productivity

来源：评论

学校读者我要写书评

暂无评论

Representing hybrid automata by action language modulo theories

引用

thEORY AND practice OF LOGIC programming 2017年第5-6期17卷 924-941页

作者： Lee, Joohyung Loney, Nikhil Meng, Yunsong Arizona State Univ Sch Comp Informat & Decis Syst Engn Tempe AZ 85281 USA Houzz Inc Palo Alto CA USA

关键词： Answer set programming Action languages Hybrid automata

来源：评论

学校读者我要写书评

暂无评论

When you must forget: Beyond strong persistence when forgetting in answer set programming

When you must forget: Beyond strong persistence when forgett...

引用

作者： Goncalves, Ricardo Knorr, Matthias Leite, Joao Woltran, Stefan Univ Nova Lisboa NOVA LINCS Lisbon Portugal TU Wien Vienna Austria

Among the myriad of desirable properties discussed in the context of forgetting in Answer Set programming, strong persistence naturally captures its essence. Recently, it has been shown that it is not always possible to forget a set of atoms from a program while obeying this property, and a precise criterion regarding what can be forgotten has been presented, accompanied by a class of forgetting operators that return the correct result when forgetting is possible. However, it is an open question what to do when we have to forget a set of atoms, but cannot without violating this property. In this paper, we address this issue and investigate three natural alternatives to forget when forgetting without violating strong persistence is not possible, which turn out to correspond to the different possible relaxations of the characterization of strong persistence. Additionally, we discuss their preferable usage, shed light on the relation between forgetting and notions of relativized equivalence established earlier in the context of Answer Set programming, and present a detailed study on their computational complexity.

关键词： forgetting Answer Set programming strong equivalence relativized equivalence computational complexity

来源：评论

学校读者我要写书评

暂无评论

Productive corecursion in logic programming

Productive corecursion in logic programming

引用

作者： Komendantskaya, Ekaterina Li, Yue Heriot Watt Univ Edinburgh Midlothian Scotland

关键词： Horn clauses (co) recursion (co) induction infinite term trees productivity

来源：评论

学校读者我要写书评

暂无评论

When you must forget: Beyond strong persistence when forgetting in answer set programming

引用

thEORY AND practice OF LOGIC programming 2017年第5-6期17卷 837-854页

作者： Goncalves, Ricardo Knorr, Matthias Leite, Joao Woltran, Stefan Univ Nova Lisboa NOVA LINCS Lisbon Portugal TU Wien Vienna Austria

关键词： forgetting Answer Set programming strong equivalence relativized equivalence computational complexity

来源：评论

学校读者我要写书评

暂无评论

ACM international conference Proceeding Series

ACM International Conference Proceeding Series

引用

19th international Symposium on principles and practice of Declarative programming, PPDP 2017

ISBN: (纸本)9781450352918

the proceedings contain 20 papers. the topics discussed include: ethical issues in data management;programming by examples: applications, algorithms, and ambiguity resolution;environments and the complexity of abstract machines;conditional narrowing modulo SMT and axioms;attribute grammars with set attributes and global constraints as a unifying framework for planning domain models;shrink fast correctly!;function definitions for compound values in object-oriented languages;verifiable semantic difference languages;theory learning with symmetry breaking;copattern-matchings and first-class observations in OCaml, with a macro;practical evaluation of the lasp programming model at large scale - an experience report;selective unification in constraint logic programming;causally consistent reversible choreographies: a monitors-as-memories approach;machine fusion: merging merges, more or less;alpha-renaming of higher-order meta-expressions;characterization of strong normalizability for a sequent lambda calculus with co-control;defunctionalisation as modular closure conversion;a core calculus for provenance for provenance inspection;and expressive and strongly type-safe code generation.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Computing on many cores

Computing on many cores

引用

Euro-Par conference / 7th international Workshop on programming Models and Applications for Multicores and Manycores (PMAM) held in conjunction with the 21st SIGPLAN Symposium on principles and practice of Parallel programming (PPoPP)

作者： Goossens, Bernard Parello, David Porada, Katarzyna Rahmoune, Djallal UPVD DALI 52 Ave Paul Alduy F-66860 Perpignan 9 France UM2 CNRS UMR 5506 LIRMM 161 Rue Ada F-34095 Montpellier 5 France

this paper presents an alternative method to parallelize programs, better suited to manycore processors than actual operating system-/API-based approaches like OpenMP and MPI. the method relies on a parallelizing hardware and an adapted programming style. It frees and captures the instruction-level parallelism (ILP). A many-core design is presented in which cores are multithreaded and able to fork new threads. the programming style is based on functions. the hardware creates a concurrent thread at each function call. the programming style and the hardware create the conditions to free the ILP, by eliminating the architectural dependences between a call and its continuation after return. We illustrate the method on a sum reduction, a matrix multiplication and a sort. We measure the ILP of the parallel runs and show that it is high enough to feed thousands of cores because it increases with data size. We compare our method to pthread parallelization, showing that (1) our parallel execution is deterministic, (2) our thread management is cheap, (3) our parallelism is implicit, and (4) our method parallelizes functions and loops. Implicit parallelism makes parallel code easy to write and read. Deterministic parallel execution makes parallel code easy to debug.

关键词： computing model deterministic parallelism instruction level parallelism many-core processor multithreading parallelizing core

来源：评论

学校读者我要写书评

暂无评论

htd - A Free, Open-Source Framework for (Customized) Tree Decompositions and Beyond 14th

htd - A Free, Open-Source Framework for (Customized) Tree De...

引用

14th international conference on the Integration of Artificial Intelligence and Operations Research Techniques in constraint programming (CPAIOR)

作者： Abseher, Michael Musliu, Nysret Woltran, Stefan TU Wien Inst Informat Syst 184-2Favoritenstr 9-11 A-1040 Vienna Austria

ISBN: (纸本)9783319597768;9783319597751

Decompositions of graphs play a central role in the field of parameterized complexity and are the basis for many fixed-parameter tractable algorithms for problems that are NP-hard in general. Tree decompositions are the most prominent concept in this context and several tools for computing tree decompositions recently competed in the 1st Parameterized Algorithms and Computational Experiments Challenge. However, in practice the quality of a tree decomposition cannot be judged without taking concrete algorithms that make use of tree decompositions into account. In fact, practical experience has shown that generating decompositions of small width is not the only crucial ingredient towards efficiency. To this end, we present htd, a free and open-source software library, which includes efficient implementations of several heuristic approaches for tree decomposition and offers various features for normalization and customization of decompositions. the aim of this article is to present the specifics of htd together with an experimental evaluation underlining the effectiveness and efficiency of the implementation.

关键词： Tree decompositions Dynamic programming Software library

来源：评论

学校读者我要写书评

暂无评论

Argumentation-Based Semantics for Logic Programs with First-Order Formulae 19th

Argumentation-Based Semantics for Logic Programs with First-...

引用

19th international conference on principles and practice of Multi-Agent Systems (PRIMA)

作者： Phan Minh Dung Tran Cao Son Phan Minh thang Asian Inst Technol Dept Comp Sci Klongluang Thailand New Mexico State Univ Dept Comp Sci Las Cruces NM 88003 USA Burapha Univ Int Coll Dept Comp Sci Bangsaen Thailand

ISBN: (纸本)9783319448329;9783319448312

this paper studies different semantics of logic programs with first order formulae under the lens of argumentation framework. It defines the notion of an argumentation-based answer set and the notion of an argumentation-based well-founded model for programs with first order formulae. the main ideas underlying the new approach lie in the notion of a proof tree supporting a conclusion given a program and the observation that proof trees can be naturally employed as arguments in an argumentation framework whose stable extensions capture the program's well justified answer semantics recently introduced in [23]. the paper shows that the proposed approach to dealing with programs with first order formulae can be easily extended to a generalized class of logic programs, called programs with FOL-representable atoms, that covers various types of extensions of logic programming proposed in the literature such as weight constraint atoms, aggregates, and abstract constraint atoms. For example, it shows that argumentation-based well-founded model is equivalent to the well-founded model in [27] for programs with abstract constraint atoms. Finally, the paper relates the proposed approach to others and discusses possible extensions.

关键词： Logic programming formula Semantics semiotics Atoms Formal logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：