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

作者： Gebser, Martin Kaufmann, Benjamin Schaub, Torsten Institut für Informatik Universität Potsdam Germany

Abstract We present the new multi-threaded version of the state-of-the-art answer set solver clasp. We detail its component and communication architecture and illustrate how they support the principal functionalities of clasp. Also, we provide some insights into the data representation used for different constraint types handled by clasp. All this is accompanied by an extensive experimental analysis of the major features related to multi-threading in clasp. © Cambridge University Press 2012.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Annotating answer-set programs in LANA

引用

theory and practice of logic programming 2012年第4-5期12卷 619-637页

作者： De Vos, Marina Kisa, Doga Gizem Oetsch, Johannes Puehrer, Joerg Tompits, Hans Univ Bath Dept Comp Bath BA2 7AY Avon England Sabanci Univ Fac Engn & Nat Sci TR-34956 Istanbul Turkey Vienna Univ Technol Inst Informat Syst 184 3 A-1040 Vienna Austria

While past research in answer-set programming (ASP) mainly focused on theory, ASP solver technology, and applications, the present work situates itself in the context of a quite recent research trend: development support for ASP. In particular, we propose to augment answer-set programs with additional meta-information formulated in a dedicated annotation language, called LANA. This language allows the grouping of rules into coherent blocks and to specify language signatures, types, pre- and postconditions, as well as unit tests for such blocks. While these annotations are invisible to an ASP solver, as they take the form of program comments, they can be interpreted by tools for documentation, testing, and verification purposes, as well as to eliminate sources of common programming errors by realising syntax checking or code completion features. To demonstrate its versatility, we introduce two such tools, viz. (i) ASPDOC, for generating an HTML documentation for a program based on the annotated information, and (ii) ASPUNIT, for running and monitoring unit tests on program blocks. LANA is also exploited in the SeaLion system, an integrated development environment for ASP based on Eclipse.

关键词： answer-set programming program annotations documentation unit testing

来源：评论

学校读者我要写书评

暂无评论

A Compositional Specification theory for Component Behaviours

A Compositional Specification Theory for Component Behaviour...

引用

21st European Symposium on programming (ESOP) held as Part of the 15th European Joint Conferences on theory and practice of Software (ETAPS)

作者： Chen, Taolue Chilton, Chris Jonsson, Bengt Kwiatkowska, Marta Univ Oxford Dept Comp Sci Oxford OX1 2JD England Uppsala Univ Dept Informat Technol S-75105 Uppsala Sweden

ISBN: (纸本)9783642288685;9783642288692

We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks.

关键词： specification theory compositionality components I/O automata interface automata logic LTS refinement conjunction quotient

来源：评论

学校读者我要写书评

暂无评论

Annotating answer-set programs in Lana

Annotating answer-set programs in Lana

引用

作者： De Vos, Marina Kisa, Doǧa Gizem Oetsch, Johannes Pührer, Jörg Tompits, Hans Department of Computing University of Bath BA2 7AY Bath United Kingdom Faculty of Engineering and Natural Sciences Sabanci University Orhanli Tuzla Istanbul 34956 Turkey Institut für Informationssysteme 184/3 Technische Universität Wien Favoritenstrae 9-11 A-1040 Vienna Austria

Abstract While past research in answer-set programming (ASP) mainly focused on theory, ASP solver technology, and applications, the present work situates itself in the context of a quite recent research trend: development support for ASP. In particular, we propose to augment answer-set programs with additional meta-information formulated in a dedicated annotation language, called Lana. This language allows the grouping of rules into coherent blocks and to specify language signatures, types, pre- and postconditions, as well as unit tests for such blocks. While these annotations are invisible to an ASP solver, as they take the form of program comments, they can be interpreted by tools for documentation, testing, and verification purposes, as well as to eliminate sources of common programming errors by realising syntax checking or code completion features. To demonstrate its versatility, we introduce two such tools, viz. (i) ASPDoc, for generating an HTML documentation for a program based on the annotated information, and (ii) ASPUnit, for running and monitoring unit tests on program blocks. Lana is also exploited in the SeaLion system, an integrated development environment for ASP based on Eclipse. © Cambridge University Press 2012.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Model checking with probabilistic tabled logic programming

Model checking with probabilistic tabled logic programming

引用

作者： Gorlin, Andrey Ramakrishnan, C.R. Smolka, Scott A. Department of Computer Science Stony Brook University Stony Brook NY 11794-4400 United States

Abstract We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queries with a finite number of explanations. This restriction prohibits the encoding of probabilistic model checkers, where explanations correspond to executions of the system being model checked. To overcome this restriction, we propose a more general inference algorithm that uses finite generative structures (similar to automata) to represent families of explanations. The inference algorithm computes the probability of a possibly infinite set of explanations directly from the finite generative structure. We have implemented our inference algorithm in XSB Prolog, and use this implementation to encode probabilistic model checkers for a variety of temporal logics, including PCTL and GPL (which subsumes PCTL*). Our experiment results show that, despite the highly declarative nature of their encodings, the model checkers constructed in this manner are competitive with their native implementations. © Cambridge University Press 2012.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them

引用

theory and practice of logic programming 2012年第4-5期12卷 775-791页

作者： Baral, Chitta Dzifcak, Juraj Gonzalez, Marcos A. Gottesman, Aaron Arizona State Univ Sch Comp Informat & Decis Syst Engn Tempe AZ 85287 USA

Our broader goal is to automatically translate English sentences into formulas in appropriate knowledge representation languages as a step towards understanding and thus answering questions with respect to English text. Our focus in this paper is on the language of Answer Set programming (ASP). Our approach to translate sentences to ASP rules is inspired by Montague's use of lambda calculus formulas as meaning of words and phrases. With ASP as the target language the meaning of words and phrases are ASP-lambda formulas. In an earlier work we illustrated our approach by manually developing a dictionary of words and their ASP-lambda formulas. However such an approach is not scalable. In this paper our focus is on two algorithms that allow one to construct ASP-lambda formulas in an inverse manner. In particular the two algorithms take as input two lambda-calculus expressions G and H and compute a lambda-calculus expression F such that F with input as G, denoted by F@G, is equal to H;and similarly G@F = H. We present correctness and complexity results about these algorithms. To do that we develop the notion of typed ASP-lambda calculus theories and their orders and use it in developing the completeness results.

关键词： natural language understanding answer set programming lambda calculus inverse lambda algorithms

来源：评论

学校读者我要写书评

暂无评论

A PSO-based adaptive fuzzy PID-controllers

引用

SIMULATION MODELLING practice AND theory 2012年 26卷 49-59页

作者： Chiou, Juing-Shian Tsai, Shun-Hung Liu, Ming-Tang So Taiwan Univ Dept Elect Engn Yung Kang 710 Tainan County Taiwan Natl Taipei Univ Technol Grad Inst Automat Technol Taipei 10608 Taiwan

In this paper, a novel design method for determining the optimal fuzzy PID-controller parameters of active automobile suspension system using the particle swarm optimization (PSO) reinforcement evolutionary algorithm is presented. This paper demonstrated in detail how to help the PSO with Q-learning cooperation method to search efficiently the optimal fuzzy-PID controller parameters of a suspension system. The design of a fuzzy system can be formulated as a search problem in high-dimensional space where each point represents a rule set, membership functions, and the corresponding system's behavior. In order to avoid obtaining the local optimum solution, we adopted a pure PSO global exploration method to search fuzzy-PID parameter. Later this paper explored the improved the limitation between suspension and tire deflection in active automobile suspension system with nonlinearity, which needs to be solved ride comfort and road holding ability problems, and so on. These studies presented many ideas to solve these existing problems, but they need much evolution time to obtain the solution. Motivated by above discussions this paper propose a novel algorithm which can decrease the number of evolution generation, and can also evolve the fuzzy system for obtaining a better performance. (C) 2012 Elsevier B.V. All rights reserved.

关键词： Fuzzy logic controllers (FLCs) Particle swarm optimization (PSO) Evolutionary programming (EP) Proportional-integral-derivative (PID) Q-learning Integral of Absolute Error (IAE) Membership functions

来源：评论

学校读者我要写书评

暂无评论

D-FLAT: Declarative problem solving using tree decompositions and answer-set programming

D-FLAT: Declarative problem solving using tree decomposition...

引用

作者： Bliem, Bernhard Morak, Michael Woltran, Stefan Institute of Information Systems 184/2 Vienna University of Technology Favoritenstrasse 9-11 1040 Vienna Austria

Abstract In this work, we propose Answer-Set programming (ASP) as a tool for rapid prototyping of dynamic programming algorithms based on tree decompositions. In fact, many such algorithms have been designed, but only a few of them found their way into implementation. The main obstacle is the lack of easy-to-use systems which (i) take care of building a tree decomposition and (ii) provide an interface for declarative specifications of dynamic programming algorithms. In this paper, we present D-FLAT, a novel tool that relieves the user of having to handle all the technical details concerned with parsing, tree decomposition, the handling of data structures, etc. Instead, it is only the dynamic programming algorithm itself which has to be specified in the ASP language. D-FLAT employs an ASP solver in order to compute the local solutions in the dynamic programming algorithm. In the paper, we give a few examples illustrating the use of D-FLAT and describe the main features of the system. Moreover, we report experiments which show that ASP-based D-FLAT encodings for some problems outperform monolithic ASP encodings on instances of small treewidth. © Cambridge University Press 2012.

关键词： Trees (mathematics)

来源：评论

学校读者我要写书评

暂无评论

logic programming: From underspecification to undefinedness

Logic programming: From underspecification to undefinedness

引用

theory of Computing 2012 - 18th Computing: The Australasian theory Symposium, CATS 2012

作者： Naish, Lee Søndergaard, Harald Horsfall, Benjamin Department of Computing and Information Systems University of Melbourne VIC 3010 Australia

ISBN: (纸本)9781921770098

The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood, but also for " undefined" The three-valued semantics proposed by Fitting and by Kunen are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued semantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the third truth value being associated with underspecification. Naish used an (apparently) novel " arrow" operator to relate the intended meaning of left and right sides of predicate definitions. In this paper we suggest that the additional truth values of Fitting/Kunen and Naish are best viewed as duals. We use Fitting's later four-valued approach to unify the two three-valued approaches. The additional truth value has very little affect on the Fitting three-valued semantics, though it can be useful when finding approximations to this semantics for program analysis. For the Naish semantics, the extra truth value allows intended interpretations to be more expressive, allowing us to verify and debug a larger class of programs. We also explain that the " arrow" operator of Naish (and our four-valued extension) is essentially the information ordering. This sheds new light on the relationships between specifications and programs, and successive executions states of a program. © 2012, Australian Computer Society, Inc.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Inference in probabilistic logic programs with continuous random variables

Inference in probabilistic logic programs with continuous ra...

引用

作者： Islam, Muhammad Asiful Ramakrishnan, C.R. Ramakrishnan, I.V. Department of Computer Science Stony Brook University Stony Brook NY 11794 United States

Abstract Probabilistic logic programming (PLP), exemplified by Sato and Kameya's PRISM, Poole's ICL, Raedt et al.'s ProbLog and Vennekens et al.'s LPAD, is aimed at combining statistical and logical knowledge representation and inference. However, the inference techniques used in these works rely on enumerating sets of explanations for a query answer. Consequently, these languages permit very limited use of random variables with continuous distributions. In this paper, we present a symbolic inference procedure that uses constraints and represents sets of explanations without enumeration. This permits us to reason over PLPs with Gaussian or Gamma-distributed random variables (in addition to discrete-valued random variables) and linear equality constraints over reals. We develop the inference procedure in the context of PRISM;however the procedure's core ideas can be easily applied to other PLP languages as well. An interesting aspect of our inference procedure is that PRISM's query evaluation process becomes a special case in the absence of any continuous random variables in the program. The symbolic inference procedure enables us to reason over complex probabilistic models such as Kalman filters and a large subclass of Hybrid Bayesian networks that were hitherto not possible in PLP frameworks. © Cambridge University Press 2012.

关键词： Random variables

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：