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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

1,409 篇 会议
50 篇 期刊文献
33 册 图书

馆藏范围

1,490 篇 电子文献
2 种 纸本馆藏

日期分布

学科分类号

1,116 篇 工学
- 855 篇 计算机科学与技术...
- 501 篇 软件工程
- 120 篇 电气工程
- 112 篇 控制科学与工程
- 83 篇 土木工程
- 77 篇 机械工程
- 74 篇 建筑学
- 67 篇 信息与通信工程
- 42 篇 动力工程及工程热...
- 41 篇 安全科学与工程
- 39 篇 材料科学与工程（可...
- 35 篇 仪器科学与技术
- 33 篇 交通运输工程
- 31 篇 化学工程与技术
- 31 篇 石油与天然气工程
- 29 篇 水利工程
- 23 篇 力学（可授工学、理...
- 23 篇 生物医学工程（可授...
- 22 篇 电子科学与技术（可...
316 篇 理学
- 194 篇 数学
- 63 篇 系统科学
- 55 篇 统计学（可授理学、...
- 43 篇 物理学
- 38 篇 化学
- 30 篇 生物学
198 篇 管理学
- 143 篇 管理科学与工程(可...
- 81 篇 工商管理
- 71 篇 图书情报与档案管...
35 篇 经济学
- 35 篇 应用经济学
28 篇 医学
26 篇 法学
- 24 篇 社会学
23 篇 教育学
9 篇 文学
7 篇 农学
3 篇 艺术学
2 篇 军事学

主题

60 篇 model checking
42 篇 tools
28 篇 static analysis
27 篇 data mining
24 篇 algorithm design...
23 篇 analytical model...
21 篇 stochastic syste...
21 篇 artificial intel...
20 篇 software enginee...
18 篇 semantics
17 篇 real time system...
17 篇 visualization
16 篇 hybrid systems
15 篇 computer archite...
15 篇 big data
15 篇 feature extracti...
15 篇 hardware
15 篇 mathematical mod...
14 篇 machine learning
14 篇 software

机构

12 篇 ludwig maximilia...
7 篇 univ illinois ur...
7 篇 univ twente form...
7 篇 univ penn philad...
6 篇 tech univ munich...
4 篇 verimag ctr equa...
4 篇 rhein westfal th...
4 篇 natl aerosp univ...
4 篇 department of co...
4 篇 suny stony brook...
3 篇 saarland univ sa...
3 篇 university of wa...
3 篇 vienna universit...
3 篇 univ colorado bo...
3 篇 university colle...
3 篇 rwth aachen univ...
3 篇 carnegie mellon ...
3 篇 chinese acad sci...
3 篇 univ oxford dept...
3 篇 iowa state univ ...

作者

13 篇 beyer dirk
8 篇 parker david
8 篇 katoen joost-pie...
8 篇 kwiatkowska mart...
7 篇 hermanns holger
6 篇 yi w
5 篇 majumdar rupak
5 篇 podelski andreas
5 篇 van de pol jaco
5 篇 alur rajeev
5 篇 pettersson p
5 篇 norman gethin
4 篇 behrmann gerd
4 篇 kroening daniel
4 篇 neele thomas
4 篇 bozga marius
4 篇 abdulla parosh a...
4 篇 mateescu radu
4 篇 sharygina natash...
4 篇 groote jan friso

语言

1,438 篇 英文
30 篇 其他
15 篇 德文
7 篇 中文
2 篇 俄文

检索条件"任意字段=12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems"

共 1492 条记录，以下是1401-1410 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

Symbolic model checking for rectangular hybrid systems

Symbolic model checking for rectangular hybrid systems

引用

6th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2000 Held as Part of the Joint European conferences on theory and Practice of Software, ETAPS 2000

作者： Henzinger, thomas A. Majumdar, Rupak Department of Electrical Engineering and Computer Sciences University of California BerkeleyCA94720 United States

ISBN: (纸本)3540672826

An important case of hybrid systems are the rectangular automata. First, rectangular dynamics can naturally and arbitrarily closely approximate more general, nonlinear dynamics. Second, rectangular automata are the most general type of hybrid systems for which model checking-in particular, LTL model checking-is decidable. However, on one hand, the original proofs of decidability did not suggest practical algorithms and, on the other hand, practical symbolic model-checking procedures-such as those implemented in HyTech-were not known to terminate on rectangular automata. We remedy this unsatisfactory situation: we present a symbolic method for LTL model checking which can be performed by HyTech and is guaranteed to terminate on all rectangular automata. We do so by proving that our method for symbolic Ltl model checking terminates on an infinite-state transition system if the trace-equivalence relation of the system has finite index, which is the case for all rectangular automata. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Hybrid systems

来源：评论

学校读者我要写书评

暂无评论

Support based measures applied to ice hockey scoring summaries

Support based measures applied to ice hockey scoring summari...

引用

international conference on tools for Artificial Intelligence (ICTAI)

作者： B.P. Kram J.A. Hall H.J. Hamilton Regina Univ. Sask. Canada University of Regina Regina SAS Canada

We present the hockey line extraction (HLE) algorithm, which examines ice hockey scoring summaries in an attempt to determine a team's lines. the players on a hockey team are divided into units called "lines" that appear together on the ice. the HLE algorithm uses single link clustering, support based measures and positional information to identify lines of players. the hockey lines software enables users to view relationships between players on a team based on time period and either support or confidence.

关键词： Data mining Clustering algorithms Ice Statistical analysis Statistics Data analysis Databases Position measurement Pattern analysis Gunshot detection systems

来源：评论

学校读者我要写书评

暂无评论

Local minimum structures of graph-coloring problems for stochastic constraint satisfaction algorithms

Local minimum structures of graph-coloring problems for stoc...

引用

international conference on tools for Artificial Intelligence (ICTAI)

作者： F. Mizuno S. Nishihara Institute of Information Sciences and Electronics University of Tsukuba Tsukuba Ibaraki Japan

Many stochastic search algorithms developed to solve large-scale constraint satisfaction problems in a practical time have the drawback of becoming stuck in locally minimal solutions which are not acceptable as solutions. We analyze a stochastic search algorithm from the viewpoint of local constraint structures of local minima. Using the graph-coloring problem with three colors, we studied the local graph structures around which concurrent conflicts arise. We present a key constraint structure, an LM pair; which may make up a local minimum, clarifying the mechanism of how conflicted coloring in an LM pair hinders stepwise refinement of hill-climbing. Experimental results show that LM pairs are strongly correlated with the search efficiency of the stochastic search algorithm.

关键词： Stochastic processes Large-scale systems Algorithm design and analysis Search problems Artificial intelligence Pattern analysis Computational complexity State-space methods Costs NP-complete problem

来源：评论

学校读者我要写书评

暂无评论

A Markov chain model checker

A Markov chain model checker

引用

6th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2000

作者： Hermanns, Holger Katoen, Joost-Pieter Meyer-Kayser, Joachim Siegle, Markus Formal Methods and Tools Group University of Twente P.O. Box 217 7500 AE Enschede Netherlands Lehrstuhl für Informatik 7 University of Erlangen-Nürnberg Martensstraße 3 91058 Erlangen Germany

ISBN: (纸本)3540672826

Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker (E MC2), where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of E MC2. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

An approach to incremental SVM learning algorithm

An approach to incremental SVM learning algorithm

引用

international conference on tools for Artificial Intelligence (ICTAI)

作者： Rong Xiao Jicheng Wang Fayan Zhang State Key Laboratory for Novel Software Technology Nanjing University of Posts and Telecommunications Nanjing China

the classification algorithm that is based on a support vector machine (SVM) is now attracting more attention, due to its perfect theoretical properties and good empirical results. In this paper, we first analyze the properties of the support vector (SV) set thoroughly, then introduce a new learning method, which extends the SVM classification algorithm to the incremental learning area. the theoretical basis of this algorithm is the classification equivalence of the SV set and the training set. In this algorithm, knowledge is accumulated in the process of incremental learning. In addition, unimportant samples are discarded optimally by a least-recently used (LRU) scheme. theoretical analyses and experimental results showed that this algorithm could not only speed up the training process, but it could also reduce the storage costs, while the classification precision is also guaranteed.

关键词： Support vector machines Support vector machine classification Algorithm design and analysis Learning systems Costs Laboratories Software algorithms Neural networks Pattern recognition Classification algorithms

来源：评论

学校读者我要写书评

暂无评论

Iterative analysis of markov regenerative models 11th

Iterative analysis of markov regenerative models

引用

11th international conference on Modelling tools and Techniques for Computer and Communication System Performance Evaluation, tools 2000

作者： German, Reinhard Technische Universität Berlin Prozeßdatenverarbeitung und Robotik Franklinstr. 28/29 Berlin10587 Germany

ISBN: (纸本)3540672605

Conventional algorithms for the steady-state analysis of Markov regenerative models suffer from high computational costs which are caused by densely populated matrices. In this paper a new algorithm is suggested which avoids to compute these matrices explicitly. Instead, a two-stage iteration scheme is used. An extended version of uniformization is applied as a subalgorithm to compute the required transient quantities "on-the fly". the algorithm is formulated in terms of stochastic Petri nets. A detailed example illustrates the proposed concepts. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Stochastic systems

来源：评论

学校读者我要写书评

暂无评论

Compositional state space generation with partial order reductions for asynchronous communicating systems

Compositional state space generation with partial order redu...

引用

作者： Krimm, Jean-Pierre Mounier, Laurent VERIMAG Joint Laboratory of CNRS UJF and INPG Centre Equation 2 avenue de Vignate GièresF-38610 France

ISBN: (纸本)3540672826

Compositional generation is an incremental technique for generating a reduced labelled transition system representing the behaviour of a set of communicating processes. In particular, since intermediate reductions can be performed after each generation step, the size of the LTs can be kept small and state-explosion can be av oided in many cases. this paper deals with compositional generation in presence of asynchronous communications via shared buffers. More precisely, we show how partial-order reduction techniques can be used in this context to define equivalence relations: that preserve useful properties, are congruence w.r.t asynchronous composition, and rely on a (syntactic) notion of preorder on execution sequences characterizing their "executability" in any buffer environment. Two such equivalences are proposed, together with dedicated asynchronous composition operators able to directly produce reduced LTs. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Artificial intelligence

来源：评论

学校读者我要写书评

暂无评论

Verification of parameterized systems using logic program transformations

Verification of parameterized systems using logic program tr...

引用

6th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2000

作者： Roychoudhury, Abhik Kumar, K. Narayan Ramakrishnan, C.R. Ramakrishnan, I.V. Smolka, Scott A. Dept. of Computer Science SUNY Stony Brook Stony Brook NY 11794 United States Chennai Mathematical Institute 92 G.N. Chetty Road Chennai India

ISBN: (纸本)3540672826

We show how the problem of verifying parameterized systems can be reduced to the problem of determining the equivalence of goals in a logic program. We further show how goal equivalences can be established using induction-based proofs. Such proofs rely on a powerful new theory of logic program transformations (encompassing unfold, fold and goal replacement over multiple recursive clauses), can be highly automated, and are applicable to a variety of network topologies, including uni- and bi-directional chains, rings, and trees of processes. Unfold transformations in our system correspond to algorithmic model-checking steps, fold and goal replacement correspond to deductive steps, and all three types of transformations can be arbitrarily interleaved within a proof. Our framework thus provides a seamless integration of algorithmic and deductive verification at fine levels of granularity. © Springer-Verlag Berlin Heidelberg 2000.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Vision based localisation for a mobile robot

Vision based localisation for a mobile robot

引用

international conference on tools for Artificial Intelligence (ICTAI)

作者： F. Gechter F. Charpillet Universite de Lorraine Nancy Lorraine FR

Presents a vision-based localisation system for a mobile robot that uses a representative set of images obtained during an initial exploration of the environment. this set of images makes it possible to represent the environment as a partially Markov decision process. the originality of this approach is the resulting data fusion process that uses both image matching and the decisions made by the robot in order to estimate the set of plausible positions of the robot and the associated probabilities. Image matching or recognition is achieved using principal components analysis.

关键词： Mobile robots Robot vision systems Principal component analysis Machine vision Vehicles Image matching Data mining Feature extraction Image processing Computational efficiency

来源：评论

学校读者我要写书评

暂无评论

Monitoring knowledge acquisition instead of evaluating knowledge bases 12th

引用

12th international conference on Knowledge Engineering and Knowledge Management

作者： Beydoun, G Hoffmann, A Univ New S Wales Sch Comp Sci & Engn Sydney NSW 2052 Australia

ISBN: (纸本)3540411194

Evaluating the success of a knowledge acquisition (KA) task is difficult and expensive. Most evaluation approaches rely on the expert themselves, either directly, or indirectly by relying on data previously prepared with the help of experts. In incremental KA, knowledge base (KB) errors are monitored and corrected by an expert. thus, during its evolution a record of the knowledge based system (KBS) performance is usually easy to keep. We propose to integrate with the incremental KA process, an evaluation process based on a statistical analysis to estimate the effectiveness of the KBS, as the KBS is actually evolved. We tailor such an analysis for Ripple Down Rules (RDR), which is an effective incremental KA methodology where a record of the KBS performance can be easily derived and updated as new cases are processed by the system. An RDR KB is a collection of rules with hierarchical exceptions, which are entered and validated by the expert in the context of their use. this greatly facilitates the knowledge maintenance task which, characteristically in RDR, overlaps with the incremental KA process. the work in this paper aims to overlap evaluation with maintenance and development of the knowledge base. It also minimises the major expense in deploying the RDR KBS, that of keeping a domain expert on-line during maintenance and the initial period of deployment. the expert is not kept on-line longer than it is absolutely necessary. We use the structure and semantics of an evolving RDR KB, combined with proven machine learning statistical methods, to estimate the added value in every KB update, as the KB evolves. Using these values, the decision-makers in the organisation employing the KBS can apply a cost-benefit analysis of the continuation of the incremental KA process. they can then determine when this process, involving keeping an expert on-line, should be terminated.

关键词： Learning systems

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共150页 << < 137 138 139 140 141 142 143 144 145 146 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：