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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

884 篇 期刊文献
589 篇 会议
104 册 图书
22 篇 学位论文

馆藏范围

1,600 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

1,376 篇 工学
- 1,341 篇 计算机科学与技术...
- 1,202 篇 软件工程
- 28 篇 控制科学与工程
- 20 篇 电气工程
- 17 篇 信息与通信工程
- 15 篇 机械工程
- 7 篇 建筑学
- 5 篇 电子科学与技术（可...
- 4 篇 土木工程
- 4 篇 交通运输工程
- 4 篇 生物医学工程（可授...
- 3 篇 仪器科学与技术
- 3 篇 农业工程
- 3 篇 网络空间安全
929 篇 理学
- 902 篇 数学
- 31 篇 系统科学
- 14 篇 统计学（可授理学、...
- 7 篇 生物学
- 2 篇 物理学
67 篇 管理学
- 41 篇 管理科学与工程(可...
- 26 篇 图书情报与档案管...
- 22 篇 工商管理
16 篇 教育学
- 14 篇 教育学
6 篇 医学
- 5 篇 基础医学(可授医学...
- 5 篇 临床医学
- 4 篇 公共卫生与预防医...
- 3 篇 药学(可授医学、理...
3 篇 哲学
- 2 篇 哲学
3 篇 经济学
- 3 篇 应用经济学
3 篇 农学
- 3 篇 作物学
1 篇 法学
1 篇 文学

主题

274 篇 answer set progr...
251 篇 logic programmin...
71 篇 software enginee...
67 篇 mathematical log...
60 篇 logics and meani...
59 篇 programming lang...
45 篇 semantics
41 篇 knowledge repres...
34 篇 constraint logic...
32 篇 constraint progr...
30 篇 programming tech...
27 篇 constraint theor...
27 篇 prolog
25 篇 answer-set progr...
24 篇 artificial intel...
23 篇 software enginee...
22 篇 inductive logic ...
21 篇 program transfor...
20 篇 theory
20 篇 non-monotonic re...

机构

38 篇 univ potsdam pot...
22 篇 tu wien austria
18 篇 new mexico state...
16 篇 imdea software i...
15 篇 univ genoa dibri...
15 篇 univ kentucky de...
14 篇 univ a coruna la...
14 篇 univ texas austi...
13 篇 univ calabria ar...
12 篇 univ texas dalla...
11 篇 katholieke univ ...
11 篇 katholieke univ ...
11 篇 vienna univ tech...
10 篇 katholieke univ ...
10 篇 imperial coll lo...
10 篇 vienna univ tech...
9 篇 univ politecn ma...
9 篇 univ genoa genoa
9 篇 univ nebraska om...
9 篇 sabanci univ fac...

作者

47 篇 schaub torsten
34 篇 dodaro carmine
30 篇 eiter thomas
30 篇 cabalar pedro
30 篇 ricca francesco
26 篇 lierler yuliya
26 篇 fandinno jorge
26 篇 gupta gopal
23 篇 riguzzi fabrizio
23 篇 maratea marco
22 篇 alviano mario
21 篇 woltran stefan
21 篇 lifschitz vladim...
19 篇 pontelli enrico
18 篇 gebser martin
17 篇 erdem esra
13 篇 leone nicola
13 篇 carro manuel
13 篇 calimeri frances...
13 篇 oetsch johannes

语言

1,558 篇 英文
26 篇 中文
16 篇 其他

检索条件"任意字段=Theory and Practice of Logic Programming"

共 1600 条记录，以下是611-620 订阅

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

详细简洁

排序：

theory Refinement for Program Verification 1

引用

33rd International Conference on logic programming colocated with the 23rd International Conference on Principles and practice of Constraint programming / 20th International Conference on theory and Applications of Satisfiability Testing

作者： Hyvaerinen, Antti E. J. Asadi, Sepideh Even-Mendoza, Karine Fedyukovich, Grigory Chockler, Hana Sharygina, Natasha Univ Svizzera Italiana Lugano Switzerland Kings Coll London London England Univ Washington Seattle WA 98195 USA

ISBN: (数字)9783319662633

ISBN: (纸本)9783319662633;9783319662626

Recent progress in automated formal verification is to a large degree due to the development of constraint languages that are sufficiently light-weight for reasoning but still expressive enough to prove properties of programs. Satisfiability modulo theories (SMT) solvers implement efficient decision procedures, but offer little direct support for adapting the constraint language to the task at hand. theory refinement is a new approach that modularly adjusts the modeling precision based on the properties being verified through the use of combination of theories. We implement the approach using an augmented version of the theory of bit-vectors and uninterpreted functions capable of directly injecting non-clausal refinements to the inherent Boolean structure of SMT. In our comparison to a state-of-the-art model checker, our prototype implementation is in general competitive, being several orders of magnitudes faster on some instances that are challenging for flattening, while computing models that are significantly more succinct.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

The ASP System DLV2 14th

The ASP System DLV2

引用

14th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Alviano, Mario Calimeri, Francesco Dodaro, Carmine Fusca, Davide Leone, Nicola Perri, Simona Ricca, Francesco Veltri, Pierfrancesco Zangari, Jessica Univ Calabria DeMaCS Arcavacata Di Rende Italy Univ Genoa DIBRIS Genoa Italy

ISBN: (纸本)9783319616605;9783319616599

We introduce dlv2, a new Answer Set programming (ASP) system. dlv2 combines I-dlv, a fully-compliant ASP-Core-2 grounder, with the well-assessed solver wasp. Input programs may be enriched by annotations and directives that customize heuristics of the system and extend its solving capabilities. An empirical analysis conducted on benchmarks from past ASP competitions shows that dlv2 outperforms the old dlv system and is close to the state-of-the-art ASP system CLINGO.

关键词： Answer Set programming Systems Grounding Solving

来源：评论

学校读者我要写书评

暂无评论

Constraint programming Applied to the Multi-Skill Project Scheduling Problem 23rd

Constraint Programming Applied to the Multi-Skill Project Sc...

引用

33rd International Conference on logic programming / 23rd International Conference on Principles and practice of Constraint programming (CP) / 20th International Conference on theory and Applications of Satisfiability Testing (SAT)

作者： Young, Kenneth D. Feydy, Thibaut Schutt, Andreas Univ Melbourne Melbourne Vic Australia CSIRO Decis Sci Data61 Melbourne Vic Australia

ISBN: (纸本)9783319661582;9783319661575

The Multi-Skill Project Scheduling Problem is a variant of the well-studied Resource Constrained Project Scheduling Problem, in which the resources are assumed to be multi-skilled. Practical applications of this problem occur when the resources considered are a multi-skilled workforce or multi-purpose machines. This variant introduces a set of assignment decisions between the resources and activities, further to the usual scheduling decisions. This additional layer of complexity results in the problem becoming far more difficult to solve. We investigate different constraint programming models and searches tailored for solvers with nogood learning. These models and searches are then evaluated on instances available from the literature as well as newly generated ones. Using the best performing model and search, we are able to close at least 87 open instances from the literature.

关键词： Constraint programming

来源：评论

学校读者我要写书评

暂无评论

CoverSize: A Global Constraint for Frequency-Based Itemset Mining 23rd

CoverSize: A Global Constraint for Frequency-Based Itemset M...

引用

作者： Schaus, Pierre Aoga, John O. R. Guns, Tias UCLouvain ICTEAM Louvain La Neuve Belgium ED SDI UAC Abomey Calavi Benin VUB Brussels Brussels Belgium Katholieke Univ Leuven Leuven Belgium

ISBN: (纸本)9783319661582;9783319661575

Constraint programming is becoming competitive for solving certain data-mining problems largely due to the development of global constraints. We introduce the CoverSize constraint for itemset mining problems, a global constraint for counting and constraining the number of transactions covered by the itemset decision variables. We show the relation of this constraint to the well-known table constraint, and our filtering algorithm internally uses the reversible sparse bitset data structure recently proposed for filtering table. Furthermore, we expose the size of the cover as a variable, which opens up new modelling perspectives compared to an existing global constraint for (closed) frequent itemset mining. For example, one can constrain minimum frequency or compare the frequency of an itemset in different datasets as is done in discriminative itemset mining. We demonstrate experimentally on the frequent, closed and discriminative itemset mining problems that the CoverSize constraint with reversible sparse bitsets allows to outperform other CP approaches.

关键词： Constraint theory

来源：评论

学校读者我要写书评

暂无评论

Branch-and-Check with Explanations for the Vehicle Routing Problem with Time Windows 23rd

Branch-and-Check with Explanations for the Vehicle Routing P...

引用

作者： Lam, Edward Van Hentenryck, Pascal CSIRO Data61 Eveleigh NSW 2015 Australia Univ Melbourne Parkville Vic 3010 Australia Univ Michigan Ann Arbor MI 48109 USA

ISBN: (纸本)9783319661582;9783319661575

This paper proposes the framework of branch-and-check with explanations (BCE), a branch-and-check method where combinatorial cuts are found by general-purpose conflict analysis, rather than by specialized separation algorithms. Specifically, the method features a master problem that ignores combinatorial constraints, and a feasibility sub-problem that uses propagation to check the feasibility of these constraints and performs conflict analysis to derive nogood cuts. The BCE method also leverages conflict-based branching rules and strengthens cuts in a post-processing step. Experimental results on the Vehicle Routing Problem with Time Windows show that BCE is a potential alternative to branch-and-cut. In particular, BCE dominates branch-and-cut, both in proving optimality and in finding high-quality solutions quickly.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

The Essence of Higher-Order Concurrent Separation logic 26th

The Essence of Higher-Order Concurrent Separation Logic

引用

26th European Symposium on programming (ESOP) Held as Part of the European Joint Conferences on theory and practice of Software (ETAPS)

作者： Krebbers, Robbert Jung, Ralf Bizjak, Ales Jourdan, Jacques-Henri Dreyer, Derek Birkedal, Lars Delft Univ Technol Delft Netherlands MPI SWS Saarland Informat Campus Saarbrucken Germany Aarhus Univ Aarhus Denmark

ISBN: (纸本)9783662544341;9783662544334

Concurrent separation logics (CSLs) have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids (PCMs) and invariants. However, the realization of these concepts in Iris still bakes in several complex mechanisms-such as weakest preconditions and mask-changing view shifts-as primitive notions. In this paper, we take the Iris story to its (so to speak) logical conclusion, applying the reductionist methodology of Iris to Iris itself. Specifically, we define a small, resourceful base logic, which distills the essence of Iris: it comprises only the assertion layer of vanilla separation logic, plus a handful of simple modalities. We then show how the much fancier logical mechanisms of Iris-in particular, its entire program specification layer-can be understood as merely derived forms in our base logic. This approach helps to explain the meaning of Iris's program specifications at a much higher level of abstraction than was previously possible. We also show that the step-indexed "later" modality of Iris is an essential source of complexity, in that removing it leads to a logical inconsistency. All our results are fully formalized in the Coq proof assistant.

关键词： Computer circuits

来源：评论

学校读者我要写书评

暂无评论

Arc Consistency via Linear programming 23rd

Arc Consistency via Linear Programming

引用

作者： German, Grigori Briant, Olivier Cambazard, Hadrien Jost, Vincent Univ Grenoble Alpes CNRS Grenoble INP G SCOP F-38000 Grenoble France

ISBN: (纸本)9783319661582;9783319661575

A typical technique in integer programming for filtering variables is known as variable fixing. The optimal dual solution of the linear relaxation can be used to detect some of the 0/1 variables that must be fixed to either 0 or 1 in any solution improving the best known, but this filtering is incomplete. A complete technique is proposed in this paper for satisfaction problems with an ideal integer programming formulation. We show, in this case, that the 0/1 variables taking the same value in all solutions can be identified by solving a single linear program with twice the number of the original variables. In other words, a complete variable fixing of the 0/1 variables can be performed for a small overhead. As a result, this technique can be used to design generic arc consistency algorithms. We believe it is particularly useful to quickly prototype arc consistency algorithms for numerous polynomial constraints and demonstrate it for the family of Sequence global constraints.

关键词： Constraint programming Linear programming filtering Arc consistency Reduced-cost fixing

来源：评论

学校读者我要写书评

暂无评论

A Column-Generation Algorithm for Evacuation Planning with Elementary Paths 23rd

A Column-Generation Algorithm for Evacuation Planning with E...

引用

作者： Hasan, Mohd. Hafiz Van Hentenryck, Pascal Univ Michigan Ann Arbor MI 48109 USA

ISBN: (纸本)9783319661582;9783319661575

Evacuation planning algorithms are critical tools for assisting authorities in orchestrating large-scale evacuations while ensuring optimal utilization of resources. To be deployed in practice, these algorithms must include a number of constraints that dramatically increase their complexity. This paper considers the zone-based non-preemptive evacuation planning problem in which each evacuation zone is assigned a unique evacuation path to safety and the flow of evacuees over time for a given zone follows one of a set of specified response curves. The starting point of the paper is the recognition that the first and only optimization algorithm previously proposed for zone-based non-preemptive evacuation planning may produce non-elementary paths, i.e., paths that visit the same node multiple times over the course of the evacuation. Since non-elementary paths are undesirable in practice, this paper proposes a column-generation algorithm where the pricing subproblem is a least-cost path under constraints. The paper investigates a variety of algorithms for solving the subproblem as well as their hybridization. Experimental results on a real-life case study show that the new algorithm produces evacuation plans with elementary paths of the same quality as the earlier algorithm in terms of the number of evacuees reaching safety and the completion time of the evacuation, at the expense of a modest increase in CPU time.

关键词： Column generation Evacuation planning k-shortest paths Mixed-integer programming Constraint programming

来源：评论

学校读者我要写书评

暂无评论

A Tolerant Algebraic Side-Channel Attack on AES Using CP 23rd

A Tolerant Algebraic Side-Channel Attack on AES Using CP

引用

作者： Liu, Fanghui Cruz, Waldemar Ma, Chujiao Johnson, Greg Michel, Laurent Univ Connecticut Dept Comp Sci & Engn Sch Engn Storrs CT 06269 USA

ISBN: (纸本)9783319661582;9783319661575

AES is a mainstream block cipher used in many protocols and whose resilience against attack is essential for cybersecurity. In [14], Oren and Wool discuss a Tolerant Algebraic Side-Channel Analysis (TASCA) and show how to use optimization technology to exploit side-channel information and mount a computational attack against AES. This paper revisits the results and posits that Constraint programming is a strong contender and a potent optimization solution. It extends bit-vector solving as introduced in [8], develops a CP and an IP model and compares them with the original Pseudo-Boolean formulation. The empirical results establish that CP can deliver solutions with orders of magnitude improvement in both run time and memory usage, traits that are essential to potential adoption by cryptographers.

关键词： Algebraic Side-Channel Attack AES Cryptography Block cipher Constraint programming Optimization

来源：评论

学校读者我要写书评

暂无评论

Answer Set Programs with Queries over Subprograms 14th

Answer Set Programs with Queries over Subprograms

引用

14th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Redl, Christoph Tech Univ Wien Inst Informat Syst Favoritenstr 9-11 A-1040 Vienna Austria

ISBN: (纸本)9783319616605;9783319616599

Answer-Set programming (ASP) is a declarative programming paradigm. In this paper we discuss two related restrictions and present a novel modeling technique to overcome them: (1) Meta-reasoning about the collection of answer sets of a program is in general only possible by external postprocessing, but not within the program. This prohibits the direct continuation of reasoning based on the answer to the query over a (sub) program's answer sets. (2) The saturation programming technique exploits the minimality criterion for answer sets of a disjunctive ASP program to solve co-NP-hard problems, which typically involve checking if a property holds for all objects in a certain domain. However, the technique is advanced and not easily applicable by average ASP users;moreover, the use of default-negation within saturation encodings is limited. In this paper, we present an approach which allows for brave and cautious query answering over normal subprograms within a disjunctive program in order to address restriction (1). The query answer is represented by a dedicated atom within each answer set of the overall program, which paves the way also for a more intuitive alternative to saturation encodings and allows also using default-negation within such encodings, which addresses restriction (2).

关键词： Answer Set programming Nonmonotonic reasoning FLP semantics Meta programming Saturation

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共160页 << < 58 59 60 61 62 63 64 65 66 67 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：