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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

136 篇 会议
11 册 图书
1 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

119 篇 工学
- 118 篇 计算机科学与技术...
- 66 篇 软件工程
- 5 篇 电气工程
- 4 篇 信息与通信工程
- 2 篇 控制科学与工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 生物医学工程（可授...
37 篇 理学
- 36 篇 数学
- 1 篇 生物学
4 篇 管理学
- 3 篇 图书情报与档案管...
- 1 篇 管理科学与工程(可...
- 1 篇 工商管理
1 篇 医学
- 1 篇 基础医学(可授医学...
- 1 篇 临床医学
- 1 篇 药学(可授医学、理...

主题

37 篇 logic programmin...
10 篇 program transfor...
8 篇 computer circuit...
8 篇 semantics
8 篇 logics and meani...
7 篇 artificial intel...
6 篇 mathematical log...
5 篇 program analysis
5 篇 programming tech...
4 篇 program synthesi...
4 篇 software enginee...
4 篇 software enginee...
4 篇 constraint handl...
4 篇 programming lang...
3 篇 static analysis
3 篇 source-to-source...
2 篇 program debuggin...
2 篇 floating-point n...
2 篇 concurrent const...
2 篇 types

机构

4 篇 katholieke univ ...
4 篇 univ politecn va...
3 篇 nagoya inst tech...
2 篇 univ politecn ma...
2 篇 univ fed rio gra...
2 篇 univ politecn va...
2 篇 katholieke univ ...
2 篇 univ southern de...
2 篇 rhein westfal th...
2 篇 univ complutense...
2 篇 univ north texas...
2 篇 tech u madrid sc...
2 篇 imdea software i...
2 篇 univ new mexico ...
2 篇 univ new mexico ...
2 篇 ecole polytech l...
2 篇 univ ulm d-89069...
2 篇 ecole polytech i...
2 篇 german univ cair...
2 篇 nagoya institute...

作者

6 篇 vidal german
4 篇 schneider-kamp p...
4 篇 silva josep
4 篇 falaschi moreno
4 篇 seki hirohisa
4 篇 abdennadher slim
4 篇 giesl juergen
3 篇 proietti maurizi...
3 篇 de schreye danny
3 篇 leuschel michael
3 篇 lucas salvador
3 篇 meseguer jose
2 篇 puebla german
2 篇 vanhoof w
2 篇 bruynooghe mauri...
2 篇 senni valerio
2 篇 michael hanus
2 篇 gallagher john p...
2 篇 komendantskaya e...
2 篇 sharaf nada

语言

145 篇 英文
3 篇 中文

检索条件"任意字段=18th International Symposium on Logic-Based Program Synthesis and Transformation"

共 148 条记录，以下是101-110 订阅

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

详细简洁

排序：

Correctness of Context-Moving transformations for Term Rewriting Systems 25th

Correctness of Context-Moving Transformations for Term Rewri...

引用

25th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Sato, Koichi Kikuchi, Kentaro Aoto, Takahito Toyama, Yoshihito Tohoku Univ RIEC Aoba Ku 2-1-1 Katahira Sendai Miyagi 9808577 Japan

ISBN: (纸本)9783319274362;9783319274355

Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. the conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.

关键词： Tail-recursion program transformation Term rewriting system Inductive theorem proving

来源：评论

学校读者我要写书评

暂无评论

Analysis of Air Traffic Track Data with the AutoBayes synthesis System

引用

20th international symposium on logic-based program synthesis and transformation, LOPSTR 2010

作者： Schumann, Johann Cate, Karen Lee, Alan SGT Inc NASA Ames Moffett Field CA 94035 USA NASA Ames Res Ctr Moffett Field CA 94035 USA

ISBN: (纸本)9783642205507

the Next Generation Air Traffic System (NGATS) is aiming to provide substantial computer support for the air traffic controller. Algorithms for the accurate prediction of aircraft movements are of central importance for such software systems but trajectory prediction has to work reliably in the presence of unknown parameters and uncertainties. We are using the AutoBayes program synthesis system to generate customized data analysis algorithms that process large sets of aircraft radar track data in order to estimate parameters and uncertainties. In this paper, we present, how the tasks of finding structure in track data, estimation of important parameters in climb trajectories, and detection of continuous descent approaches (CDA) can be supported by code generated from compact AUTOBAYES specifications. We present an overview of the AutoBayes architecture and describe, how its schema-based approach generates customized analysis algorithms, documented C/C++ code, and detailed mathematical derivations. Results of experiments with actual air traffic control data are discussed.

关键词： Air traffic control

来源：评论

学校读者我要写书评

暂无评论

Annotation algorithms for unrestricted independent and-parallelism in logic programs

引用

17th international symposium on logic-based program synthesis and transformation

作者： Casas, Amadeo Carro, Manuel Hermenegildo, Manuel V. Univ New Mexico Dept Comp Sci & Elect Albuquerque NM 87131 USA Univ Politecn Madrid Sch Comp Sci Madrid Spain

ISBN: (纸本)9783540787686

We present two new algorithms which perform automatic parallelization via source-to-source transformations. the objective is to exploit goal-level, unrestricted independent and-parallelism. the proposed algorithms use as targets new parallel execution primitives which are simpler and more flexible than the well-known &/2 parallel operator. this makes it possible to generate better parallel expressions by exposing more potential parallelism among the literals of a clause than is possible with &/2. the difference between the two algorithms stems from whether the order of the solutions obtained is preserved or not. We also report on a preliminary evaluation of an implementation of our approach. We compare the performance obtained to that of previous annotation algorithms and show that relevant improvements can be obtained.

关键词： logic programming automatic parallelization and-parallelism program transformation

来源：评论

学校读者我要写书评

暂无评论

Intuitionistic logic programming for SQL 26th

Intuitionistic Logic Programming for SQL

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Saenz-Perez, Fernando Univ Complutense Madrid Declarat Programming Grp Dept Ingn Software & Inteligencia Artificial Madrid Spain

ISBN: (纸本)9783319631394;9783319631387

Intuitionistic logic programming provides the notion of embedded implication in rule bodies, which can be used to reason about a current database modified by the antecedent. this can be applied to a system that translates SQL to Datalog to solve SQL WIth queries, for which relations are locally defined and can therefore be understood as locally added to the current database. In addition, assumptions in SQL queries as either adding or removing data can be modelled in this way as well, which is an interesting feature for decision-support scenarios. this work suggests a way to apply intuitionistic logic programming to SQL, and provides a pointer to a working system implementing this idea.

关键词： Intuitionistic logic programming SQL Datalog Extended relational algebra

来源：评论

学校读者我要写书评

暂无评论

Determinacy analysis for logic programs using mode and type information

引用

14th international symposium on logic based program synthesis and transformation

作者： López-García, P Bueno, F Hermenegildo, M Tech Univ Madrid UPM Sch Comp Sci Madrid Spain Univ New Mexico Dept Comp Sci Albuquerque NM 87131 USA Univ New Mexico Dept Elect & Comp Engn Albuquerque NM 87131 USA

ISBN: (纸本)3540266550

We propose an analysis for detecting procedures and goals that are deterministic (i.e. that produce at most one solution), or predicates whose clause tests are mutually exclusive (which implies that at most one of their clauses will succeed) even if they are not deterministic (because they call other predicates that can produce more than one solution). Applications of such determinacy information include detecting programming errors, performing certain high-level program transformations for improving search efficiency, optimizing low level code generation and parallel execution, and estimating tighter upper bounds on the computational costs of goals and data sizes, which can be used for program debugging, resource consumption and granularity control, etc. We have implemented the analysis and integrated it in the CiaoPP system, which also infers automatically the mode and type information that our analysis takes as input. Experiments performed on this implementation show that the analysis is fairly accurate and efficient.

关键词： determinacy inference program analysis modes types

来源：评论

学校读者我要写书评

暂无评论

Proof Checking and logic programming 25th

Proof Checking and Logic Programming

引用

25th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Miller, Dale Ecole Polytech Inria Palaiseau France Ecole Polytech LIX Palaiseau France

ISBN: (纸本)9783319274362;9783319274355

In a world where trusting software systems is increasingly important, formal methods and formal proof can help provide trustable foundations. Proof checking can help to reduce the size of the trusted base since we do not need to trust an entire theorem prover if we can check the proofs they produce by a trusted (and smaller) checker. Many approaches to building proof checkers require embedding within them a full programming language. In most many modern proof checkers and theorem provers, that programming language is a functional programming language, often a variant of ML. In fact, parts of ML (e.g., strong typing, abstract datatypes, and higher-order programming) were designed to make ML into a trustworthy "meta-language" for checking proofs. While there is considerable overlap in the foundations of logic programming and proof checking (both benefit from unification, backtracking search, efficient term structures, etc.), the discipline of logic programming has, in fact, played a minor role in the history of proof checking. I will argue that logic programming can have a major role in the future of this important topic.

关键词： Computer circuits

来源：评论

学校读者我要写书评

暂无评论

Towards description and optimization of abstract machines in an extension of prolog

Towards description and optimization of abstract machines in...

引用

16th international symposium on logic-based program synthesis and transformation

作者： Morales, Jose F. Carro, Manuel Hermenegildo, Manuel Univ Complutense Madrid Madrid Spain

ISBN: (纸本)9783540714095

Competitive abstract machines for Prolog are usually large, intricate, and incorporate sophisticated optimizations. this makes them difficult to code, optimize, and, especially, maintain and extend. this is partly due to the fact that efficiency considerations make it necessary to use low-level languages in their implementation. Writing the abstract machine (and ancillary code) in a higher-level language can help harness this inherent complexity. In this paper we show how the semantics of basic components of an efficient virtual machine for Prolog can be described using (a variant of) Prolog which retains much of its semantics. these descriptions are then compiled to C and assembled to build a complete bytecode emulator. thanks to the high level of the language used and its closeness to Prolog the abstract machine descriptions can be manipulated using standard Prolog compilation and optimization techniques with relative ease. We also show how, by applying program transformations selectively, we obtain abstract machine implementations whose performance can match and even exceed that of highly-tuned, hand-crafted emulators.

关键词： prolog abstract machines compilation optimization program transformation

来源：评论

学校读者我要写书评

暂无评论

Verification of the Schorr-Waite Algorithm - From Trees to Graphs

引用

20th international symposium on logic-based program synthesis and Transformatoin, LOPSTR 2010

作者： Giorgino, Mathieu Strecker, Martin Matthes, Ralph Pantel, Marc Univ Toulouse IRIT Toulouse France

ISBN: (纸本)9783642205507

this article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a (pseudo-)imperative version of the Schorr-Waite algorithm by refinement of a functional one working on trees. It is composed of two orthogonal steps of refinement - functional to imperative and tree to graph - finally merged to obtain the result. Our imperative specifications use monadic constructs and syntax sugar, making them close to common imperative languages. this work has been realized within the Isabelle/HOL proof assistant.

关键词： Verification of imperative programs Pointer algorithms program refinement

来源：评论

学校读者我要写书评

暂无评论

logic-based program synthesis and transformation 1

引用

丛书名： Lecture Notes in Computer Science

1000年

作者： María Alpuente

ISBN: (数字)9783642205514

ISBN: (纸本)9783642205507

this book constitutes the thoroughly refereed post-proceedings of the 20th international symposium on logic-based program synthesis and transformation, LOPSTR 2010, held in Hagenberg, Austria in July 2010. the 13 revised full papers presented together with two invited papers were carefully reviewed and selected from 26 submissions. Among the topics covered are specification, synthesis, verification, analysis, optimization, specialization, security, certification, application and tools, program/model manipulation, and transformation techniques for any programming language paradigm.

关键词： Software Engineering programming Techniques logics and Meanings of programs Artificial Intelligence Algorithms

来源：评论

学校读者我要写书评

暂无评论

Scaling Bounded Model Checking by Transforming programs with Arrays 26th

Scaling Bounded Model Checking by Transforming Programs with...

引用

26th international symposium on logic-based program synthesis and transformation (LOPSTR)

作者： Jana, Anushri Khedker, Uday P. Datar, Advaita Venkatesh, R. Niyas, C. Tata Res Dev & Design Ctr Pune Maharashtra India Indian Inst Technol Bombay Maharashtra India

ISBN: (纸本)9783319631394;9783319631387

Bounded Model Checking is one the most successful techniques for finding bugs in program. However, model checkers are resource hungry and are often unable to verify programs with loops iterating over large arrays. We present a transformation that enables bounded model checkers to verify a certain class of array properties. Our technique transforms an array-manipulating (Ansi-C) program to an array-free and loop-free (Ansi-C) program thereby reducing the resource requirements of a model checker significantly. Model checking of the transformed program using an off-the-shelf bounded model checker simulates the loop iterations efficiently. thus, our transformed program is a sound abstraction of the original program and is also precise in a large number of cases-we formally characterize the class of programs for which it is guaranteed to be precise. We demonstrate the applicability and usefulness of our technique on both industry code as well as academic benchmarks.

关键词： program transformation Bounded model checking Array Verification

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：