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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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

分类表

所选分类

>> <<

限定检索结果

文献类型

358 篇 会议
2 篇 期刊文献

馆藏范围

360 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

238 篇 工学
- 235 篇 计算机科学与技术...
- 76 篇 软件工程
- 16 篇 电子科学与技术（可...
- 11 篇 电气工程
- 7 篇 信息与通信工程
- 7 篇 控制科学与工程
- 4 篇 机械工程
- 4 篇 动力工程及工程热...
- 2 篇 力学（可授工学、理...
- 2 篇 光学工程
- 2 篇 仪器科学与技术
- 2 篇 建筑学
- 2 篇 化学工程与技术
- 1 篇 材料科学与工程（可...
- 1 篇 土木工程
- 1 篇 农业工程
- 1 篇 环境科学与工程（可...
- 1 篇 生物工程
160 篇 理学
- 155 篇 数学
- 11 篇 统计学（可授理学、...
- 4 篇 物理学
- 1 篇 化学
- 1 篇 生物学
11 篇 管理学
- 8 篇 管理科学与工程(可...
- 8 篇 工商管理
- 2 篇 图书情报与档案管...
3 篇 教育学
- 3 篇 教育学
2 篇 经济学
- 2 篇 应用经济学
2 篇 法学
- 2 篇 社会学
1 篇 农学
- 1 篇 作物学

主题

83 篇 computer science
32 篇 formal logic
19 篇 logic
19 篇 computational mo...
19 篇 polynomials
16 篇 registers
16 篇 semantics
15 篇 mathematics
13 篇 probabilistic lo...
13 篇 standards
13 篇 delay
12 篇 computer archite...
12 篇 hardware
11 篇 concurrent compu...
11 篇 first-order logi...
11 篇 contracts
11 篇 complexity theor...
10 篇 automata
9 篇 linear logic
9 篇 application soft...

机构

8 篇 univ oxford oxfo...
8 篇 cnrs
6 篇 rhein westfal th...
5 篇 univ warsaw wars...
5 篇 department of co...
4 篇 univ bologna bol...
4 篇 tech univ dresde...
3 篇 inria le chesnay
3 篇 department of co...
3 篇 department of ap...
3 篇 univ tokyo
3 篇 carnegie mellon ...
3 篇 mit laboratory f...
2 篇 department of co...
2 篇 vienna tech univ...
2 篇 international co...
2 篇 univ warsaw inst...
2 篇 shanghai jiao to...
2 篇 univ pisa pisa
2 篇 nyu ny 10003 usa

作者

4 篇 b. awerbuch
4 篇 dal lago ugo
3 篇 vardi moshe y.
3 篇 d.m. tullsen
3 篇 d. peleg
3 篇 bojanczyk mikola...
3 篇 gastin paul
3 篇 kiefer sandra
3 篇 worrell james
3 篇 schweitzer pasca...
2 篇 s. dwarkadas
2 篇 adsul bharat
2 篇 kanovich max i.
2 篇 t. leighton
2 篇 kolaitis phokion...
2 篇 avanzini martin
2 篇 krishna shankara...
2 篇 d.h. albonesi
2 篇 tsukada takeshi
2 篇 skrzypczak micha...

语言

358 篇 英文
2 篇 其他

检索条件"任意字段=Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science"

共 360 条记录，以下是251-260 订阅

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

详细简洁

排序：

Finitely monotone properties

Finitely monotone properties

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Stolboushkin, Alexei P. Univ of California Los Angeles Los Angeles United States

A characterization of definability by positive first order formulas in terms of Fraisse-Ehrenfeucht-like games is developed. Using this characterization, an elementary, purely combinatorial, proof of the failure of Lyndon's Lemma (that every monotone first order property is expressible positively) for finite models is given. the proof implies that first order logic is a bad candidate to the role of uniform version of positive Boolean circuits of constant depth and polynomial size. Although Lyndon's Lemma fails for finite models, some similar characterization may be established for finitely monotone properties, and we formulate a particular open problem in this direction.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

Infinitary logic of sparse random graphs

Infinitary logic of sparse random graphs

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Lynch, James F. Tyszkiewicz, Jerzy Clarkson Univ Potsdam United States

Let L$-∞ω/$+ω/ be the infinitary language obtained from the first-order language of graphs by closure under conjunctions and disjunctions of arbitrary sets of formulas, provided only finitely many distinct variables occur among the formulas. Let p(n) be the edge probability of the random graph on n vertices. Previous articles have shown that when p(n) is constant or p(n) = n-α and α > 1, then every sentence in L$-∞ω/omega has probability that converges as n gets large;however, when p(n) = n-α and α -α. It is shown that if α is irrational, then every sentence in L$-∞ω/$+ω/ has probability that converges to 0 to 1. It is also shown that if α = 1, then there are sentences in the deterministic transitive closure logic (and therefore in L$-∞ω/$+ω/), whose probability does not converge.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

Uniform proofs and disjunctive logic programming

Uniform proofs and disjunctive logic programming

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Nadathur, Gopalan Loveland, Donald W. Univ of Chicago Chicago United States

One formulation of the concept of logic programming is the notion of Abstract logic Programming Language, introduced in [8]. Central to that definition is uniform proof, which enforces the requirements of inference direction, including goal-directedness, and the duality of readings, declarative and procedural. We use this technology to investigate Disjunctive logic Programming (DLP), an extension of traditional logic programming that permits disjunctive program clauses. this extension has been considered by some to be inappropriately identified with logic programming because the indefinite reasoning introduced by disjunction violates the goal-oriented search directionality central to logic programming. We overcome this criticism by showing that the requirement of uniform provability can be realized in a logic more general than that of DLP under a modest, sound, modification of programs. We use this observation to derive inference rules that capture the essential proof structure of InH-Prolog, a known proof procedure for DLP.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Semantic challenge of Verilog HDL

Semantic challenge of Verilog HDL

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Gordon, Mike Univ of Cambridge Cambridge United Kingdom

the Verilog hardware description language (HDL) is widely used to model the structure and behaviour of digital systems ranging from simple hardware building blocks to complete systems. Its semantics is based on the scheduling of events and the propagation of changes. Different Verilog models of the same device are used during the design process and it is important that these be 'equivalent';formal methods for ensuring this could be commercially significant. Unfortunately, there is very little theory available to help. this self-contained tutorial paper explains the semantics of Verilog informally and poses a number of logical and semantic problems that are intended to provoke further research. Any theory developed to support Verilog is likely to be useful for the analysis of the similar (but more complex) language VHDL.

关键词： computer hardware description languages

来源：评论

学校读者我要写书评

暂无评论

Partial model checking

Partial model checking

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Andersen, Henrik Reif Technical Univ of Denmark Lyngby Denmark

A major obstacle in applying finite-state model checking to the verification of large systems is the combinatorial explosion of the state space arising when many loosely coupled parallel processes are considered. the problem also known as the state-explosion problem has been attacked from various sides. this paper presents a new approach based on partial model checking: Parts of the concurrent system are gradually removed while transforming the specification accordingly. When the intermediate specifications constructed in this manner can be kept small, the state-explosion problem is avoided. Experimental results with a prototype implemented in Standard ML, shows that for Milner's Scheduler - an often used benchmark - this approach improves on the published results on Binary Decision Diagrams and is comparable to results obtained using generalized Decision Diagrams. Specifications are expressed in a variant of the modal μ-calculus.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

On the complexity of modular model checking

On the complexity of modular model checking

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Vardi, Moshe Y. Rice Univ Houston United States

In modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. the other part describes the assumed behavior of the environment with which the module is interacting. this is called the assume-guarantee paradigm. Even when one specifies the guaranteed behavior of the module in a branching temporal logic, the assumption in the assume-guarantee pair concerns the interaction of the environment with the module along each computation, and is therefore often naturally expressed in linear temporal logic. In this paper we consider assume-guarantee specifications in which the assumption is given by an LTL formula and the guarantee is given by a CTL formula. Verifying modules with respect to such specifications is called the linear-branching model-checking problem. We apply automata-theoretic techniques to obtain a model-checking algorithm whose running time is linear in the size of the module and the size of the CTL guarantee, but doubly exponential in the size of the LTL assumption. We also show that the high complexity in the size of the LTL specification is inherent by proving that the problem is EXPSPACE-complete. the lower bound applies even if the branching temporal guarantee is restricted to be specified in CTL, the universal fragment of CTL.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

First-order queries on finite structures over the reals

First-order queries on finite structures over the reals

引用

proceedings of the 10th annual ieee symposium on logic in computer science

作者： Paredaens, Jan Van den Bussche, Jan Van Gucht, Dirk Antwerp Belgium

We investigate properties of finite relational structures over the reals expressed by first-order sentences whose predicates are the relations of the structure plus arbitrary polynomial inequalities, and whose quantifiers can range over the whole set of reals. In constraint programming terminology, this corresponds to Boolean real polynomial constraint queries on finite structures. the fact that quantifiers range over all reals seems crucial;however, we observe that each sentence in the first-order theory of the reals can be evaluated by letting each quantifier range over only a finite set of real numbers without changing its truth value. Inspired by this observation, we then show that when all polynomials used are linear, each query can be expressed uniformly on all finite structures by a sentence of which the quantifiers range only over the finite domain of the structure. In other words, linear constraint programming on finite structures can be reduced to ordinary query evaluation as usual in finite model theory and databases. Moreover, if only 'generic' queries are taken into consideration, we show that this can be reduced even further by proving that such queries can be expressed by sentences using as polynomial inequalities only those of the simple form x < y.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

A modified approach to data cache management

A modified approach to data cache management

引用

ieee/acm International symposium on Microarchitecture (MICRO)

作者： G. Tyson M. Farrens J. Matthews A.R. Pleszkun Department of Computer Science University of California Riverside CA USA Computer Science Department University of California Davis CA USA Department of Electrical and Electronic Engineering University of Colorado Boulder Boulder CO USA

As processor performance continues to improve, more emphasis must be placed on the performance of the memory system. In this paper, a detailed characterization of data cache behavior for individual load instructions is given. We show that by selectively applying cache line allocation according the characteristics of individual load instructions, overall performance can be improved for both the data cache and the memory system. this approach can improve some aspects of memory performance by as much as 60 percent on existing executables.

关键词： Clocks computer science Time measurement Bandwidth Pins Velocity measurement Sun logic Delay Prefetching

来源：评论

学校读者我要写书评

暂无评论

Improving CISC instruction decoding performance using a fill unit

Improving CISC instruction decoding performance using a fill...

引用

ieee/acm International symposium on Microarchitecture (MICRO)

作者： M. Smotherman M. Franklin Department of Computer Science Clemson University Clemson SC USA Department of Elect. and Computer Engineering Clemson University Clemson SC USA

Current superscalar processors, both RISC and CISC, require substantial instruction fetch and decode bandwidth to keep multiple functional units utilized. While CISC instructions can sometimes provide reduced fetch bandwidth requirements, they are correspondingly more difficult to decode. A hardware assist, called a fill unit, can dynamically collect decoded microoperations into a decoded instruction cache. Future code fetches to those locations can be satisfied out of this cache and thus bypass the decoding logic. this approach is investigated using the Intel x86 architecture, and a speedup of approximately a factor of two over a P6-like decoding structure is seen for the three SPEC benchmarks investigated. this design is accompanied by a microengine-register allocation and renaming scheme that prevents the increased supply of microoperations from placing excessive demands on the normal register renaming hardware.

关键词： Decoding Hardware Reduced instruction set computing Bandwidth Dynamic scheduling Instruction sets computer science logic Registers Processor scheduling

来源：评论

学校读者我要写书评

暂无评论

Partial resolution in branch target buffers

Partial resolution in branch target buffers

引用

ieee/acm International symposium on Microarchitecture (MICRO)

作者： B. Fagin K. Russell Dept of Computer Science US Air Force Academy Lockheed Sanders Corporation

Branch target buffers, or BTBs, are small caches for recently accessed program branching information. Like data caches, the set of intercepted addresses is divided into equivalence classes based on the low order bits of an address. Unlike data caches, however, complete resolution of a single address from within an equivalence class is not required for correct program execution. Substantial savings are therefore possible by employing partial resolution, using fewer tag bits than necessary to uniquely identify an address. We present our analysis of the relationship between the number of tag bits in a branch target buffer and prediction accuracy, based on dynamic simulations of the SPECINT92 benchmark suite. For a 512 entry BTB, our results indicate that, on average, only 2 tag bits are necessary to obtain 99.9% of the accuracy obtainable with a full tag. this suggests that existing microprocessors can achieve substantial area savings in BTB tag storage by employing partial resolution.

关键词： Analytical models Hardware computer science Predictive models Microprocessors Buffer storage Frequency logic Cost benefit analysis Reproducibility of results

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共36页 << < 22 23 24 25 26 27 28 29 30 31 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：