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

作者： Brown, Chad E. Programming Systems Lab Universität des Saarlandes Campus E1 3 66123 Saarbrücken Germany

We describe a complete theorem proving procedure for higher-order logic that uses SAt-solving to do much of the heavy lifting. the theoretical basis for the procedure is a complete, cut-free, ground refutation calculus that incorporates a restriction on instantiations. the refined nature of the calculus makes it conceivable that one can search in the ground calculus itself, obtaining a complete procedure without resorting to meta-variables and a higher-order lifting lemma. Once one commits to searching in a ground calculus, a natural next step is to consider ground formulas as propositional literals and the rules of the calculus as propositional clauses relating the literals. With this view in mind, we describe a theorem proving procedure that primarily generates relevant formulas along with their corresponding propositional clauses. the procedure terminates when the set of propositional clauses is unsatisfiable. We prove soundness and completeness of the procedure. the procedure has been implemented in a new higher-order theorem prover, Satallax, which makes use of the SAt-solver MiniSat. We also describe the implementation and give several examples. Finally, we include experimental results of Satallax on the higher-order part of the tPtP library. © 2013 Springer Science+Business Media Dordrecht.

关键词： theorem proving

来源：评论

学校读者我要写书评

暂无评论

Metalogue: A Multiperspective Multimodal Dialogue System with Metacognitive Abilities for Highly Adaptive and Flexible Dialogue Management

Metalogue: A Multiperspective Multimodal Dialogue System wit...

引用

International Conference on Intelligent Environments (IE)

作者： Jan Alexandersson Maria Aretoulaki Nick Campbell Michael Gardner Andrey Girenko Dietrich Klakow Dimitris Koryzis Volha Petukhova Marcus Specht Dimitris Spiliotopoulos Alexander Stricker Niels taatgen German Research Centre for Artificial Intelligence GmbH (DFKI) Saarbrücken Germany Interaction Design Lab University of Peloponnese Greece Department of Spoken Language Systems Universität des Saarlandes Saarbrücken Germany Hellenic Parliament Athens Greece Department of Artificial Intelligence University of Groningen Netherlands Teaching and Technology Open University of the Netherlands (OUNL) Trinity College School of Linguistic Speech and Communication Sciences Dublin Ireland DialogConnection Ltd Manchester UK Charamel GmbH Cologne Germany School of Computer Science and Electronic Engineering University of Essex UK

this poster paper presents a high-level description of the Metalogue project that is developing a multi-modal dialogue system that is able to implement interactive behaviors that seem natural to users and is flexible enough to exploit the full potential of multimodal interaction. We provide an outline of the initial work undertaken to define a an open architecture for the integrated Metalogue system. this system includes components that are necessary for the implementation of the processing stages for a variety of application domains: initialization, training, information gathering, orchestration, multimodality, dialogue management, speech recognition, speech synthesis and user modelling.

关键词： Educational institutions Computer architecture Speech Artificial intelligence Natural languages Context training

来源：评论

学校读者我要写书评

暂无评论

An Analysis of Anonymity Side Effects in the Internet of Services

An Analysis of Anonymity Side Effects in the Internet of Ser...

引用

International Conference and Workshops on Networked systems (NetSys)

作者： Ulrich Lampe André Miede tim Lusa Stefan Schulte Ralf Steinmetz Schahram Dustdar Multimedia Communications Lab (KOM) Technische Universität Darmstadt Darmstadt Germany Fakultät für Ingenieurwissenschaften HTW des Saarlandes Saarbrucken Germany Distributed Systems Group Vienna University of Technology Vienna Austria

the Internet of Services will facilitate cross-organizational collaboration by allowing companies to utilize services from external providers. Even though standard security mechanisms such as message encryption may be in place, attackers could create detailed profiles of service consumers, providers, and marketplaces by monitoring communication endpoints. this threatens the security objective of relationship anonymity and potentially permits sensitive information about the underlying business processes or relationships between service consumers and providers to be revealed. While state-of-the-art countermeasures in the form of anonymity systems allow this problem to be addressed, they may have undesired side effects on the Quality of Service. this work provides a detailed empirical analysis of these side effects, based on an extensive measurement of the response time, availability, and throughput of representative, globally distributed services. Our experimental results are available to the interested public within the comprehensive dataset WS-Anon.

关键词： Servers Web services Quality of service time factors throughput Availability

来源：评论

学校读者我要写书评

暂无评论

Multi-dimensional dependency grammar as multigraph description

Multi-dimensional dependency grammar as multigraph descripti...

引用

FLAIRS 2006 - 19th International Florida Artificial Intelligence Research Society Conference

作者： Debusmann, Ralph Smolka, Gert Programming Systems Lab Universität des Saarlandes Postfach 15 11 50 66041 Saarbrücken Germany

Extensible Dependency Grammar (XDG) is new, modular grammar formalism for natural language. An XDG analysis is a multi-dimensional dependency graph, where each dimension represents a different aspect of natural language, e.g. syntactic function, predicate-argument structure, information structure etc. thus, XDG brings together two recent trends in computational linguistics: the increased application of ideas from dependency grammar and the idea of multi-layered linguistic description. In this paper, we tackle one of the stumbling blocks of XDG so far - its incomplete formalization. We present the first complete formalization of XDG, as a description language for multigraphs based on simply typed lambda calculus. Copyright © 2006, American Association for Artificial Intelligence (***). All rights reserved.

关键词： Context sensitive grammars

来源：评论

学校读者我要写书评

暂无评论

Lexicalized syntax and topology for non-projective dependency grammar

Lexicalized syntax and topology for non-projective dependenc...

引用

Proceedings of the Joint Meeting of the 6th Conference on Formal Grammar and the 7th Conference on Mathematics of Language

作者： Duchier, Denys Programming Systems Lab Universität des Saarlandes Saarbrücken Germany

We propose a lexicalized formulation of dependency grammar that addresses both immediate dependence and linear precedence. Our approach distinguishes two orthogonal, yet mutually constraining dependency trees: an ID tree of syntactic dependencies and a LP tree of topological dependencies. the ID tree is non-ordered, non-projective and its edges are labeled by grammatical functions. the LP tree is ordered and projective and expresses licensed linearizations;its edges are labeled by topological fields. the LP tree can be regarded as deriving from the ID tree through a process of emancipation controlled by lexicalized constraints and principles. In the present article, we formalize valid ID/LP analyses and show how they can be characterized as the solutions of a constraint satisfaction problem. the latter can be solved by constraint programming and forms the basis of our implementation. © 2004 Published by Elsevier Science B.V.

关键词： Context free grammars

来源：评论

学校读者我要写书评

暂无评论

Lexicalized Syntax and topology for Non-projective Dependency Grammar

引用

Electronic Notes in theoretical Computer Science 2004年 53卷 70-80页

作者： Denys Duchier Programming Systems Lab Universität des Saarlandes Saarbrücken Germany

We propose a lexicalized formulation of dependency grammar that addresses both immediate dependence and linear precedence. Our approach distinguishes two orthogonal, yet mutually constraining dependency trees: an ID tree of syntactic dependencies and a LP tree of topological dependencies. the ID tree is non-ordered, non-projective and its edges are labeled by grammatical functions. the LP tree is ordered and projective and expresses licensed linearizations; its edges are labeled by topological fields. the LP tree can be regarded as deriving from the ID tree through a process of emancipation controlled by lexicalized constraints and principles. In the present article, we formalize valid ID/LP analyses and show how they can be characterized as the solutions of a constraint satisfaction problem. the latter can be solved by constraint programming and forms the basis of our implementation.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Configuration of labeled trees under Lexicalized Constraints and Principles

引用

Research on Language and Computation 2003年第3期1卷 307-336页

作者： Duchier, Denys Programming Systems Lab Universität des Saarlandes Saarbrücken Germany (E-mail

trees with labeled edges have widespread applicability, for examplefor the representation of dependency syntax trees. Given a fixednumber of nodes and constraints on how edges may be drawn betweenthem, the task of finding solution trees is known as a configurationproblem. In this paper, we formalize the configuration problem oflabeled trees and argue that it can be regarded as a constraintsatisfaction problem which can be solved directly and efficiently byconstraint propagation. In particular, we derive and prove correcta formulation of dependency parsing as a constraint satisfactionproblem. Our approach, based on constraints on finite sets and a new family of`selection' constraints, is especially well-suited for the compactrepresentation and efficient processing of ambiguity. We addressvarious issues of interest to the computational linguist such aslexical ambiguity, structural ambiguity, valency constraints,grammatical principles, and linear precedence. Finally we turn to thechallenge of efficient processing and characterize the servicesexpected of a constraint programming system: we define a formalconstraint language and specify its operational semantics withinference rules of propagation and distribution. this framework generalizes our presentation of immediate syntacticdependence for dependency parsing (Duchier, 1999a)and extends naturally to our corresponding treatment of linearprecedence (Duchier and Debusmann, 2001) based on a notion of topological ratherthan syntactic dependencies.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Processing Underspecified Semantic Representations in the Constraint Language for Lambda Structures

引用

Research on Language and Computation 2003年第1期1卷 127-169页

作者： Erk, Katrin Koller, Alexander Niehren, Joachim Programming Systems Lab Universität des Saarlandes Saarbrücken Germany (E-mail Department of Computational Linguistics Universität des Saarlandes Saarbrücken Germany (E-mail

the Constraint Language for Lambda Structures (CLLS)is an expressive language of tree descriptions which combinesdominance constraints with powerful parallelism and bindingconstraints. CLLS was introduced as a uniform framework for definingunderspecified semantics representations of natural languagesentences, covering scope, ellipsis, and anaphora. this articlepresents saturation-based algorithms for processing the completelanguage of CLLS. It also gives an overview of previous results on questions of processing and complexity.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Alice in the land of oz: An interoperability-based implementation of a functional language on top of a relational language

Alice in the land of oz: An interoperability-based implement...

引用

BABEL'01, First International Workshop on Multi-Language Infrastructure and Interoperability (Satellite Event of PLI 2001)

作者： Kornstaedt, Leif Programming Systems Lab Universität des Saarlandes Saarbrücken Germany

this paper reports practical experience in implementing Alice, an extension of Standard ML, on top of an existing implementation of Oz. this approach yields a high-quality implementation with little effort. the combination is an advanced programming system for both Oz and Alice, which offers more than either language on its own. Many thanks go to Ulrike Becker-Kornstaedt, thorsten Brunklaus, tobias Müller, and Christian Schulte for their comments on a previous version of this paper. For the numerous discussions regarding the details of the translation scheme, thanks go to Andreas Rossberg, implementor of the Alice compiler frontend. Finally, I'd like to thank the anonymous referees for their commments. © 2001 Published by Elsevier B.V.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Beta reduction constraints 1

引用

12th International Conference on Rewriting techniques and Applications, RtA 2001

作者： Bodirsky, Manuel Erk, Katrin Koller, Alexander Niehren, Joachim Programming Systems Lab Universität des Saarlandes Saarbrücken Germany Dept. of Computational Linguistics Universität des Saarlandes Saarbrücken Germany

ISBN: (数字)9783540451273

ISBN: (纸本)3540421173

the constraint language for lambda structures (CLLS) can model lambda terms that are known only partially. In this paper, we introduce beta reduction constraints to describe beta reduction steps between partially known lambda terms. We show that beta reduction constraints can be expressed in an extension of CLLS by group *** then extend a known semi-decision procedure for CLLS to also deal with group parallelism and thus with beta-reduction constraints. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Computers

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：