Data processing: artificial intelligence – Adaptive system
Reexamination Certificate
1993-05-03
2004-01-13
Follansbee, John A. (Department: 2121)
Data processing: artificial intelligence
Adaptive system
Reexamination Certificate
active
06678667
ABSTRACT:
FIELD OF INVENTION
The invention belongs to artificial intelligence which is a subfield of computer science. It relates to a computer system which has a memory for storing programs including knowledge. By means of controlling adjustments it adapts its programs to input signals and generates output signals on the basis of the adapted programs. The input signals can be generated by keyboards or sensors and the output signals can control printers, displays, or the movements of robots.
DESCRIPTION OF PRIOR ART
The efficiency of systems of “artificial intelligence” is still very small compared to the capabilities of “human intelligence”. This shall be illustrated in the field of automated theorem proving.
The objective of the field of automated theorem proving is to develop computer systems, so-called theorem provers, which automatically generate proofs of mathematical theorems. After more than thirty years of research and development the efficiency of theorem provers is still trivial compared to the capabilities of mathematicians (see Bundy, A.,
The Computer Modelling of Mathematical Reasoning
, San Diego, Calif.: Academic Press, 1983, p. 10). A well-known problem in automated theorem proving is SAM's Lemma. The Markgraf Karl Refutation Procedure is one of the greatest projects in the history of automated theorem proving (see Bläsius, K., Eisinger, N., Siekmann, J., Smolka, G., Herold, A., and Walther, C., The Markgraf Karl Refutation Procedure,
Proceedings of the Seventh International Joint Conference on Artificial Intelligence
, August 1981, Vancouver, Canada). After some fifteen years of development Ohlbach and Siekmann give SAM's Lemma as the only more difficult theorem the Markgraf Karl Refutation Procedure has proved. But a proof of SAM's Lemma is rather trivial from a mathematician's point of view because the proof consists of eight equations seven of which simplify the right side of the first equation (see Ammon, K.,
Proceedings of the Seventh National Conference on Artificial Intelligence
, Aug. 21-26, 1988, St. Paul, USA).
The most known procedure in the field of automated theorem proving is the resolution procedure. The theorem prover OTTER 2.2, which is often regarded as the most powerful resolution prover, is also capable of proving SAM's Lemma (McCune, W. W., OTTER 2.0 Users Guide, Report ANL-90/9, Argonne National Laboratory, Argonne, Ill., 1990, and McCune, W. W., What's new in OTTER 2.2. Report ANL/MCS-TM-153, Argonne National Laboratory, Argonne, Ill., 1991). But in the proof of SAM's Lemma the Markgraf Karl Refutation Procedure and OTTER 2.2 do not satisfy the important minimal requirement that a theorem prover should be capable of processing all axioms. For example, the set of axioms in McCharen, J. D., Overbeek, R. A., and Wos, L. A., Problems and experiments for and with automated theorem-proving programs,
IEEE Transactions on Computers
, Vol. C-25, No. 8, pp. 773-782, is not complete because it does not contain the ordinary lattice operations “join” and “meet”, that is, the existence of a minimum and a maximum in McCharen et al.'s representation. If these most elementary axioms are given to the system, the theorem prover OTTER 2.2 breaks down in a combinatorial explosion. This means that OTTER 2.2 is not capable of proving SAM's Lemma because the proof is largely given to the system by a manual selection of the axioms. For the Markgraf Karl Refutation Procedure a proof of SAM's Lemma is even more difficult than for OTTER 2.2.
Conventional theorem provers such as the Karl Refutation Procedure and OTTER 2.2 have to be controlled manually by so-called options (McCune, W. W., OTTER 2.0 Users Guide, Report ANL-90/9, Argonne National Laboratory, Argonne, Ill., 1990). Because these theorem provers are extensive programs which contain many complex procedures and require powerful computers, a manual control of these options is extremely difficult. This difficulty is even increased by the fact that the procedures in these theorem provers are very different from human reasoning processes, that is, the reasoning processes of the users of these theorem provers. Furthermore, theorem proving problems must be manually translated into a form that can be processed by these theorem provers. For example, the proof of SAM's Lemma requires a translation of the lattice operations into minimum and maximum relations. Such a manual translation of a theorem can be more difficult than a manual proof of the theorem. Furthermore, it is not known in advance into which representation a theorem must be translated so that a theorem prover can find a proof. Furthermore, conventional theorem provers produce unreadable proofs which must be manually retranslated into a readable form.
Conventional theorem provers are not capable of generating the central ideas of significant theorems in higher mathematics, for example a proof of Gödel's Incompleteness Theorem. Even if these ideas are given to a conventional theorem prover, it breaks down after few simple steps in an combinatorial explosion because it cannot process all definitions and lemmas required for proving significant theorems (vgl. Bledsoe, W. W., Non-resolution theorem proving,
Artificial Intelligence
, Vol. 9, 1977, p. 27). Newer approaches to the development of theorem provers, for example the technology of expert systems, have hardly been applied or did not yield better results. Thus, the capabilities of conventional theorem provers are limited to trivial marginal subfields of mathematics.
An essential property of conventional theorem provers is that they contain many complex and extensive procedures which cannot adapt themselves to hardly predictable new problems and situations. Thus, these theorem provers produce many useless steps and finally break down in a combinatorial explosion because they cannot find new ways if a chosen way does not solve a problem.
The problems and limits of the capabilities described above are not restricted to the field of automated theorem proving. Rather, they apply to systems in other fields of artificial intelligence such as image and language processing and robotics.
DISCLOSURE OF INVENTION
The object of the invention is to provide a user-friendly, economical and efficient computer system having a memory for storing knowledge and programs which can also be used in fields that require the solution of new and hardly predictable problems.
According to the invention, this object is achieved by the computer system described subsequently. It processes input signals and finally generates output signals with the aid of the programs and the knowledge in its memory wherein the input and the output signals represent information. It is called adaptive because it is capable of adapting its programs and its knowledge to hardly predictable new problems. An adaptive computer system contains control components and execution components. The control components control the execution components in so-called adjustments. In this process resources are withdrawn from execution components that cannot solve a problem. The withdrawal of resources can be carried out in different ways, for example, completely, partially or temporarily. The withdrawal of resources can also be achieved in that an execution components terminates of itself without result. An important advantage of adaptive computer systems is that they can, by means of adjustments, select execution components that are suitable for solving a problem. Thus, the application of execution components that are not useful for solving a problem is largely avoided. This entails that adaptive computer systems can select and organize a tailored set of efficient execution components which are suitable for solving a problem.
An adaptive computer system is capable of adapting itself to unpredictable new situations, that is, situations that cannot in advance be described completely and in all details. It is capable of generating variations of execution components and then activating these components. It is particularl
Follansbee John A.
Holmes Michael B.
LandOfFree
Adaptive computer system does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Adaptive computer system, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Adaptive computer system will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3250231