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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

20 篇 会议
5 册 图书

馆藏范围

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

日期分布

学科分类号

15 篇 工学
- 15 篇 计算机科学与技术...
- 13 篇 软件工程
- 1 篇 农业工程
6 篇 理学
- 5 篇 数学
- 2 篇 系统科学
2 篇 管理学
- 1 篇 管理科学与工程(可...
- 1 篇 工商管理
- 1 篇 图书情报与档案管...
1 篇 农学
- 1 篇 作物学

主题

7 篇 logic programmin...
4 篇 mathematical log...
4 篇 logics and meani...
3 篇 programming tech...
3 篇 artificial intel...
2 篇 computer system ...
1 篇 fuzzy logic
1 篇 order, lattices,...
1 篇 computer circuit...
1 篇 project manageme...
1 篇 international
1 篇 inference engine...
1 篇 software enginee...
1 篇 formal logic
1 篇 prolog (programm...
1 篇 programming
1 篇 symbolic and alg...
1 篇 software enginee...
1 篇 automated
1 篇 neural networks

机构

2 篇 dipartimento di ...
1 篇 computer science...
1 篇 departement comp...
1 篇 the pennsylvania...
1 篇 nicta nsw
1 篇 taras shevchenko...
1 篇 computer science...
1 篇 institut für inf...
1 篇 simon fraser uni...
1 篇 leria université...
1 篇 fg intellektik f...
1 篇 microsoft resear...
1 篇 computing scienc...
1 篇 at&t labs resear...
1 篇 university of ma...
1 篇 manchester metro...
1 篇 institut für inf...
1 篇 departamento de ...
1 篇 the university o...
1 篇 dsic upv camino ...

作者

2 篇 andrei voronkov
1 篇 merz stephan
1 篇 a.r. gray
1 篇 saubion frédéric
1 篇 bruynooghe mauri...
1 篇 luís moniz perei...
1 篇 rudolf berghamme...
1 篇 kung-kiu lau
1 篇 lyaletski alexan...
1 篇 h. ganzinger
1 篇 ali mohamed jaou...
1 篇 veronica dahl
1 篇 mayer marta cial...
1 篇 baumgartner pete...
1 篇 manfred kerber
1 篇 papadimitriou ch...
1 篇 harald ganzinger
1 篇 andreoli jean-ma...
1 篇 john lloyd
1 篇 peter j. stuckey

语言

25 篇 英文

检索条件"任意字段=6th International Conference on Logic for Programming and Automated Reasoning, LPAR 1999"

共 25 条记录，以下是11-20 订阅

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

详细简洁

排序：

Proving failure of queries for definite logic programs using XSB-Prolog

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Pelov, Nikolay Bruynooghe, Maurice Departement Computerwetenschappen Katholieke Universiteit Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium

ISBN: (纸本)3540664920

Proving failure of queries for definite logic progrfims can be done by constructing a finite model of the program in which the query is false. A general purpose model generator for first order logic can be used for this. A recent paper presented at PLILP98 shows how the peculiarities of definite progrcims can be exploited to obtain a better solution. there a procedure is described which combines abduction with tabulation and uses a meta-interpreter for heuristic control of the search. the current paper shows how similcir results Ccin be obtained by direct execution under the standard tabulation of the XSB-Prolog system. the loss of control is compensated for by better intelligent beicktracking cind more accurate failure analysis.

关键词： Computer circuits

来源：评论

学校读者我要写书评

暂无评论

A partial evaluation framework for curry programs

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Albert, Elvira Alpuente, María Hanus, Michael Vidal, Germán DSIC UPV Camino de Vera s/n E-46022 Valencia Spain Informatik II RWTH Aachen D-52056 Germany

ISBN: (纸本)3540664920

In this work, we develop a partial evaluation technique for residuating functional logic programs, which generalize the concurrent computation models for logic programs with delays to functional logic prograjns. We show how to lift the nondeterministic choices from run time to specialization time. We ascertain the conditions under which the original and the trainsformed prograjn have the same answer expressions for the considered class of queries as well as the same floundering behavior. All these results are relevjint for prograim optimization in Curry, a functional logic language which is intended to become a staindard in this area. Preliminary empiriccil evaluation of the specialized Curry programs demonstrates that our technique also works well in practice and leads to substantial performance improvements. To our knowledge, this work is the first attempt to formally define and prove correct a generaJ scheme for the partisd evaluation of functional logic programs with delays.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Focusing and proof-nets in linear and non-commutative logic

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Andreoli, Jean-Marc Maieli, Roberto Xerox Research Centre Europe 38240 Meylan France Logica - Università Roma 3 00154 Roma Italy

ISBN: (纸本)3540664920

Linear logic [4] has radsed a lot of interest in computer research, especially because of its resource sensitive nature. One hne of research studies proof construction procedures and their interpretation as computationil models, in the "logic programming" tradition. An efficient proof search procedure, based on a proof normalization result called "Focusing", has been described in [2]. Pocusing is described in terms of the sequent system of commutative Linear logic, which it refines in two steps. It is shown here that Pocusing Ccin also be interpreted in the proof-net formalism, where it appecirs, at least in the multiplicative fragment, to be a simple refinement of the "Splitting lemma" for proof-nets. this change of perspective allows to generalize the Focusing result to (the multiplicative fragment of) any logic where the "Splitting lemma" holds. this is, in particular, the CEise of the Non-Commutative logic of [1], and all the computational exploitation of Pocusing which has been performed in the commutative case can thus be revised and adapted to the non commutative case.

关键词： Focusing

来源：评论

学校读者我要写书评

暂无评论

Resource management in linear logic proof search revisited

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： López, Pablo Pimentel, Ernesto Departamento de Lenguajes y Ciencias de la Computación Universidad de Málaga Campus de Teatinos 29071 Málaga Spain

ISBN: (纸本)3540664920

Linear logic provides a logical framework to express ftindamentEd computationcil concepts in a declcirative style. As a consequence, it has been used as a sound foundation for the design of expressive progreimming and specification languages. Unfortunately, linearity is as convenient for specifying as difficult to implement. In particular, the successful implementation of linear logic Ismguages Eind provers involving context splitting strongly depends on the efficiency of the method computing a suitable split. A number of solutions have been proposed, referred to as lazy splitting or resource management systems. In this paper, we present a new resource management system for the Lolli linear logic Icinguage. We show that the choice of the structure employed to represent the contexts has a strong influence on the overall performcince of the resource mzinagement system. We also estimate the performsmce of previous proposals, and compare them to our new system.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

On the complexity of single-rule datalog queries

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Gottlob, Georg Papadimitriou, Christos Computer Science Division Dept of Electrical Engineering and Computer Science University of California Berkeley Berkeley CA 94720 United States

ISBN: (纸本)3540664920

Datalog is a well-known database query language based on the logic programming paradigm. A general datalog program consists of a number of rules and facts. Programs containing a unique rule and possibly some facts are called single rule programs (sirups). We study both the combined and the program complexity of sirups, ie., the complexity of evaluating sirups over variable and fixed databases, respectively. Moreover, we study the descriptive complexity of sirups, i.e., their expressive power. In ail cases it turns out that even very restricted classes of sirups have the same complexity and essentially the same expressive power as general datalog programs. We show that the evaluation of single clause programs is EXPTIME complete (combined complexity), and, if restricted to linear recursive rules, PSPACE complete. Moreover, sirups with one recursive rule and one additional fact capture PTIME on ordered structures, if a certain data representation is assumed and certain predefined relations are provided. Our results are obtained by a uniform product construction which maps a datalog program into a single rule by essentially maintaining its semantics. We also prove that the datalog clause implication problem, i.e., deciding whether a datalog clause implies another one, is EXPTIME complete.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

First order linear temporal logic over finite time structures

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Cerrito, Serenella Mayer, Marta Cialdea Praud, Sébastien Université de Paris-Sud L.R.I. France Università di Roma Tre France

ISBN: (纸本)3540664920

In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTLfin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTLfin is not recursively axiomatizable. this negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is defined to be A-valid if it is true in all tempered models whose underlying time frtime is not greater them κ, where κ is any fixed positive integer. In this work a tableau calculus is defined, that is sound and complete with respect to κ-validity, when given as input the initial formula and the bound κ on the size of the temporal models. the main feature of the system, extending the prepositional calculus defined in [7], is that of explicitly denoting time points and having tableau nodes labelled by either expressions intuitively stating that a formula holds in a given temporal interval or "temporal constraints" i.e. linear inequalities on time points. Branch closure is reduced to unsatisfiability over the integers of the set of temporal constraints in the branch.

关键词： Calculations

来源：评论

学校读者我要写书评

暂无评论

CHAT is θ(SLG-WAM)

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Demoen, Bart Sagonas, Konstantinos Department of Computer Science Katholieke Universiteit Leuven Belgium Computing Science Department Uppsala Universitet Sweden

ISBN: (纸本)3540664920

CHAT offers an Eilternative to SLG-WAM for implementing the suspension eind resumption of consumers that tabling needs;unlike SLG-WAM, it does not use freeze registers nor a complicated trail to preserve their execution environments. CHAT Eilso limits the amount of copying of CAT, which was previously put forwMd as another alternative to SLG-WAM. Although experimented results show that in preictice CHAT is competitive with - if not better than - SLG-WAM, there remains the annoying fact that on contrived programs the original CHAT can be made axbitraxily worse than SLG-WAM, i.e. the origincd CHAT has an intrinsically higher complexity. In this paper we show how to overcome this problem, in particular, we deal with the two sources of higher complexity of CHAT: the repeated traversal of the choice point stack, Eind the lack of sufficient sharing of the trail. this is eichieved without fundamentally changing the underlying principle of CHAT by a technique that manipulates a Prolog choice point so that it assumes temporarily a different functionality smd in a way that is treinsparent to the underlying WAM. there is more potential use of this technique besides lowering the worst case complexity of CHAT: it leads to considering scheduling strategies that were not feasible before either in CHAT or in SLG-WAM. We aJso discuss extensively issues related to the implementation of the trail in a tabled logic programming system.

关键词： PROLOG (programming language)

来源：评论

学校读者我要写书评

暂无评论

Evidence algorithm and sequent logical inference search

引用

6th international conference on logic for programming and automated reasoning, lpar 1999

作者： Degtyarev, Anatoli I. Lyaletski, Alexander V. Morokhovets, Marina K. Manchester Metropolitan University Department of Computing and Mathematics Chester Street Manchester M1 5GD United Kingdom Taras Shevchenko Kyiv University Cybernetics Department 6 Glushkov avenue 252127 Kyiv Ukraine Glushkov Institute of Cybernetics Digital Automata Theory Department 40 Glushkov avenue 252187 Kyiv Ukraine Glushkov Institute of Cybernetics Ukraine

ISBN: (纸本)3540664920

In this paper we continue to develop the approach to automated search for theorem proofe started in Kyiv in 1960-1970s. this approatch presupposes the development of deductive techniques used for the processing of mathematical texts, written in a formal first-order language, close to the natural language used in mathematical papers. We construct two logical caJculi, gS tnd mS, satisfying the following requirements: the syntacticetl form of the initial problem should be preserved;the proof search should be goal-oriented;preliminary skolemization is not obligatory;equality handling should be sepeurated from the deduction process. the calculus gS is a machine-oriented sequent-type csilculus with "large-block" inference rules for first-order classical logic. the calculus mS is a further development of the calculus gS, enriched with formal analogs of the natursil proof sesurch techniques such as definition handling and application of auxiliary propositions. the results on soundness and completeness of gS and mS aie given.

关键词： Inference engines

来源：评论

学校读者我要写书评

暂无评论

A simulation-based comparison of empirical modeling techniques for software metric models of development effort

A simulation-based comparison of empirical modeling techniqu...

引用

international conference on Neural Information Processing

作者： A.R. Gray Department of Inforimation Science University of Otago New Zealand

Empirical models for the management of software development projects have until recently been based, with only limited exceptions, on linear least-squares regression. the continued failure of the resulting empirical models to provide adequate assistance to managers has led to the examination (and even some adoption) of more sophisticated modeling techniques. these techniques have included robust statistical procedures, various forms of neural network models, fuzzy logic, case-based reasoning, and regression trees. this paper describes a simulation-based study on the performance of some of these empirical modeling techniques using a size and effort software metric data set. the models are assessed using a variety of "goodness of fit" measures-assessing the predictive performance on hold-out samples across 50 simulations using both sampling with replacement and without replacement. the relative performances of each technique can be used to select that which is "best" given the desired predictive accuracy criterion. Overall the best performing technique appears to be M-estimation. this suggests that robustness to outliers, in this case at least, may be more important than modeling non-linearities or interactions.

关键词： Robustness Predictive models Project management Software development management programming Neural networks Fuzzy logic Regression tree analysis Software metrics Sampling methods

来源：评论

学校读者我要写书评

暂无评论

A general framework for R-unification problems 10th

A general framework for R-unification problems

引用

10th international Symposium on programming Languages, Implementations, logics and Programs, PLILP 1998, Held Jointly with the 6th international conference, ALP 1998

作者： Limet, Sébastien Saubion, Frédéric LIFO Université d’Orléans France LERIA Université d’Angers France

ISBN: (纸本)3540650121

E-unification (i.e. solving equations modulo an equational theory E) is an essential technique in automated reasoning, functional logic programming and symbolic constraint solving but, in general E-unification is undecidable. In this paper, we focus on R-unification (i.e. E-unification where theories E are presented by term rewriting systems R). We propose a general method based on tree tuple languages which allows one to decide if two terms are unifiable modulo a term rewriting system R and to represent the set of solutions. As an application, we prove a new decidability result using primal grammars. © Springer-Verlag Berlin Heidelberg 1998.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共3页 << < 1 2 3 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：