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

Call-By-Push-Value from a Linear logic Point of View 25th

Call-By-Push-Value from a Linear Logic Point of View

25th European Symposium on programming (ESOP) Held as Part of the European Joint Conferences on theory and practice of Software (ETAPS)

作者： Ehrhard, Thomas Univ Paris Diderot Sorbonne Paris Cite CNRS IRIFUMR 8243 F-75205 Paris France

ISBN: (纸本)9783662494981;9783662494974

We present and study a simple Call-By-Push-Value lambda-calculus with fix-points and recursive types. We explain its connection with Linear logic by presenting a denotational interpretation of the language in any model of Linear logic equipped with a notion of embedding retraction pairs. We consider the particular case of the Scott model of Linear logic from which we derive an intersection type system for our calculus and prove an adequacy theorem. Last, we introduce a fully polarized version of this calculus which turns out to be a term language for a large fragment of LLP and refines lambda-mu.

关键词： Calculations

来源：评论

学校读者我要写书评

暂无评论

The DLVHEX system for knowledge representation: recent advances (system description)

The DLVHEX system for knowledge representation...

引用

32nd International Conference on logic programming (ICLP)

作者： Redl, Christoph Vienna Univ Technol Inst Informat Syst Favoritenstr 9-11 A-1040 Vienna Austria

The DLVHEX system implements the hex-semantics, which integrates answer set programming (ASP) with arbitrary external sources. Since its first release ten years ago, significant advancements were achieved. Most importantly, the exploitation of properties of external sources led to efficiency improvements and flexibility enhancements of the language, and technical improvements on the system side increased user's convenience. In this paper, we present the current status of the system and point out the most important recent enhancements over early versions. While existing literature focuses on theoretical aspects and specific components, a bird's eye view of the overall system is missing. In order to promote the system for real-world applications, we further present applications which were already successfully realized on top of DLVHEX.

关键词： Answer Set programming Nonmonotonic Reasoning Knowledge representation

来源：评论

学校读者我要写书评

暂无评论

A Physician Advisory System for Chronic Heart Failure management based on knowledge patterns

A Physician Advisory System for Chronic Heart Failure manage...

引用

32nd International Conference on logic programming (ICLP)

作者： Chen, Zhuo Marple, Kyle Salazar, Elmer Gupta, Gopal Tamil, Lakshman Univ Texas Dallas Richardson TX 75083 USA

Management of chronic diseases such as chronic heart failure (CHF) is a major problem in health care. A standard approach followed by the medical community is to have a committee of experts develop guidelines that all physicians should follow. These guidelines typically consist of a series of complex rules that make recommendations based on a patient's information. Due to their complexity, often the guidelines are ignored or not complied with at all. It is not even clear whether it is humanly possible to follow these guidelines due to their length and complexity. For instance, for CHF, the guidelines run nearly eighty pages. In this paper we describe a physician-advisory system for CHF management that codes the entire set of clinical practice guidelines for CHF using answer set programming (ASP). Our approach is based on developing reasoning templates, that we call knowledge patterns, and using them to systemically code the clinical guidelines for CHF as ASP rules. Use of the knowledge patterns greatly facilitates the development of our system. Given a patient's medical information, our system generates a recommendation for treatment just as a human physician would, using the guidelines. Our system works even in the presence of incomplete information.

关键词： chronic disease management knowledge pattern answer set programming knowledge representation automated reasoning

来源：评论

学校读者我要写书评

暂无评论

Unary Resolution: Characterizing PTIME 19th

Unary Resolution: Characterizing PTIME

引用

19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) Held as Part of the European Joint Conferences on theory and practice of Software (ETAPS)

作者： Aubert, Clement Bagnol, Marc Seiller, Thomas Appalachian State Univ Dept Comp Sci Boone NC 28608 USA Univ Ottawa Dept Math & Stat Ottawa ON Canada Univ Copenhagen Dept Comp Sci Copenhagen Denmark

ISBN: (纸本)9783662496305;9783662496299

We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring, whose elements can be understood as logic programs or sets of rewriting rules over first-order terms. This construction stems from an interactive interpretation of the cut-elimination procedure of linear logic known as the geometry of interaction. This framework is restricted to terms (logic programs, rewriting rules) using only unary symbols, and this restriction is shown to be complete for polynomial time computation by encoding pushdown automata. Soundness w. r. t. Ptime is proven thanks to a saturation method similar to the one used for pushdown systems and inspired by the memoization technique. A Ptime-completeness result for a class of logic programming queries that uses only unary function symbols comes as a direct consequence.

关键词： Implicit complexity Unary queries logic programming Geometry of interaction Proof theory Pushdown automata Saturation Memoization

来源：评论

学校读者我要写书评

暂无评论

Assertion-based analysis via slicing with ABETS (system description)

引用

theory and practice of logic programming 2016年第5-6期16卷 515-532页

作者： Alpuente, M. Frechina, F. Sapina, J. Ballis, D. Univ Politecn Valencia Dept Sistemas Informat & Computac Camino VeraS-N E-46022 Valencia Spain Univ Udine Dipartimento Matemat & Informat Via Sci206 I-33100 Udine Italy

We present ABETS, an assertion-based, dynamic analyzer that helps diagnose errors in Maude programs. ABETS uses slicing to automatically create reduced versions of both a run's execution trace and executed program, reduced versions in which any information that is not relevant to the bug currently being diagnosed is removed. In addition, ABETS employs runtime assertion checking to automate the identification of bugs so that whenever an assertion is violated, the system automatically infers accurate slicing criteria from the failure. We summarize the main services provided by ABETS, which also include a novel assertion-based facility for program repair that generates suitable program fixes when a state invariant is violated. Finally, we provide an experimental evaluation that shows the performance and effectiveness of the system.

关键词： runtime assertion checking dynamic program and trace slicing program diagnosis and Debugging rewriting logic Maude

来源：评论

学校读者我要写书评

暂无评论

A mechanism of function calls in MSVL

引用

THEORETICAL COMPUTER SCIENCE 2016年 654卷 11-25页

作者： Zhang, Nan Duan, Zhenhua Tian, Cong Xidian Univ Inst Comp Theory & Technol Xian 710071 Peoples R China Xidian Univ ISN Lab Xian 710071 Peoples R China

Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and internal function calls. To do so, the syntax of function definitions and function calls is formalized. Then, the syntax of expressions in MSVL is extended by including function calls. Further, the evaluation rules are redefined. Moreover, the set of statements in MSVL is also extended and the semantics of function call statements is formalized. In addition, the existence of minimal models of MSVL programs involving new added statements is proved. Finally, an example is given to illustrate how to interpret function calls in practice with MSVL. (C) 2016 Elsevier B.V. All rights reserved.

关键词： Temporal logic programming Projection Function call Modeling Simulation Verification

来源：评论

学校读者我要写书评

暂无评论

Assertion-based analysis via slicing with ABETS (system description)

Assertion-based analysis via slicing with ABETS (s...

引用

32nd International Conference on logic programming (ICLP)

关键词： runtime assertion checking dynamic program and trace slicing program diagnosis and Debugging rewriting logic Maude

来源：评论

学校读者我要写书评

暂无评论

Correctness of compiling polymorphism to dynamic typing

引用

JOURNAL OF FUNCTIONAL programming 2017年 27卷 1-24页

作者： Hou (Favonia), Kuen-Bang Benton, Nick Harper, Robert Carnegie Mellon Univ Pittsburgh PA 15213 USA Microsoft Res Cambridge Cambridge Cambs England

The connection between polymorphic and dynamic typing was originally considered by Curry et al. (1972, Combinatory logic, vol. ii) in the form of "polymorphic type assignment" for untyped lambda-terms. Types are assigned after the fact to what is, in modern terminology, a dynamic language. Interest in type assignment was revitalized by the proposals of Bracha et al. (1998, OOPSLA) and Bank et al. (1997, POPL) to enrich Java with polymorphism (generics), which in turn sparked the development of other languages, such as Scala, with similar combinations of features. In such a setting, where the target language already has a monomorphic type system, it is desirable to compile polymorphism to dynamic typing in such a way that as much static typing as possible is preserved, relying on dynamics only insofar as genericity is actually required. The basic approach is to compile polymorphism using embeddings from each type into a universal "top" type, ID, and partial projections that go in the other direction. This scheme is intuitively reasonable, and, indeed, has been used in practice many times. Proving its correctness, however, is non-trivial. This paper studies the compilation of System F to an extension of Moggi's computational meta-language with a dynamic type and shows how the compilation may be proved correct using a logical relation.

关键词： Computation theory

来源：评论

学校读者我要写书评

暂无评论

Description and Optimization of Abstract Machines in a Dialect of Prolog

引用

theory and practice of logic programming 2016年第1期16卷 1-58页

作者： Morales, Jose F. Carro, Manuel Hermenegildo, Manuel IMDEA Software Inst Madrid Spain Tech Univ Madrid UPM Sch Comp Sci Madrid Spain

In order to achieve competitive performance, abstract machines for Prolog and related languages end up being large and intricate, and incorporate sophisticated optimizations, both at the design and at the implementation levels. At the same time, efficiency considerations make it necessary to use low-level languages in their implementation. This makes them laborious to code, optimize, and, especially, maintain and extend. Writing the abstract machine (and ancillary code) in a higher-level language can help tame this inherent complexity. We show how the semantics of most basic components of an efficient virtual machine for Prolog can be described using (a variant of) Prolog. These descriptions are then compiled to C and assembled to build a complete bytecode emulator. Thanks to the high-level of the language used and its closeness to Prolog, the abstract machine description can be manipulated using standard Prolog compilation and optimization techniques with relative ease. We also show how, by applying program transformations selectively, we obtain abstract machine implementations whose performance can match and even exceed that of state-of-the-art, highly-tuned, hand-crafted emulators.

关键词： Abstract machines compilation optimization program transformation prolog logic languages

来源：评论

学校读者我要写书评

暂无评论

Parameterised three-valued model checking

引用

SCIENCE OF COMPUTER programming 2016年 126卷 94-110页

作者： Timm, Nils Gruner, Stefan Univ Pretoria Dept Comp Sci ZA-0002 Pretoria South Africa

Three-valued abstraction is an established technique in software model checking. It proceeds by generating a state space model over the values true, false and unknown, where the latter value is used to represent the loss of information due to abstraction. Temporal logic properties can then be evaluated on such models. In case of an unknown result, the abstraction is iteratively refined until a definite result can be obtained. In this paper, we present and extend our work on parameterised three-valued model checking (PMC). In our parameterised three-valued models, unknown parts can be either associated with the constant value unknown or with expressions over boolean parameters. Our parameterisation is an alternative way to state that the truth value of certain predicates or transitions is actually not known and that the checked property has to yield the same result under each possible parameter instantiation. A specific feature of our approach is that it allows for establishing logical connections between parameters: While unknown parts in pure three-valued models are never related to each other, our parameterisation approach enables to represent facts like 'a certain pair of transitions has unknown but complementary truth values', or the value of a predicate is unknown but remains unchanged along all states of a certain path'. We demonstrate that such facts can be automatically derived from the system to be verified and that covering these facts in an abstract model can be crucial for the success and the efficiency of checking temporal logic safety and liveness properties. Parameterisation enhances the precision of three valued models without increasing their state space, but it leads to an exponential increase in time complexity, since any property of interest must be checked for each possible parameter instantiation. In this extended paper, we introduce a novel algorithm for direct parameterised three-valued model checking that straightly explores the parameterise

关键词： Three-valued logic Three-valued abstraction Parameterisation Model checking Counterexample-guided abstraction refinement

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：