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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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 条记录，以下是51-60 订阅

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

详细简洁

排序：

Ramsey Qantifiers over Automatic Structures: Complexity and Applications to Verification 37

Ramsey Qantifiers over Automatic Structures: Complexity and ...

引用

37th annual acm/ieee symposium on logic in computer science, LICS 2022

作者： Bergsträßer, Pascal Ganardi, Moses Lin, Anthony W. Zetzsche, Georg Department of Computer Science Tu Kaiserslautern Kaiserslautern Germany Kaiserslautern Germany Kaiserslautern Germany

ISBN: (纸本)9781450393515

Automatic structures are infnite structures that are fnitely represented by synchronized fnite-state automata. this paper concerns specifcally automatic structures over fnite words and trees (ranked/unranked). We investigate the "directed version"of Ramsey quantifers, which express the existence of an infnite directed clique. this subsumes the standard "undirected version"of Ramsey quantifers. Interesting connections between Ramsey quantifers and two problems in verifcation are frstly observed: (1) reachability with Büchi and generalized Büchi conditions in regular model checking can be seen as Ramsey quantifcation over transitive automatic graphs (i.e., whose edge relations are transitive), (2) checking monadic decomposability (a.k.a. recognizability) of automatic relations can be viewed as Ramsey quantifcation over co-transitive automatic graphs (i.e., the complements of whose edge relations are transitive). We provide a comprehensive complexity landscape of Ramsey quantifers in these three cases (general, transitive, co-transitive), all between NL and EXP. In turn, this yields a wealth of new results with precise complexity, e.g., verifcation of subtree/flat prefx rewriting, as well as monadic decomposability over tree-automatic relations. We also obtain substantially simpler proofs, e.g., for NL complexity for monadic decomposability over word-automatic relations (given by DFAs). © 2022 Copyright held by the owner/author(s). Publication rights licensed to acm.

关键词： Forestry

来源：评论

学校读者我要写书评

暂无评论

Zero-One Laws and Almost Sure Valuations of First-Order logic in Semiring Semantics 22

Zero-One Laws and Almost Sure Valuations of First-Order Logi...

引用

37th annual acm/ieee symposium on logic in computer science, LICS 2022

作者： Grädel, Erich Helal, Hayyan Naaf, Matthias Wilke, Richard Rwth Aachen University Aachen Germany

ISBN: (纸本)9781450393515

Semiring semantics evaluates logical statements by values in some commutative semiring (K, +, •, 0, 1). Random semiring interpretations, induced by a probability distribution on K, generalise random structures, and we investigate here the question of how classical results on frst-order logic on random structures, most importantly the 0-1 laws of Glebskii et al. and Fagin, generalise to semiring semantics. For positive semirings, the classical 0-1 law implies that every frst-order sentence is, asymptotically, either almost surely evaluated to 0 by random semiring interpretations, or almost surely takes only values different from 0. However, by means of a more sophisticated analysis, based on appropriate extension properties and on algebraic representations of frst-order formulae, we can prove much stronger results. For many semirings K the frst-order sentences in FO(t) can be partitioned into classes (Fj)j ?K such that for each j K, every sentence in Fj evaluates almost surely to j under random semiring interpretations. Further, for fnite or infnite lattice semirings, this partition actually collapses to just three classes F0, F1, and Fe, of sentences that, respectively, almost surely evaluate to 0, 1, and to the smallest value e , 0. For all other values j ? K we have that Fj = the problem of computing the almost sure valuation of a frst-order sentence on fnite lattice semirings is Pspace-complete. © 2022 Copyright held by the owner/author(s). Publication rights licensed to acm.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

the amazing mixed polynomial closure and its applications to two-variable first-order logic 22

The amazing mixed polynomial closure and its applications to...

引用

37th annual acm/ieee symposium on logic in computer science, LICS 2022

作者： Place, thomas LaBRI Bordeaux University Talence33400 France

ISBN: (纸本)9781450393515

Polynomial closure is a standard operator which is applied to a class of regular languages. In this paper, we investigate three restrictions called left (LPol), right (RPol) and mixed polynomial closure (MPol). the frst two were known while MPol is new. We look at two decision problems that are defned for every class C . Membership takes a regular language as input and asks if it belongs to C . Separation takes two regular languages as input and asks if there exists a third language in C including the frst one and disjoint from the second. We prove that LPol, RPol and MPol preserve the decidability of membership under mild hypotheses on the input class, and the decidability of separation under much stronger hypotheses. We apply these results to natural hierarchies. First, we look at several language theoretic hierarchies that are built by applying LPol, RPol and MPol recursively to a single input class. We prove that these hierarchies can actually be defned using almost exclusively MPol. We also consider quantifer alternation hierarchies for two-variable frst-order logic (FO2) and prove that one can climb them using MPol. the result is generic in the sense that it holds for most standard choices of signatures. We use it to prove that for most of these choices, membership is decidable for all levels in the hierarchy. Finally, we prove that separation is decidable for the hierarchy of two-variable frst-order logic equipped with only the linear order (FO2( © 2022 Copyright held by the owner/author(s). Publication rights licensed to acm.

关键词： Separation

来源：评论

学校读者我要写书评

暂无评论

Superconducting Computing with Alternating logic Elements 21

Superconducting Computing with Alternating Logic Elements

引用

acm/ieee 48th annual International symposium on computer Architecture (ISCA)

作者： Tzimpragos, Georgios Volk, Jennifer Wynn, Alex Smith, James E. Sherwood, Timothy UC Santa Barbara Santa Barbara CA 93106 USA MIT Lincoln Lab Cambridge MA 02139 USA Univ Wisconsin Madison Madison WI USA

ISBN: (纸本)9781665433334

Although superconducting single flux quantum (SFQ) technologies offer the potential for low-latency operation with energy dissipation of the order of attojoules per gate, their inherently pulse-driven nature and stateful cells have led to designs in which every logic gate is clocked. this means that clocked buffers must be added to equalize logic path lengths, and every gate becomes a pipeline stage. We propose a different approach, where gates are clock-free and synchronous designs have a conventional look-and-feel. Despite being clock-free, however, the gates are state machines by nature. To properly manage these state machines, the logical clock cycle is composed of two synchronous alternating phases: the first of which implements the desired function, and the second of which returns the state machines to the ground state. Moreover, to address the challenges associated with the asynchronous implementation of Boolean NOT operations in pulse-based systems, values are represented as unordered binary codes - in particular, dual-rail codes. With unordered codes, AND and OR operations are functionally complete. We demonstrate that our new approach, xSFQ, with its dual-rail construction and alternating clock phases, along with "double-pumped" logical latches and a timing optimization through latch decomposition, is capable of implementing arbitrary digital designs without gate-level pipelining and the overheads that come with it. We evaluate energy-delay tradeoffs enabled by this approach through a mix of detailed analog circuit modeling, pulse-level discrete-event simulation, and high-level pipeline efficiency analysis. the resulting systems are shown to deliver energy-delay product (EDP) gains over conventional SFQ even with pipeline hazard ratios (HR) below 1%. For hazard ratios equal to 15% and 20% and a design resembling a RISC-V RV32I core (excluding the cost of interlock logic), xSFQ achieves 22x and 31x EDP savings, respectively.

关键词： superconductor electronics alternating logic unordered codes pipelining xSFQ

来源：评论

学校读者我要写书评

暂无评论

Successor-Invariant First-Order logic on Classes of Bounded Degree 20

Successor-Invariant First-Order Logic on Classes of Bounded ...

引用

35th annual acm/ieee symposium on logic in computer science (LICS)

作者： Grange, Julien ENS Paris PSL INRIA CNRS Paris France

ISBN: (纸本)9781450371049

We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of an additional successor relation on the structure is allowed, as long as the validity of formulas is independent on the choice of a particular successor. We show that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.

关键词： finite model theory successor-invariance first-order logic

来源：评论

学校读者我要写书评

暂无评论

First-order tree-to-tree functions 20

First-order tree-to-tree functions

引用

35th annual acm/ieee symposium on logic in computer science (LICS)

作者： Bojanczyk, Mikolaj Doumane, Amina Univ Warsaw Warsaw Poland ENS Lyon CNRS Lyon France

ISBN: (纸本)9781450371049

We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.

关键词： First-order logic monadic second-order logic tree transducer automata

来源：评论

学校读者我要写书评

暂无评论

Counting Bounded Tree Depth Homomorphisms 20

Counting Bounded Tree Depth Homomorphisms

引用

35th annual acm/ieee symposium on logic in computer science (LICS)

作者： Grohe, Martin Rhein Westfal TH Aachen Aachen Germany

ISBN: (纸本)9781450371049

We prove that graphs G, G' satisfy the same sentences of first-order logic with counting of quantifier rank at most k if and only if they are homomorphism-indistinguishable over the class of all graphs of tree depth at most k. Here G, G' are homomorphism-indistinguishable over a class F of graphs if for each graph F is an element of F, the number of homomorphisms from F to G equals the number of homomorphisms from F to G'.

关键词： tree depth counting homomorphisms first order logic homomorphism indistinguishability

来源：评论

学校读者我要写书评

暂无评论

the logic of action lattices is undecidable 19

The logic of action lattices is undecidable

引用

proceedings of the 34th annual acm/ieee symposium on logic in computer science

作者： Stepan Kuznetsov National Research University Higher School of Economics Moscow Russia

We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Register Automata with Extrema Constraints, and an Application to Two-Variable logic 20

引用

35th annual acm/ieee symposium on logic in computer science (LICS)

作者： Torunczyk, Szymon Zeume, thomas Univ Warsaw Warsaw Poland Ruhr Univ Bochum Bochum Germany

ISBN: (纸本)9781450371049

We introduce a model of register automata over infinite trees with extrema constraints. Such an automaton can store elements of a linearly ordered domain in its registers, and can compare those values to the suprema and infima of register values in subtrees. We show that the emptiness problem for these automata is decidable. As an application, we prove decidability of the countable satisfiability problem for two-variable logic in the presence of a tree order, a linear order, and arbitrary atoms that are MSO definable from the tree order. As a consequence, the satisfiability problem for two-variable logic with arbitrary predicates, two of them interpreted by linear orders, is decidable.

关键词： register automata two-variable logic decidability

来源：评论

学校读者我要写书评

暂无评论

Uniformisations of Regular Relations Over Bi-Infinite Words 20

Uniformisations of Regular Relations Over Bi-Infinite Words

引用

35th annual acm/ieee symposium on logic in computer science (LICS)

作者： Fabianski, Grzegorz Skrzypczak, Michal Torunczyk, Szymon Univ Warsaw Inst Informat Warsaw Poland

ISBN: (纸本)9781450371049

We consider the problem of deciding whether a given MSO-definable relation over bi-infinite words contains an MSO-definable function with the same domain. We prove that this problem is decidable. there are two obstacles to the existence of such uniformisations: the first is related to the existence of non-trivial automorphisms of bi-infinite words, whereas the second, more subtle obstacle, is related to the existence of finite, discrete dynamical systems, where no trajectory can be selected by an MSO formula.

关键词： bi-infinite words monadic second-order logic uniformisation

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共36页 << < 2 3 4 5 6 7 8 9 10 11 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：