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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

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

详细简洁

排序：

Path Spaces of Higher Inductive Types in Homotopy Type theory 34

Path Spaces of Higher Inductive Types in Homotopy Type Theor...

引用

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

作者： Kraus, Nicolai von Raumer, Jakob Univ Nottingham Nottingham England Eotvos Lorand Univ Budapest Hungary

ISBN: (纸本)9781728136080

the study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. this result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.

关键词： computer languages Mathematics Equalizers Standards categories Terminology Switches

来源：评论

学校读者我要写书评

暂无评论

On the Termination Problem for Probabilistic Higher-Order Recursive Programs 34

On the Termination Problem for Probabilistic Higher-Order Re...

引用

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

作者： Kobayashi, Naoki Dal Lago, Ugo Grellois, Charles Univ Tokyo Tokyo Japan Univ Bologna Bologna Italy Aix Marseille Univ Marseille France

ISBN: (纸本)9781728136080

In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. As a first step towards model checking of probabilistic higher-order programs, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. the model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem - or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (but possibly incomplete) procedure for approximately computing the termination probability.

关键词： Probabilistic logic Model checking Markov processes Computational modeling Mathematical model computer languages Safety

来源：评论

学校读者我要写书评

暂无评论

A Probabilistic and Non-Deterministic Call-by-Push-Value Language 34

A Probabilistic and Non-Deterministic Call-by-Push-Value Lan...

引用

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

作者： Goubault-Larrecq, Jean Univ Paris Saclay CNRS ENS Paris Saclay LSV St Aubin France

ISBN: (纸本)9781728136080

there is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract-and those two primitives are required for that.

关键词： Probabilistic logic Semantics Lattices Topology Cost accounting Coherence Standards

来源：评论

学校读者我要写书评

暂无评论

Probabilistic Relational Reasoning via Metrics 34

Probabilistic Relational Reasoning via Metrics

引用

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

作者： de Amorim, Arthur Azevedo Gaboardi, Marco Hsu, Justin Katsumata, Shin-ya Carnegie Mellon Univ Pittsburgh PA 15213 USA Univ Buffalo Buffalo NY USA Univ Wisconsin Madison WI USA Natl Inst Informat Tokyo Japan

ISBN: (纸本)9781728136080

the Fuzz programming language by Reed and Pierce uses an elegant linear type system combined with a monad -like type to express and reason about probabilistic sensitivity properties, most notably s -differential privacy. We show how to extend Fuzz to capture more general relational properties of probabilistic programs, with approximate, or (s, 5) differential privacy serving as a leading example. Our technical contributions are threefold. First, we introduce the categorical notion of comonadic lifting of a monad to model composition properties of probabilistic divergences. then, we show how to express relational properties in terms of sensitivity properties via an adjunction we call the path construction. Finally, we instantiate our semantics to model the terminating fragment of Fuzz extended with types carrying information about other divergences between distributions.

关键词： Extraterrestrial measurements Sensitivity Differential privacy Probabilistic logic Databases Semantics

来源：评论

学校读者我要写书评

暂无评论

Graph Planning with Expected Finite Horizon 34

Graph Planning with Expected Finite Horizon

引用

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

作者： Chatterjee, Krishnendu Doyen, Laurent IST Austria Klosterneuburg Austria CNRS Paris France ENS Paris Saclay LSV Paris France

ISBN: (纸本)9781728136080

Graph planning gives rise to fundamental algorithmic questions such as shortest path, traveling salesman problem, etc. A classical problem in discrete planning is to consider a weighted graph and construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary, to represent the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stoppingtime distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stopping time also computes an optimal plan among all possible plans.

关键词： Planning Transducers Switches computer science Mathematical model Traveling salesman problems

来源：评论

学校读者我要写书评

暂无评论

Timed Systems through the Lens of logic 34

Timed Systems through the Lens of Logic

引用

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

作者： Akshay, S. Gastin, Paul Juge, Vincent Krishna, Shankara Narayanan Indian Inst Technol Mumbai Maharashtra India ENS Paris Saclay LSV Cachan France Univ Paris Saclay CNRS St Aubin France Univ Paris Est Marne Vallee LIGM CNRS Champs Sur Marne France

ISBN: (纸本)9781728136080

In this paper, we analyze timed systems with data structures. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. the logical definability of several graph properties [20], [10] has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.

关键词： Timed systems propositional dynamic logic logical definability Efficient algorithms graphs

来源：评论

学校读者我要写书评

暂无评论

Model Comparison Games for Horn Description logics 34

Model Comparison Games for Horn Description Logics

引用

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

作者： Jung, Jean Christoph Papacchini, Fabio Wolter, Frank Zakharyaschev, Michael Univ Bremen Bremen Germany Univ Liverpool Dept Comp Sci Liverpool Merseyside England Birkbeck Univ London Dept Comp Sci & Informat Syst London England

ISBN: (纸本)9781728136080

Horn description logics are syntactically defined fragments of standard description logics that fall within the Horn fragment of first-order logic and for which ontology-mediated query answering is in PTIME for data complexity. they were independently introduced in modal logic to capture the intersection of Horn first-order logic with modal logic. In this paper, we introduce model comparison games for the basic Horn description logic horn ALC (corresponding to the basic Horn modal logic) and use them to obtain an Ehrenfeucht-Fraisse type definability result and a van Benthem style expressive completeness result for horn ALC. We also establish a finite model theory version of the latter. the Ehrenfeucht-Fraisse type definability result is used to show that checking hornALC indistinguishability of models is EXPTIME-complete, which is in sharp contrast to ALC indistinguishability (i.e., bisimulation equivalence) checkable in PTIME. In addition, we explore the behavior of Horn fragments of more expressive description and modal logics by defining a Horn guarded fragment of first-order logic and introducing model comparison games for it.

关键词： Games Complexity theory Standards Computational modeling Cognition Description logic Databases

来源：评论

学校读者我要写书评

暂无评论

High-level methods for homotopy construction in associative n-categories 34

High-level methods for homotopy construction in associative ...

引用

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

作者： Reutter, David Vicary, Jamie Univ Oxford Dept Comp Sci Oxford England Univ Birmingham Sch Comp Sci Birmingham W Midlands England

ISBN: (纸本)9781728136080

A combinatorial theory of associative n-categories has recently been proposed, with strictly associative and unital composition in all dimensions, and the weak structure arising as a notion of 'homotopy' with a natural geometrical interpretation. Such a theory has the potential to serve as an attractive foundation for a computer proof assistant for higher category theory, since it allows composites to be uniquely described, and relieves proofs from the bureaucracy of associators, unitors and their coherence. However, this basic theory lacks a high-level way to construct homotopies, which would be intractable to build directly in complex situations;it is not therefore immediately amenable to implementation. We tackle this problem by describing a 'contraction' operation, which algorithmically constructs complex homotopies that reduce the lengths of composite terms. this contraction procedure allows building of nontrivial proofs by repeatedly contracting subterms, and also allows the contraction of those proofs themselves, yielding in some cases single-step witnesses for complex homotopies. We prove correctness of this procedure by showing that it lifts connected colimits from a base category to a category of zigzags, a procedure which is then iterated to yield a contraction mechanism in any dimension. We also present ***, an online proof assistant that implements the theory of associative n-categories, and use it to construct a range of examples that illustrate this new contraction mechanism.

关键词： Wires Tools Calculus Standards Coherence Buildings computer science

来源：评论

学校读者我要写书评

暂无评论

Codensity Games for Bisimilarity 34

Codensity Games for Bisimilarity

引用

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

作者： Komorida, Yuichi Katsumata, Shin-ya Hu, Nick Klin, Bartek Hasuo, Ichiro Natl Inst Informat Tokyo Japan Grad Univ Adv Studies SOKENDAI Hayama Kanagawa Japan Univ Oxford Oxford England Univ Warsaw Warsaw Poland

ISBN: (纸本)9781728136080

Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other;extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including what we call bisimulation topology).

关键词： Games Measurement Probabilistic logic Topology Informatics Markov processes Kernel

来源：评论

学校读者我要写书评

暂无评论

Long-run Satisfaction of Path Properties 34

Long-run Satisfaction of Path Properties

引用

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

作者： Baier, Christel Bertrand, Nathalie Piribauer, Jakob Sankur, Ocan Tech Univ Dresden Dresden Germany Univ Rennes INRIA CNRS IRISA Rennes France

ISBN: (纸本)9781728136080

the paper introduces the concepts of long-run frequency of path properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. We then study the natural optimization problem of computing the optimal values of these measures, when ranging over all paths or all schedulers, and the corresponding decision problem when given a threshold. the main results are as follows. For (repeated) reachability and other simple properties, optimal long-run probabilities and corresponding optimal memoryless schedulers are computable in polynomial time. When it comes to constrained reachability properties, memoryless schedulers are no longer sufficient, even in the non-probabilistic setting. Nevertheless, optimal long-run probabilities for constrained reachability are computable in pseudo-polynomial time in the probabilistic setting and in polynomial time for Kripke structures. Finally for co-safety properties expressed by NFA, we give an exponential-time algorithm to compute the optimal long-run frequency, and prove the PSPACE-completeness of the threshold problem.

关键词： Markov processes Probabilistic logic Frequency measurement Semantics Optimization Standards Labeling

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共36页 << < 7 8 9 10 11 12 13 14 15 16 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：