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

2nd International Conference on computer-Aided Verification, CAV 1990

作者： Josephs, Mark B. Udding, Jan Tijmen Programming Research Group Oxford University Computing Laboratory 11 Keble Road OxfordOX1 3QD United Kingdom Department of Computer Science Washington University Campus Box 1045 St. LouisMO63130 United States

ISBN: (纸本)9783540544777

A novel process algebra is presented;algebraic expressions specify delay-insensitive circuits in terms of voltage-level transitions on wires. The approach appears to have several advantages over traditional state-graph and production-rule based methods. The wealth of algebraic laws makes it possible to specify circuits concisely and facilitates the verification of designs. Individual components can be composed into circuits in which signals along internal wires axe hidden from the environment. © Springer-Verlag Berlin Heidelberg 1991.

关键词： Timing circuits

来源：评论

学校读者我要写书评

暂无评论

Formal specification of software systems using Two-Level Grammar 15

Formal specification of software systems using Two-Level Gra...

引用

15th Annual International computer Software and Applications Conference, CMPSAC 1991

作者： Bryant, Barrett R. Pan, Aiqin Computer and Information Sciences Dept. University of Alabama at Birmingham UAB Station Mail Stop 1170 BirminghamAL35294 United States Knowledge Based/Programming Systems IBM Santa Teresa Laboratory Department L78 555 Bailey Avenue San JoseCA95161 United States

ISBN: (纸本)0818621524

Two-Level Grammar (TLG) is proposed for the formal specification and automatic generation of software systems. TLG specifications are unique in that they are a structured form of natural language which is executable. This has the potential for greatly increasing the reliability of the developed software system for the following reasons. Because it is a form of natural language, TLG may be used as an effective communication medium between the system users, designers, and implementors, thereby reducing the likelihood of errors caused by miscommunication. Furthermore, we may automatically generate an efficient software system, expressed in C, from the specification in a provably correct way. Successful applications have included database/knowledge base systems and programming language compilers. © 1991 IEEE.

关键词： Formal specification

来源：评论

学校读者我要写书评

暂无评论

Improving tableau deductions in multiple-valued logics

Improving tableau deductions in multiple-valued logics

引用

International Symposium on Multiple-Valued Logic

作者： N.V. Murray E. Rosenthal Institute for Programming & Logics Department of Computer Science State University of New York Albany Albany NY USA Department of Mathematics University of New Haven West Haven CT USA

Path dissolution is an efficient generalization of the method of analytic tableaux. Both methods feature (in the propositional case) strong completeness, the lack of reliance upon conjunctive normal form (CNF), and the ability to produce a list of essential models (satisfying interpretations) of a formula. Dissolution can speed up every step in a tableau deduction in classical logic. The authors consider means for adapting both techniques to multiple-valued logics, and show that the speed-up theorem applies in this more general setting. These results are pertinent for modeling uncertainty and commonsense reasoning.< >

关键词： Logic programming computer science Uncertainty Mechanical factors Mathematics Inference mechanisms Artificial intelligence Knowledge representation

来源：评论

学校读者我要写书评

暂无评论

ROLE OF SIMULATION IN RAPID PROTOTYPING FOR CONCEPT DEVELOPMENT

引用

NAVAL ENGINEERS JOURNAL 1991年第3期103卷 204-211页

作者： KING, JF BARTON, DE J. Fred King:is the manager of the Advanced Technology Department for Unisys in Reston Virginia. He earned his Ph.D. in mathematics from the University of Houston in 1977. He has been principal investigator of research projects in knowledge engineering pattern recognition and heuristic problem-solving. Efforts include the development of a multi-temporal multispectral classifier for identifying graincrops using LANDSAT satellite imagery data for NASA. Also as a member of the research team for a NCI study with Baylor College of Medicine and NASA he helped develop techniques for detection of carcinoma using multispectral microphotometer scans of lung tissue. He established and became technical director of the AI Laboratory for Ford Aerospace where he developed expert scheduling modeling and knowledge acquisition systems for NASA. Since joining Unisys in 1985 he has led the development of object-oriented programming environments blackboard architectures data fusion techniques using neural networks and intelligent data base systems. Douglas E. Barton:is manager of Logistics Information Systems for Unisys in Reston Virginia. He earned his B.A. degree in computer science from the College of William and Mary in 1978 and did postgraduate work in London as a Drapers Company scholar. Since joining Unisys in 1981 his work has concentrated on program management and software engineering of large scale data base management systems and design and implementation of knowledge-based systems in planning and logistics. As chairman of the Logistics Data Subcommittee of the National Security Industrial Association (NSIA) he led an industry initiative which examined concepts in knowledge-based systems in military logistics. His responsibilities also include evaluation development and tailoring of software engineering standards and procedures for data base and knowledge-based systems. He is currently program manager of the Navigation Information Management System which provides support to the Fleet Ballistic Missile Progr

A valuable technique during concept development is rapid prototyping of software for key design components. This approach is particularly useful when the optimum design approach is not readily apparent or several known alternatives need to be rapidly evaluated. A problem inherent in rapid prototyping is the lack of a "target system" with which to interface. Some alternatives are to develop test driver libraries, integrate the prototype with an existing working simulator, or build one for the specific problem. This paper presents a unique approach to concept development using rapid prototyping for concept development and scenario-based simulation for concept verification. The rapid prototyping environment, derived from artificial intelligence technology, is based on a blackboard architecture. The rapid prototype simulation capability is provided through an object-oriented modeling environment. It is shown how both simulation and blackboard technologies are used collectively to rapidly gain insight into a tenacious problem. A specific example will be discussed where this approach was used to evolve the logic of a mission controller for an autonomous underwater vehicle.

关键词： Military Engineering

来源：评论

学校读者我要写书评

暂无评论

UNNECESSARY INFERENCES IN ASSOCIATIVE-COMMUTATIVE COMPLETION PROCEDURES

引用

MATHEMATICAL SYSTEMS THEORY 1990年第3期23卷 175-206页

作者： ZHANG, HT KAPUR, D 1. Department of Computer Science The University of Iowa 52242 Iowa City IA USA 2. Institute of Programming and Logics Department of Computer Science State University of New York at Albany 12222 Albany NY USA

Theoretical results for identifying unnecessary inferences are discussed in the context of the use of a completion-procedure-based approach toward automated reasoning. The notion of a general superposition is introduced and it is proved that in a completion procedure, once a general superposition is considered, all its instances are unnecessary inferences and, thus, do not have to be considered. It is also shown that this result can be combined with another criterion, called the prime superposition criterion, proposed by Kapur, Musser, and Narendran, thus implying that prime and general superpositions are sufficient. These results should be applicable to other approaches toward automated reasoning, too. These criteria can be effectively implemented, and their implementation has resulted in automatically proving instances of Jacobson's theorem (also known as the ring commutativity problems) usingRRL (Rewrite Rule Laboratory), a theorem prover based on rewriting techniques and completion.

关键词： Prime Automated Reasoning AUTOMATIC Completion kapur Theorem

来源：评论

学校读者我要写书评

暂无评论

Specification & verification of higher order processes 15th

Specification & verification of higher order processes

引用

15th Symposium on Mathematical Foundations of computer Science, MFCS 1990

作者： Hansen, Michael R. Chao-Chen, Zhou Department of Computer Science Technical University of Denmark LyngbyDK-2800 Denmark Programming Research Group Oxford University United Kingdom

ISBN: (纸本)9783540529538

A system is a collection of processes connected by channels over which they communicate. We consider systems where processes can be communicated. We propose an extension to propositional temporal logic as specification language and an extension to CSP as programming notation for such higher order systems, and we give a sound compositional proof system for verifying that a process satisfies a specification. © Springer-Verlag Berlin Heidelberg 1990.

关键词： Specifications

来源：评论

学校读者我要写书评

暂无评论

A proof-theoretic approach to logic programming. I. Clauses as rules

引用

Journal of Logic and Computation 1990年第2期1卷 261-283页

作者： Hallnäs, Lars Schroeder-Heister, Peter Programming Methodology Group Department of Computer Science Chalmers University of Technology Sweden Universität Tubingen 7400 Tubingen FRG Germany University of Göteborg 412 96 Goteborg Sweden

In this paper definite Horn clause programs are investigated within a proof-theoretic framework;program clauses being considered rules of a formal system. Based on this approach, the soundness and completeness of SLD-resolution is established by purely proof-theoretic methods. Extended Horn clauses are defined as rules of higher levels and related to an approach based on implication formulae in the bodies of clauses. In a further extension, which is treated in Part II of this series, program clauses are viewed as clauses in inductive definitions of atoms, justifying an additional inference schema: a reflection principle that roughly corresponds to interpreting the program clauses as introduction rules in the sense of natural deduction. The evaluation procedures for queries with respect to the defined extensions of definite Horn clause programs are shown to be sound and complete. The sequent calculus with the general elimination schema even permits the introduction of a genuine notion of falsity which is not defined via a meta-rule. © 1990 Oxford University Press.

关键词： Inductive definition Logic programming Proof theory Rule

来源：评论

学校读者我要写书评

暂无评论

A complete semantic back chaining proof system 10th

引用

10th International Conference on Automated Deduction, CADE 1990

作者： Nie, Xumin Plaisted, David A. Department of Computer Science University of North Carolina at Chapel Hill Chapel HillNC27599 United States Institute for Programming and Logics Deparment of Computer Science University of Albany State University of New York AlbanyNY12222 United States

ISBN: (纸本)9783540528852

We discuss a sequent style clause-based proof system that supports several important strategies in automatic theorem proving. The system has a goal-subgoal structure and supports back chaining with caching;it permits semantic deletion, sometimes using multiple models;it is also a genuine set of support strategy;and it is complete for first order logic in clause form. © Springer-Verlag Berlin Heidelberg 1990.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

APU: an automatic programmer for UNIX

APU: an automatic programmer for UNIX

引用

International Conference on Tools for Artificial Intelligence (ICTAI)

作者： M.T. Harandi S. Bhansali Knowledge Based Programming Assistant Group Department of Computer Science University of Illinois Urbana-Champaign Urbana IL USA

The authors present a paradigm for automating programming based on how humans program. The paradigm involves top-down decomposition of a given problem into smaller problems using, if possible, programming cliches and analogies from previously solved problems till a primitive level is reached; at the primitive level the problem is solved by making calls to a library of pre-existing sub-routines that encode specific knowledge about the domain. The authors describe APU, which uses the above paradigm to automate UNIX programming, and focus on the knowledge structure and the problem-solving capability without the use of analogy.< >

关键词： programming profession Automatic programming Humans Libraries Sorting Dictionaries computer science Problem-solving Artificial intelligence Writing

来源：评论

学校读者我要写书评

暂无评论

Representation and execution support for reliable robot applications

Representation and execution support for reliable robot appl...

引用

Reliable Distributed Systems

作者： P.S. Gopinath D.M. Lyons S. Mehta Computer Architecture and Programming Systems Department North American Philips Corporation Briarcliff Manor NY USA Autonomous Systems Department Philips Laboratories North American Philips Corporation Briarcliff Manor NY USA

ISBN: (纸本)0818620811

Robot applications, represented as plans, are used to outline a viewpoint that robustness needs to be emphasized in two areas: in the plan representation and in the underlying system software. Robot applications are inherently distributed, since the hardware usually comprises a set of independent actuators and sensors, with the robot programs acting as links between them. A special model of distributed computation, the RS (Robot Schemas) model, has been designed to handle the issues of robot plan representation, and an overview of the model is presented. An initial implementation of the model with minimal execution support demonstrated that the domain-dependent aspect of robustness on its own was not sufficient for robust behavior. Consequently, the OS has been augmented with real-time scheduling, and monitoring facilities.< >

关键词： Robustness Robot sensing systems Robotics and automation Application software Monitoring Timing Real time systems Human robot interaction Robot programming Laboratories

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：