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

Explanations as Programs in Probabilistic logic programming 1

16th international symposium on functional and logic programming (flops)

作者： Vidal, German Univ Politecn Valencia VRAIN Valencia Spain

ISBN: (数字)9783030994617

ISBN: (纸本)9783030994600;9783030994617

the generation of comprehensible explanations is an essential feature of modern artificial intelligence systems. In this work, we consider probabilistic logic programming, an extension of logic programming which can be useful to model domains with relational structure and uncertainty. Essentially, a program specifies a probability distribution over possible worlds (i.e., sets of facts). the notion of explanation is typically associated with that of a world, so that one often looks for the most probable world as well as for the worlds where the query is true. Unfortunately, such explanations exhibit no causal structure. In particular, the chain of inferences required for a specific prediction (represented by a query) is not shown. In this paper, we propose a novel approach where explanations are represented as programs that are generated from a given query by a number of unfolding-like transformations. Here, the chain of inferences that proves a given query is made explicit. Furthermore, the generated explanations are minimal (i.e., contain no irrelevant information) and can be parameterized w.r.t. a specification of visible predicates, so that the user may hide uninteresting details from explanations.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Proving partial-correctness and invariance properties of transition-system models

引用

SCIENCE OF COMPUTER programming 2020年 186卷 102342-000页

作者： Rusu, Vlad Grimaud, Gilles Hauspie, Michael INRIA Lille France Univ Lille Lille France

We propose an approach for proving partial-correctness and invariance properties of transition systems, and illustrate it on a model of a security hypervisor. Regarding partial correctness, we generalise the recently introduced formalism of Reachability logic, currently used as a language-parametric logic for programs, to transition systems. We propose a coinductive proof system for the resulting logic, which can be seen as performing an "infinite symbolic execution" of the transition-system model under verification. We embed the proof system in the Coq proof assistant and formally prove its soundness and completeness. the soundness result provides us with a Coq-certified Reachability-logic prover for transition-system models. the completeness result, although more theoretical in nature, also has a practical value, as it suggests a proof strategy that is able to deal with all valid formulas on a given transition system. the complete proof strategy reduces partial correctness to invariance. For the latter we propose an incremental verification technique for dealing with the case-explosion problem that is known to affect it. All these combined techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in a simple hypervisor that we designed in earlier work meets its expected functional requirements. (C) 2019 Elsevier B.V. All rights reserved.

关键词： Formal verification Coinduction Coq proof assistant Reachability logic Hypervisor

来源：评论

学校读者我要写书评

暂无评论

Formal Verification of Parallel Prefix Sum 12th

Formal Verification of Parallel Prefix Sum

引用

12th international NASA Formal Methods symposium (NFM)

作者： Safari, Mohsen Oortwijn, Wytse Joosten, Sebastiaan Huisman, Marieke Univ Twente Formal Methods & Tools Enschede Netherlands Swiss Fed Inst Technol Dept Comp Sci Zurich Switzerland

ISBN: (纸本)9783030557539;9783030557546

With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. this means, the algorithm should be functionally correct, and the implementation should be thread and memory safe. In this paper, we use deductive program verification based on permission-based separation logic, as supported by VerCors, to show correctness of the two most frequently used parallel in-place prefix sum algorithms for an arbitrary array size. Interestingly, the correctness proof for the second algorithm reuses the auxiliary lemmas that we needed to create the first proof. To the best of our knowledge, this paper is the first tool-supported verification of functional correctness of the two parallel in-place prefix sum algorithms which does not make any assumption about the size of the input array.

关键词： GPU verification Deductive verification Separation logic

来源：评论

学校读者我要写书评

暂无评论

functional and logic programming - 12th international symposium, flops 2014, Proceedings

Functional and Logic Programming - 12th International Sympos...

引用

12th international symposium on functional and logic programming, flops 2014

ISBN: (纸本)9783319071503

the proceedings contain 21 papers. the topics discussed include: generating constrained random data with uniform distribution;guided type debugging;using big-step and small-step semantics in Maude to perform declarative debugging;Faustine: a vector Faust interpreter test bed for multimedia signal processing - system description;on cross-stage persistence in multi-stage programming;lightweight higher-kinded polymorphism;generic programming with multiple parameters;type-based amortized resource analysis with integers and arrays;type-based amortized resource analysis with integers and arrays;dynamic programming via thinning and incrementalization;proving correctness of compilers using structured graphs;and a new formalization of subtyping to match subclasses to subtypes.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Breaking Symmetries with Lex Implications 1

引用

14th international symposium on functional and logic programming (flops)

作者： Codish, Michael Ehlers, thorsten Gange, Graeme Itzhakov, Avraham Stuckey, Peter J. Ben Gurion Univ Negev Dept Comp Sci Beer Sheva Israel Univ Kiel Dept Comp Sci Kiel Germany Univ Melbourne Dept Comp & Informat Syst Melbourne Vic Australia Data61 CSIRO Melbourne Vic Australia

ISBN: (数字)9783319906867

ISBN: (纸本)9783319906867;9783319906850

Breaking symmetries is crucial when solving hard combinatorial problems. A common way to eliminate symmetries in CP/SAT is to add symmetry breaking constraints. Ideally, symmetry breaking constraints should be complete and compact. the aim of this paper is to find compact and complete symmetry breaks applicable when solving hard combinatorial problems using CP/SAT approach. In particular: graph search problems and matrix model problems where symmetry breaks are often specified in terms of lex constraints. We show that sets of lex constraints can be expressed with only a small portion of their inner lex implications which are a particular form of Horn clauses. We exploit this fact and compute a compact encoding of the row-wise LexLeader and state of the art partial symmetry breaking constraints. We illustrate the approach for graph search problems and matrix model problems.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Proving Partial-Correctness and Invariance Properties of Transition-System Models 12

Proving Partial-Correctness and Invariance Properties of Tra...

引用

international symposium on theoretical Aspects of Software Engineering (TASE)

作者： Rusu, Vlad Grimaud, Gilles Hauspie, Michael Inria Lille France Univ Lille Lille France

ISBN: (纸本)9781538673058

We propose a deductive verification approach for proving partial-correctness and invariance properties on transition-system models. Regarding partial correctness, we generalise the recently introduced formalism of Reachability logic, currently used as a language-parametric logic for programs, to transition systems. We propose a sound and relatively complete proof system for the resulting reachability logic. the soundness of the proof system is formally established in the Coq proof assistant, and the mechanised proof provides us with a Coq-certified Reachability-logic prover for transition-system models. the relative completeness of the proof system, although theoretical in nature, also has a practical value, as it induces a proof strategy that is guaranteed to prove all valid formulas on a given transition system. the strategy reduces partial-correctness verification to invariance verification;for the latter we propose an incremental technique in order to deal with the case-explosion problem that affects it. All these techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in security hypervisor that we designed in earlier work meets its expected functional requirements.

关键词： Coq Reachability logic Transition Systems

来源：评论

学校读者我要写书评

暂无评论

Preface for special section from flops 2014

引用

JOURNAL OF functional programming 2016年 26卷 e14-e14页

作者： Codish, Michael Sumii, Eijiro Ben Gurion Univ Negev Dept Comp Sci Beer Sheva Israel Tohoku Univ Grad Sch Informat Sci Sendai Miyagi Japan

the 12th international symposium on functional and logic programming was held in Kanazawa, Japan, June 4–6, 2014. the aim of the functional and logic programming series of conferences is to bring together researchers interested in declarative programming including functional programming and logic programming. the series aims to promote cross-fertilization and integration between the two paradigms and it is traditionally organized and held in Japan.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A probabilistic and timed verification approach of SysML state machine diagram

A probabilistic and timed verification approach of SysML sta...

引用

international symposium on programming and Systems (ISPS)

作者： Abdelhakim Baouya Djamal Bennouar Otmane Ait Mohamed Samir Ouchani CS Department Blida Saad Dahleb University Algeria CS Department Bouira University of Bouira Algeria ECE Department Montreal Concordia University Canada ECE Department University of Luxembourg Luxembourg

Timed-constrained and probabilistic verification approaches gain a great importance in system behavior validation. they enable the evaluation of system behavior according to the design requirements and ensure their correctness before any implementation. In this paper, we propose a probabilistic and timed verification framework of State Machine diagrams extended with time and probability features. the approach consists on mapping the extended State Machine diagram to its equivalent probabilistic timed automata that is expressed in PRISM language. To check the functional correctness of the system under test, the properties are expressed in PCTL temporal logic. We demonstrate the approach efficiency by analyzing performability properties on a Automatic Teller Machine (ATM) case study.

关键词： Unified modeling language Probabilistic logic Automata Real-time systems Junctions Clocks Model checking

来源：评论

学校读者我要写书评

暂无评论

Constraint logic programming for Hedges: A Semantic Reconstruction

Constraint Logic Programming for Hedges: A Semantic Reconstr...

引用

12th international symposium on functional and logic programming (flops)

作者： Dundua, Besik Florido, Mario Kutsia, Temur Marin, Mircea Univ Porto DCC FC Rua Campo Alegre 823 P-4100 Oporto Portugal Johannes Kepler Univ Linz RISC Linz Austria Ivane Javakhishvili Tbilisi State Univ VIAM Tbilisi Georgia W Univ Timisoara Timisoara Romania

ISBN: (纸本)9783319071510;9783319071503

We describe the semantics of CLP(H): constraint logic programming over hedges. Hedges are finite sequences of unranked terms, built over variadic function symbols and three kinds of variables: for terms, for hedges, and for function symbols. Constraints involve equations between unranked terms and atoms for regular hedge language membership. We give algebraic semantics of CLP(H) programs, define a sound, terminating, and incomplete constraint solver, and describe some fragments of constraints for which the solver returns a complete set of solutions.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

logic programming and logarithmic space 12

Logic programming and logarithmic space

引用

12th Asian symposium on programming Languages and Systems, APLAS 2014

作者： Aubert, CléMent Bagnol, Marc Pistone, Paolo Seiller, thomas Aix Marseille Université CNRS Centrale Marseille I2M UMR 7373 Marseille13453 France I.H.É.S Le Bois-Marie 35 Route de Chartres Bures-sur-Yvette91440 France

ISBN: (纸本)9783319127354

We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof *** show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation. © Springer international Publishing Switzerland 2014.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：