Loading...




Bimonthly    Since 1986
ISSN 1000-9000(Print)
/1860-4749(Online)
CN 11-2296/TP
Indexed in:
SCIE, Ei, INSPEC, JST, AJ, MR, CA, DBLP, etc.
Publication Details
Edited by: Editorial Board of Journal Of Computer Science and Technology
P.O. Box 2704, Beijing 100190, P.R. China
Sponsored by: Institute of Computing Technology, CAS & China Computer Federation
Undertaken by: Institute of Computing Technology, CAS
Published by: SCIENCE PRESS, BEIJING, CHINA
Distributed by:
China: All Local Post Offices
Other Countries: Springer
 
ip访问总数:
ip当日访问总数:
当前在线人数:
  • Table of Content
      10 July 1990, Volume 5 Issue 3 Previous Issue    Next Issue
    For Selected: View Abstracts Toggle Thumbnails
    Articles
    A Type-Theoretic Approach to Program Development
    Li Wei;
    Journal of Computer Science and Technology, 1990, 5 (3): 209-224. 
    Abstract   PDF(377KB) ( 1295 )   Chinese Summary
    A paradigm of program development using type theories is given after analyzing some typical exam- ples.In order to carry this approach forward,a language ALT is designed.It is a linguistic description of a generalized higher order typed lambda calculus with Π,∑ types and Π,∑ kinds (supertypes). Four examples are given to show how ALT can be used to implement many concepts of software engi- neering and artificial intelligence.They are intuitionistic logic,Peano arithmetic,approximate reasoning and program tr…
    References | Related Articles | Metrics
    A Deductive Database Approach for Complex Objects
    Chen Qiming;
    Journal of Computer Science and Technology, 1990, 5 (3): 225-235. 
    Abstract   PDF(505KB) ( 1147 )   Chinese Summary
    A deductive database approach for complex objects reasoning is proposed,which is characterized by handling predicates nesting in terms of mapping hierarchically structured rules and facts to a flattened Horn-clause implementation scheme.
    References | Related Articles | Metrics
    An Efficient Algorithm for Processing Multi-Relation Queries in Relational Databases
    Liu Weiyi;
    Journal of Computer Science and Technology, 1990, 5 (3): 236-240. 
    Abstract   PDF(230KB) ( 1107 )   Chinese Summary
    After a relation scheme R is decomposed into the set of schemes ρ={R_1,...,R_n},we may pose queries as if R existed in the database,taking a join of R_i s,when it is necessary to implement the query.Suppose a query involves a set of attributes S(?)R,we want to find the smallest subset of ρ whose union includes S.We prove that the problem is NP-complete and present a polynomial-bounded approximation algorithm.A subset of ρ whose union includes S and has a decomposition into 3NF with a lossless join and prese...
    References | Related Articles | Metrics
    Automatic and Hierarchical Verification for Concurrent Systems
    Zhao Xudong; Feng Yulin;
    Journal of Computer Science and Technology, 1990, 5 (3): 241-249. 
    Abstract   PDF(403KB) ( 989 )   Chinese Summary
    Proving correctness of concurrent systems is quite difficult because of the high level of nondeterminism,especially in large and complex ones.AMC is a model checking system for verifying asynchronous concurrent systems by using branching time temporal logic.This paper introduces the tech- niques of the modelling approach,especially how to construct models for large concurrent systems with the concept of hierarchy,which has been proved to be effective and practical in verifying large systems without a large ...
    References | Related Articles | Metrics
    A Goal-Type Driven Method of Solving Horn Logic with Equality
    Hu Yunfa;
    Journal of Computer Science and Technology, 1990, 5 (3): 250-258. 
    Abstract   PDF(374KB) ( 1031 )   Chinese Summary
    A new method of solving Horn logic with equality,the goal-type driven method,is presented, which considers explicitly the unification operator as a goal and merged it into the resolution process. The method has the following advantages.The resolution and the unification have been integrated in a uniform way.The architectures of the inference engines based on Horn logic with equality are simplified. Any techniques of exploiting AND/ OR parallelism to solve goals can also be applied to unification at the same…
    References | Related Articles | Metrics
    Why SA Can Beat the Exponential Explosion in Heuristic Search
    Zhang Bo; Zhang Ling;
    Journal of Computer Science and Technology, 1990, 5 (3): 259-265. 
    Abstract   PDF(335KB) ( 1095 )   Chinese Summary
    In tree (or graph) search,most algorithms mainly use the local heuristic information of each indi- vidual node.But in the statistical heuristic search algorithms the global information about subtrees is used effectively so that the computational complexity is greatly reduced.In this paper the problem of how the global information can be extracted from the local one is discussed.Some features of SA are also concerned.
    References | Related Articles | Metrics
    A Characterization of Achievable Patterns of the MN-Puzzle Problem
    Yang Hongqing;
    Journal of Computer Science and Technology, 1990, 5 (3): 266-274. 
    Abstract   PDF(388KB) ( 1102 )   Chinese Summary
    One important MN-puzzle problem is to find a sequence of up-down and right-left movements of the empty-cell so that a goal-pattern can be achieved from a given initial-pattern.The second problem is to characterize the totality of the goal-pattern from a given initial-pattern.The third problem is finding the fewest movements to achieve it.In this paper,these problems will be completely solved.
    References | Related Articles | Metrics
    Detecting and Locating Failures in Communication Networks
    Shi Weigeng;
    Journal of Computer Science and Technology, 1990, 5 (3): 275-288. 
    Abstract   PDF(623KB) ( 997 )   Chinese Summary
    The connectivity of a strongly connected network may be destroyed after link damage.Since many net- works are connected by directed links,the reachability may be restored by altering the direction of one or more of the links and thus reconfigoring the network.The location of the failed link must first be determined.In this paper,we examine new methods to determine the location of failed links and nodes in networks.A routing test approach is proposed and the conditions under which communication networks may …
    References | Related Articles | Metrics
    Macro-Dataflow Computational Model and Its Simulation
    Sun Yudong; Xie Zhiliang;
    Journal of Computer Science and Technology, 1990, 5 (3): 289-295. 
    Abstract   PDF(175KB) ( 1252 )   Chinese Summary
    This paper discusses the relationship between parallelism granularity and system overhead of dataflow computer systems,and indicates that a trade-off between them should be determined to obtain optimal efficiency of the overall system.On the basis of this discussion,a macro-dataflow computational model is established to exploit the task-level parallelism.Working as a macro-dataflow computer,an Ex- perimental Distributed Dataflow Simulation System (EDDSS) is developed to examine the effectiveness of the macr…
    References | Related Articles | Metrics
    A Framework for Command Recovery in User Interface
    Wang Haiying;
    Journal of Computer Science and Technology, 1990, 5 (3): 296-301. 
    Abstract   PDF(274KB) ( 1272 )   Chinese Summary
    In this paper,a framework is presented for adding a general command recovery facility to user interface.A simple model of interactive system is discussed and four meta commands,UNDO,RE- DO,SKIPBACK,and SKIPFORWARD,are defined.The double-linked list is used to organize the re- covery information in a natural way for easy implementation.Applications of the framework to various demands of command recoveries show that the use of the framework is very easy and convenient.
    References | Related Articles | Metrics
    Some Hard Examples for the Resolution Method
    Yu Xiangdong;
    Journal of Computer Science and Technology, 1990, 5 (3): 302-304. 
    Abstract   PDF(141KB) ( 1091 )   Chinese Summary
    Given n propositional variables,let K_n(i,j),0≤i≤j≤n,be the set (or disjunction )of all conjunctions of i literals of which exactly j literais are negative.Dunham and Wang conjectured that it may require exponential time to decide that every disjunction K_n (i,j)is not valid by the resolution method.This paper gives a proof of the conjecture and then exhibits a new counterexample to the feasibility of the resolution or con- sensus method.
    References | Related Articles | Metrics
  Journal Online
Just Accepted
Archive
Top Cited Papers
Top 30 Most Read
Paper Lists of Areas
Surveys
Special Issues
  Download
   ScholarOne Manuscripts
   Log In

User ID:

Password:

  Forgot your password?

Enter your e-mail address to receive your account information.

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

Home
Editorial Board
Author Guidelines
Subscription
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved