摘要:

AbstractIn the resolution‐based theorem proving, logical formulas to be proved are expressed in the form of a closure set (a set of clauses). For proof efficiency, it is desirable that a clause set be reduced to a Horn set by renaming if possible. Several reducing methods have been proposed for this transformation.This paper defines a new reducing method which uses prepositional formulas and is related to a method using 0 – 1 programming. The new method generates a pro‐positional clause set for renaming from the original predicate clause set.A set of logical formulas generated in the method is called a “structural clause set,” because each element in this set indicates the distribution of positive/negative literals in the original predicate clause.An interpretation which satisfies a structural clause set corresponds to a renaming which transforms the original predicate clause set into Horn set.Furthermore, a procedure is presented which determines satisfiability of a structural clause set, and then its time complexity is

ISSN:0882-1666    

DOI:10.1002/scj.4690180301

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractThe self‐checking system refers in general to a class of logical systems with an ability to detect a fault during operation. Especially, the self‐checking system with the property that it never produces a code word in a fault, continuing the correct code word output until a noncode word is produced as the output, is called strongly fault‐secure system (SFS). Numerous studies have been made on the SFS systems and the realization of the totally self‐checking (TSC) system, which is a special case of the SFS system. Various kinds of functional circuits (combinational and sequential circuits as subcircuits) and detecting circuits have been discussed. However, there has been little discussion on the condition to be satisfied by the subsystem in order that the system composed of subsystems satisfies the SFS condition. This paper proposes two new concepts concerning the errors produced in the interface between subsystems: the error‐secure and the error‐propagating properties. Using these concepts, the condition to be satisfied by the interface in the SFS system is presented. The proposed concepts are useful in the SFS design of a complex system composed of a large number of subsystems, such as micr

ISSN:0882-1666    

DOI:10.1002/scj.4690180302

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractThis paper discusses a node‐distributed parallel‐processing event‐driven queueing network simulator, called D‐SSQ. It employs the advanced execution control, aiming at the effective utilization of the parallelism inherent in the queueing network. The advanced control works as follows. Each processor first works ignoring the restrictions from other processors. If a contradiction is detected by manifesting the effects of other processors through the interprocessor communication, the contradiction is dissolved by partially cancelling the results of the previous processing. The processing performance of D‐SSQ was examined by an experimental system and by the simulation using a large‐scale computer. It is observed that the processing capability increases linearly with the number of processors, but does not increase as rapidly as was expected because of the large overhead in the distribution and the ineffective processing by the excessive advance control. Consequently, a restricted advance control has been considered, aiming at the elimination of the excessive advanced operation. It is indicated that the processing performance can be improved and there exists an optimum value for the extent of advance

ISSN:0882-1666    

DOI:10.1002/scj.4690180303

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractWhen a new communication protocol is formulated, some method for protocol description and verification must be employed to describe and verify that protocol. This paper proposes a protocol description method based on McDermott's temporal logic. The features/characteristics of this method include: (1) The ability to describe “event” and “changes of fact” as they occur; (2) Its temporal logic is suitable for description of continuous time element as well as timeout; and (3) Its temporal logic is effective in protocol verification. A canonical form for protocol description is introduced that enables the translation of any logical inference expression into the standard form. The effectiveness of the proposed method is demonstrated by performing the description and verification of Stenning's p

ISSN:0882-1666    

DOI:10.1002/scj.4690180304

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractThis paper describes the algorithm which directly processes the gray‐level image to determine the rotational angle. A complex computation is required to transform the orthogonal coordinates into the polar coordinates. In this paper, a transformation algorithm is proposed using DDA, which is a high‐speed algorithm to generate the digital segment. To evaluate the usefulness of the proposed algorithm, a computer experiment was performed using several input images from a TV camera. The mean error of the rotational angle was ±0.8 deg, and the maximum error was ±3.9 deg, which is quite satisfa

ISSN:0882-1666    

DOI:10.1002/scj.4690180305

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractThe trial‐and‐error efforts by experts have been considered as indispensable in compiling railroad timetables. There is a strong requirement to computerize the procedure, but it has been considered difficult. It is proposed to merge the following two concepts as a means to obtain an efficient trial‐and‐error procedure, which is the basis of the compilation of railroad timetables: (1) the concept of (time) belt, where a number of alternatives for arrival and departure is handled as one alternative, considering only the order of arrivals and departures; (2) the concept of the propagation of constraints, which is well known in the artificial intelligence where alternatives in conflict to the order of arrivals and departures are eliminated. This paper discusses the scheduling problem for the partially ordered set of events. The requirement for the time difference between events is considered as a constraint. An algorithm is proposed which calculates the permissible range of time for the event generation, as a closed interval on the time axis. It is shown that the constructed algorithm can be applied as the basic algorithm for the railroad timetable compilation system, where the timetable is considered as a specification for the order of arrivals and departures of the trains, and the arrival‐departure time is considered as a belt. An efficient method of compilating the timetable by the proposed algorithm is presented, based on the search for the possible orders of the trains, together with the construction example of the timetable for the actua

ISSN:0882-1666    

DOI:10.1002/scj.4690180306

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractThe computer network and multiprocessor system have been developed and studied. They are based on a network composed of nodes containing processors, aiming at the improvement of performance by distributed processing as well as the improvement of reliability by resource distribution. To realize high system performance, adequate routing and flow controls are required in the communication of information among nodes. This paper proposes a new routing control scheme to be used in the packet communication in the computer network or multiprocessor system. The scheme is called potential routing, which models the computer network by an electric circuit, and the packet routing from the source node to the destination node is performed to the potential difference between the adjacent nodes. The node potential is determined first by Kirchhoff's law and is modified dynamically according to the traffic situation during the routing procedure, providing an adequate criterion for the routing. The proposed scheme has a feature in that ping‐pong and loop phenomena, which cause traffic congestion, are not produced in principle. It was verified by simulation that the transmission delay is reduced when the traffic is high or unbalance

ISSN:0882-1666    

DOI:10.1002/scj.4690180307

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractNumerous multiple access protocols have been proposed aiming at an efficient utilization of transmission channels. Among those, the tree‐type protocol is one of the multiple access protocols which provide a stable throughput. Various studies have been made on the tree‐type communication protocols. This paper is concerned especially with the analysis of the throughput of the reservation protocols with tree‐type reservation channel. In the proposed system, the tree‐type protocol is employed to reserve the data slot, providing stable and high throughput. There are two types of tree‐type protocols: the blocked‐access tree protocol which inhibits the transmission of a new packet in the collision resolution interval; and the free‐access tree protocol which does not inhibit the transmission. The reservation protocols employing these two protocols are discussed. Through the analysis, the optimum frame structure for each type is obtained. The maximum throughput of CCA proposed by Lee and Mark, as well as the optimum number of the small reservation slots, are obtained

ISSN:0882-1666    

DOI:10.1002/scj.4690180308

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY

摘要:

AbstractIn 4‐valued image processing, cellular logic operations can be performed by template or pattern matching. The simplification of the image processing algorithm is discussed using a minimization technique of multiple‐valued logic functions. Furthermore, from the viewpoint of hardware implementation, a new pattern matching scheme is proposed so that two different templates can be processed simultaneously in a pipelining manner. Based on these double pattern matching cells, a compact NMOS image processing chip has been implemented. It is demonstrated that the compactness derives from deduced interconnections in the double pattern matching cells using a quaternaryT‐gate realized with pass transi

ISSN:0882-1666    

DOI:10.1002/scj.4690180309

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1987

数据来源: WILEY