Automated Reasoning and Resolution
Download 63.18 Kb.
|
- Navigate this page:
- References [Boyer1984] Boyer, R., and Moore, J S., “Proof checking the RSA public key encryption algorithm”, American Mathematical Monthly 91
| Automated Reasoning and Resolution
Larry Wos Mathematics and Computer Science Division Argonne National Laboratory Argonne, IL 60439-4801
Marked success in puzzle solving, chess playing, computer program writing, or theorem proving in mathematics brings one deep satisfaction and well-deserved accolades. On what does such success rest? What is required to reach the objective in each of these activities? The key factor is careful and deep reasoning, the ability to draw useful and often difficult-to-deduce conclusions. Such fine reasoning must avoid various pitfalls and traps, such as reliance on a hidden and erroneous assumption. For example, what is the problem with the following two so-called facts? Plato likes absolutely everybody. Absolutely nobody likes Plato. Before the answer is given, imagine what would be needed for a computer program to consider the given question as well as far, far deeper questions. First, to submit questions and problems of various types to a computer program, a general language is needed. To draw conclusions in a rigorous manner, sound inference rules are needed. To “know” when the question has been answered or problem solved, a test for assignment completion is needed. And doubtless, at least for deep questions and hard problems, much more is needed. This article focuses on such a language, on diverse inference rules to draw conclusions, on a test for success, and on other key items including the use of strategy. Indeed, although today's computer is startlingly fast, strategy that controls the program's reasoning is crucial. Without reliance on strategy―as is the case for any game requiring mental skill―failure is almost certainly the result, especially if the program is instructed to attack a deep question or hard problem. The context in this article is the field called automated reasoning, a field whose objective is that of designing and implementing a program that applies flawless logical reasoning. At the heart of automated reasoning is what is referred to as “resolution theorem proving” ―the notion of finding proofs, usually by contradiction, of various theorems whose conclusions are drawn by applying inference rules each of which relies on unification (see Section 3). Automated reasoning programs do exist here in the year 2002; some of them are extremely powerful; some are available merely for the asking; and some have been used to make significant contributions to mathematics, to logic, to chip design, and to program verification. If the typical automated reasoning program were given the two so-called facts about Plato, it would find a flaw (in the form of a contradiction) in a few milliseconds. In its language (the clause language) in which logical not is denoted by “-”, the program would consider the two statements LIKES(Plato,x) (for all x) and -LIKES(y,Plato) (for all y) and substitute Plato for x in the first and Plato for y in the second and recognize that a contradiction had been found. The typical test for successful assignment completion is the discovery of a contradiction. 1. Proof and Refutation When trying to prove a theorem of the form P implies Q, two obvious approaches exist. In the first approach (often taken by a person, and almost never by a reasoning program), one begins with the elements of P and makes deductions until one recognizes that Q has been deduced. In the second approach (often taken by a mathematician, and almost always by a reasoning program), one assumes Q to be false and begins reasoning from that assumption or reasoning from P and from the given assumption until a contradiction is found. The recognition of the deduction of a contradiction is the simple test witnessed when Plato was the focus of attention. Phrased differently, the reasoning program seeks refutations of inconsistent sets when it seeks proofs by contradiction. Therefore, whether the context is puzzle solving, circuit design, program verification, or theorem proving in mathematics, the user is asked to phrase the question or problem in a manner that permits the program to seek a refutation in order to complete the assignment. 2. The Clause Language Except for the concept of equality (which is a built-in concept in some of the more powerful automated reasoning programs), the program knows nothing. Whatever information is thought to be needed must be supplied. It can be supplied in first-order predicate calculus (not discussed here) or in the language of clauses, the focus of this section. (Some programs instead rely on higher-order logic, on LISP, or on some other language.) If one chooses first-order predicate calculus, the better programs convert the supplied information into the clause language. The clause language relies on but two explicit logical connectives, not and or, here denoted respectively by “-” and “|”, and one implicit connective, and. (Various conventions are observed regarding notation.) Other connectives are expressed in not and or. For example, if-then, as in if P then Q, is replaced by (the logically equivalent) not P or Q. The language also relies on constants (such as a, b, c, 0, and Plato), functions (such as f, g, h, mother, youngest daughter, and sum), and relations called predicates (such as female, subset, and equals). Variables (denoted by expressions beginning with lower-case u through z) are implicitly universally quantified, each meaning “for all”, and their scope is just the clause in which they occur. For example, the fact that everybody is female or male and the fact that nobody is both female and male are, respectively, conveyed to the program with the following two clauses. FEMALE(x) | MALE(x). -FEMALE(x) | -MALE(x). In the preceding, each of the items separated by or is called a literal, and a clause is the or of its literals with the requirement that no literal may appear more than once in a clause. The empty clause contains no literals. The occurrence of the variable x in the two given clauses is, in effect, coincidental; the program will behave the same if the second clause has its occurrences of x replaced by y. As for existence, the language relies on appropriate (Skolem) functions; existentially quantified variables are not acceptable. For example, the fact that for every \fIx\fR there exists a \fIy\fR with \fIy\fR greater than \fIx\fR is expressed with the following clause. GREATERTHAN(f(x),x). The dependence of y on x―the fact that as x varies, y may vary―is reflected in the given clause. In contrast, when such a dependence is not present, as in the case where there exists a nonnegative number y such that for all nonnegative x, y is less than or equal to x, a constant (function of no arguments) suffices. LESSOREQUAL(a,x). An important and sometimes overlooked subtlety of the language focuses on the use of functions in contrast to the use of predicates. The former requires uniqueness (in the sense of unambiguous and well defined), where the latter does not. For example, a function can be used to convey information to the program about maternal grandfather because no ambiguity is present; but a predicate is required if the focus is merely on grandfather because then ambiguity is present, in the sense that more than one choice exists. For a second example, the notion of successor (to a number) is unique and well defined, and a function suffices; but the concept of divisor requires the use of a predicate. The clause language can hardly be called a rich language. From the user's or researcher's perspective, more richness would appear to be quite preferable. However, its lack of richness, rather than being a hindrance to the program and to automated reasoning in general, is an advantage. More richness would interfere somewhat with the formulation of computer-oriented inference rules and, most important, would play havoc with the introduction of powerful and effective strategies for controlling the reasoning. As for such inference rules, the key to each of them is unification, which is also the key to other vital components of automated reasoning. 3. Unification Computer-oriented reasoning differs from person-oriented reasoning in the former's emphasis on generality. The use of unification, a procedure key to so many aspects of automated reasoning, illustrates this difference nicely. Unification takes two expressions and seeks a most general substitution of terms for variables that, when applied to each of the two, yields two (possibly) new expressions that are identical [Robinson1965b]. In the earlier example about Plato, the program found that unification succeeded, yielding the substitution of Plato for both x and y to discover a contradiction. Of course, unification can fail, as is the case with the following two clauses. P(x,x). -P(f(y),y). Indeed, consideration of these two clauses does not yield a contradiction; ignoring the not symbol, no substitution exists that can be applied to the two that yields identical expressions. Regarding an illustration of the generality of a program's reasoning (in contrast to that often employed by a person), the following three clauses serve well. -P(x,y,z) | Q(y,z,x). P(a,b,u). Q(b,z,a).
.(l
Q(b,b,a). Q(b,a,a). Q(b,c,a). Q(b,h(b,a,b),a). However, the four given less general conclusions would not have been drawn by a reasoning program because of its preference for generality and because unification would not have yielded the appropriate substitution. STOP
For a second example (of the type that can often be found in a paper or book written by a logician), where the program might deduce a clause that (in effect) says that \fIx\fR implies \fIx\fR, a person might prefer to deduce (\fIy\fR implies z) implies (\fIy\fR implies \fIz\fR). The latter deduction is called an \fIinstance\fR of the former, and it can be obtained by replacing the variable \fIx\fR by the term (\fIy\fR implies \fIz\fR). A researcher's preference is often based on experience, intuition, and knowledge of what is likely to suffice for the task at hand, where the program lacks all three. On the other hand, where the generality evident in the program's approach contributes to its effectiveness, such generality can actually interfere with a person's attack. .sh 1 "Inference Rules" #4 .pp Unification plays a key role in each of the inference rules used to draw conclusions. Each inference rule is required to be \fIsound\fR, to yield conclusions that follow inevitably from the hypotheses to which it is applied. Some inference rules apply to pairs of hypotheses in the form of clauses; some to two or more; and (currently in automated reasoning) one to a single hypothesis. Regarding equality, one heavily used inference rule treats the relation as if it is understood (built-in). .pp The inference rule that dominated the field in the early 1960s was binary resolution [Robinson1965b], sometimes loosely called resolution. This rule requires two clauses as hypotheses, focuses on one literal in each clause with the same predicate and opposite sign, and seeks to unify the chosen literals. If unification succeeds, the two literals are canceled (ignored), and the unifier (substitution) is applied to the remaining literals in both clauses that are then used to form a new clause by taking their \fBor\fR, ignoring duplicates. The example focusing on \fIP\fR and \fIQ\fR in Section 3 illustrates the use of binary resolution, as does the following in which the third of the three clauses can be obtained from applying the inference rule to the first two. .(l -P(a,x) | -Q(x). P(y,b) | -R(y). -Q(b) | -R(a). .)l .pp
As defined, binary resolution requires the presence of another inference rule, \fIfactoring\fR, in order to guarantee that assignments that should be completable can be completed. Factoring focuses on a single clause, chooses two of its literals that are alike in both predicate and sign, and seeks to unify the two. If successful, the unifier is applied to the clause to yield the conclusion. For example, factoring applied to the first of the following four clauses yields (depending on the two literals being unified) three different conclusions, the second through the fourth. .(l
Q(f(x),y) | Q(f(u),g(v)) | Q(f(x),g(v)). Q(f(x),g(v)). Q(f(x),g(v)) | Q(f(u),g(v)). Q(f(x),y) | Q(f(x),g(v)). .)l .pp
As the following simple example shows, binary resolution without factoring would not find the desired refutation for the inconsistency that is present. .(l
P(x) | P(y) -P(u) | -P(v). .)l .pp
Among other inference rules that are heavily relied upon, one (\fIhyperresolution\fR [Robinson1965a]) requires that the deduced clause be free of \fBnot\fR, one (\fIUR-resolution\fR [McCharen1976]) requires that the conclusion be free of \fBor\fR and be nonempty, and one (\fIparamodulation\fR [Robinson1969]) offers equality-oriented reasoning. Hyperresolution and UR-resolution can consider as hypotheses two or more clauses at a time; paramodulation focuses on pairs of clauses. All three of these inference rules offer far more power in general than does binary resolution. Many of the cited inference rules have been generalized to a class called \fIlinked inference rules\fR [Veroff1992], replacing syntactic criteria with semantic criteria for conclusion acceptance. .pp As the following example shows, where the third of the three clauses is obtained by applying paramodulation \fIfrom\fR the first \fIinto\fR the second, paramodulation is one of the most graphic examples of a type of reasoning well suited to the computer but ill suited to a person. To more fully understand the example, note that unification is applied to the term \fIsum\fR(\fIx,minus\fR(\fIx\fR)) (in the first clause) and the term \fIsum\fR(\fIminus\fR(\fIy\fR),\fIz\fR) (in the second clause), yielding a substitution that asks for \fIx\fR to be replaced by \fIminus\fR(\fIy\fR) and \fIz\fR by \fIminus\fR(\fIminus\fR(\fIy\fR)). The application of this substitution produces two new clauses, respectively instances of the first and second, such that the pair contains two identical expressions. By the nature of equality, one can then substitute \fIfrom\fR the first new clause \fIinto\fR the second new clause. .(l EQUAL(sum(x,minus(x)),0). EQUAL(sum(y,sum(minus(y),z)),z). EQUAL(sum(y,0),minus(minus(y))). .)l .sh 1 "Strategy" #5 .pp The introduction of strategy, more than any other component, has contributed to the advance of and successes of automated reasoning. Various strategies restrict the program's reasoning, various direct it, and various affect it in some other important manner. Without strategy, just as is true for a person studying a deep question or hard problem, the program can wander aimlessly without success, often drowning in information that proves useless for the task at hand. Although not immediately obvious, the various strategies that have proved to be powerful in the context of automated reasoning are dependent neither on the clause language nor on any particular program that offers them. Nevertheless, few reasoning programs offer a wide variety and, as a result, offer less power than is possible. .pp Of the restriction strategies, the \fIset of support\fR strategy has proved to be the most powerful [Wos1965]. With this strategy, the user chooses a subset \fIT\fR of the input clauses, and the program is not allowed to draw a conclusion from hypotheses all of which are input clauses not in \fIT\fR. Therefore, the program is restricted to drawing conclusions that are recursively traceable to one or more clauses in \fIT\fR. In effect, the input clauses not in \fIT\fR are used only to complete the application of an inference rule. .pp The set of support strategy meshes beautifully with seeking a proof by contradiction in that a reasonable choice for \fIT\fR is \fBnot\fR \fIQ\fR, where the theorem to be proved is of the form \fIP\fR implies \fIQ\fR. A more effective choice has \fIT\fR be \fBnot\fR \fIQ\fR together with those elements of \fIP\fR that are not among the basic information (axioms). A third choice for \fIT\fR, often more effective than the preceding, has \fIT\fR be just those elements of \fIP\fR that are not among the axioms. .pp A strikingly different type of restriction strategy has the user place an upper bound on the complexity of deduced information that is retained. In the same spirit, the user can restrict the program from retaining any conclusion in which more than \fIk\fR distinct variables occur, where \fIk\fR is chosen by the user. The program can also be restricted from retaining new conclusions that contain any term designated as undesirable. For example, where the function \fIn\fR denotes negation, if the user decides that new conclusions in which \fIn\fR(\fIn\fR(\fIt\fR)) is present for some term \fIt\fR are to be discarded, the program will do so. Use of this strategy has enabled a reasoning program to discover proofs that had been missing for many, many decades, perhaps by exploring paths that were counterintuitive to the great minds. .pp As for strategies that direct a program's reasoning and focus, R. Overbeek's \fIweighting\fR strategy [McCharen1976] offers appeal in that its use enables the user to impose knowledge, experience, and intuition on the program's actions. With that strategy, templates can be included that (in effect) assign priorities to various types of term. For example, the user can instruct the program to give great preference to sums of products, give lesser preference to terms in which minus occurs, and give little or no preference to terms in which 0 occurs. .pp The \fIresonance\fR strategy [Wos1995] is another strategy that enables the user to impart knowledge and experience and intuition to the program. The user supplies equations or formulas whose functional pattern (treating all variables as indistinguishable) is conjectured to merit preference. .pp A far more naive and in some sense natural direction strategy is that of breadth first (first come first serve). Its opposite, depth first, is found in programs based on logic programming; see Section 9. Although such programs offer impressive speed for simple theorems, for even moderately deep theorems (in most cases) they lack sufficient power. Nevertheless, a breadth-first search can occasionally prove profitable, and its cousin the \fIratio\fR strategy is indeed useful. That strategy instructs the program to blend the directing of its reasoning by complexity preference (through weighting) with that of breadth first. .pp
Unlike restriction strategies and direction strategies, the \fIhot list\fR strategy [Wos1999] enables the program to visit, revisit, and re-revisit and so on some user-chosen items, items among those input to present the question or problem to be attacked. For example\(emand quite reminiscent of that which occurs in mathematics\(emconsider the theorem that asserts the provability of commutativity for rings in which \fIxxx = x\fR for all \fIx\fR. By placing the clause equivalent of \fIxxx = x\fR in the hot list, each time a new clause is retained and before any other reasoning action is taken, the hot list strategy will apply the chosen inference rules to the new clause together with the clause equivalent of \fIxxx = x\fR. This action can radically reorder the space of retained conclusions and, in turn, sharply reorder the clauses chosen to drive the program's reasoning. Sometimes proofs that would have been out of reach are easily proved by the program. .sh 1 "Subsumption and Redundancy" #6 .pp The fact that \*(lqKim's daughter is female\*(rq is a trivial consequence and instance of the fact that \*(lqeverybody's daughter is female\*(rq. If the latter information is present and the former deduced, the procedure \fIsubsumption\fR [Robinson1965b] will purge the less general bit of information. The program, as noted, prefers generality. If both bits of information were retained, then a type of redundancy would be present, which would interfere with effectiveness. By instructing the program to avoid the use of subsumption, an examination of the set of conclusions that can easily be deduced and retained reveals (to the uninitiated) a startling amount of information useless to the program. .pp To see whether one clause subsumes a second, the program seeks a substitution of terms for variables in the first that yields a subset of the second, even if the first clause consists of more literals than does the second. Indeed, in the following, the first clause subsumes the second. .(l
P(a,x) | P(y,b). P(a,b).
.)l .sh 1 "Demodulation and Simplification" #7 .pp Although a researcher often automatically simplifies expressions\(emfor example, replacing 0+\fIt\fR by \fIt\fR, where \fIt\fR is a term\(ema reasoning program does not unless instructed to do so. Therefore, if appropriate actions are not taken, much redundancy of a semantic type can be present within the database of deduced information: \fIa+b = c\fR, \fIa+b = c\fR+0, 0+\fIa+b = c\fR, and the like. This type of redundancy is quite different from that in focus when subsumption was discussed. Its avoidance is through another means, namely, the use of \fIdemodulation\fR [Wos1967]. .pp Indeed, the inclusion in the input of appropriate demodulators (rewrite rules) enables a reasoning program to simplify newly deduced conclusions and also to canonicalize them. Associativity is a fine example. In particular, the program can automatically right associate expressions, rewriting (\fIa+b\fR)+\fIc\fR to \fIa\fR+(\fIb+c\fR). If given permission, the set of input demodulators can be supplemented by new ones deduced during the program's study of a question or problem. .sh 1 "Soundness and Completeness" #8 .pp The programs in focus\(emin particular, their inference rules\(emare \fIsound\fR, meaning that any conclusion that is drawn follows inevitably from the hypotheses to which the rule is applied. Of course, a false conclusion can be drawn if the program is given false information, such as \*(lqfinches are mammals\*(rq and the like. This soundness property guarantees that the proofs the program finds are without flaw, barring a bug in the program or the inclusion of erroneous items. However, if one suspects that the supplied proof is not sound and wishes substantial assistance in checking it, one can rely on an option offered by the better programs to obtain a detailed accounting. .pp As for completeness, the typical program admits a use that is \fIrefutation complete\fR, meaning that, when given an inconsistent set of statements, the program will eventually complete a proof by contradiction, but sometimes an inordinate amount of CPU time is required. Such refutation completeness is often forsaken in order to promote effectiveness. Indeed, many combinations of strategies, inference rules, and procedures lack refutation completeness and are, nevertheless, heavily relied upon. In such cases, the usually bizarre examples that show that such completeness is lacking are merely illustrative and not relevant to serious studies. Often overlooked is the fact that the set of proofs for a given theorem is so large that the absence of refutation completeness almost never presents a practical problem. .pp Rarely does a reasoning program offer \fIdeduction completeness\fR, the guarantee that a consequence that follows from the hypotheses that are given to present a question will be eventually deduced. For example, even though Kim is mentioned in a puzzle and the program is told that everybody is female or male, most unlikely is the occurrence of deducing that Kim is female or male. The well-known inference rule \fIinstantiation\fR would suffice to draw the cited conclusion from the more general fact, but that rule is almost never offered by a reasoning program because of the difficulty of adequately controlling its use. The myriad (usually an infinite set of) instances is at the heart of the problem, and quite often the simplest instance is not what is needed. .sh 1 "Logic Programming" #9 .pp
Logic programming is concerned with languages whose instruction set is based on the direct use of clauses. Prolog is the best known, of its various dialects. Many similarities exist between logic programming and automated reasoning [Wos1991]. Indeed, in the mid-1980s, some thought that the most effective means for automating logical reasoning was to base the design of a program on logic programming. .pp
Clearly, such a program offers great speed for proving simple theorems [Stickel1988]. However, it lacks the needed power to tackle deep questions and hard problems. One of the main drawbacks is the absence of an arsenal of diverse strategies. Implicitly such a program does rely on a depth-first search and on the use of the set of support strategy. As history shows, many additional strategies are needed for the type of power required to prove, for example, interesting theorems. .pp
Among other serious drawbacks is that concerning the lack of information retention. Indeed, experimentation strongly suggests that new conclusions must be retained if deep questions and hard problems are to be successfully attacked. .sh 1 "Successful Applications" #10 .pp Despite the obstacles that, to many, seemed insurmountable even as late as the late 1970s, automated reasoning (which was so named in 1980) has prospered, and prospered greatly. Two distinct classes of success merit mention: design and verification, and mathematics and logic. The Boyer-Moore theorem prover has been used to prove the invertibility of the Rivest, Shamir, and Adleman public key encryption algorithm [Boyer1984], and various chip-designing firms (for example, Intel and AMD) are now relying on automated reasoning programs to aid them by proving numerous theorems. Perhaps the future will witness a combination of elements from each class, say, the application, to the design of simpler chips and circuits, of proof-shortening techniques used for mathematics and logic. .pp
In the second class, mathematics and logic, open questions have been answered, missing proofs found, and existing proofs improved upon in various ways. Of the open questions that were answered, the most recognized success concerns proving that every Robbins algebra is a Boolean algebra [McCune1997]. Most recently, new two-axiom systems for Boolean algebra using the Sheffer stroke have been found [Veroff2001]. Automated reasoning programs have also made substantial contributions in areas that include groups [Hart1995; Kunen1992], combinatory logic [Glickfeld1986; Wos1993], abstract algebra [McCune1996], and logical calculi [Harris2001; Fitelson2001]. .uh "Further Reading" .pp
More than twenty-five years ago, C. Chang and R. Lee coauthored the book \fISymbolic Logic and Mechanical Theorem Proving\fR (Academic Press, New York, 1973), which provides a thorough treatment of the clause language paradigm as well as proofs of the theorems that establish the needed logical properties of various inference rules and strategies. Another classic text is D. Loveland's book \fIAutomated Theorem Proving: A Logical Basis\fR (Elsevier Science, 1978). .pp
A more recent introductory book that serves well in guiding the reader through the basics of automated reasoning and its applications and that offers numerous open questions and research topics is \fIA Fascinating Country in the World of Computing: Your Guide to Automated Reasoning\fR by L. Wos and G. W. Pieper (World Scientific Press, Singapore, 1999). More technical is the text by J. Kalman entitled \fIAutomated Reasoning with Otter\fR (Rinton Press, Princeton, 2001); the book covers such topics as how to convey a problem to an automated reasoning program, how to find a proof by contradiction, and how to reason about equality. Both books include a CD-ROM with the automated reasoning program OTTER (designed and implemented by McCune). An equally rigorous book is a graduate-level text by M. Fitting entitled \fIFirst-Order Logic and Automated Theorem Proving,\fR (Springer-Verlag, Berlin, 1996); the book presents fundamental concepts and results of classical logic. .pp
.pp For a history of the field and relevant papers, one might consult \fIThe Automation of Reasoning: Collected Papers from 1957 to 1970\fR edited by J. Siekmann and G. Wrightson (Springer-Verlag, New York, 1983) and, more recently, \fIThe Collected Works of Larry Wos\fR, by L. Wos with G. W. Pieper (World Scientific, Singapore, 2000); this latter book provides a convenient source for all of the papers by Wos cited in the references. .pp Finally, for reviews of the field, two encyclopedia articles are of interest. The first article, \*(lqResolution, Binary: Its Nature, History, and Impact on the Use of Computers\*(rq, by L. Wos and R. Veroff, is in the \fIEncyclopedia of Artificial Intelligence\fR (2nd ed., John Wiley & Sons, New York, pp. 1341-1353, 1992). The second article, \*(lqLogical Basis for the Automation of Reasoning: Case Studies\*(rq, by L. Wos and R. Veroff, is in the \fIHandbook of Logic in Artificial Intelligence and Logic Programming\fR (ed. D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Oxford University Press, Oxford, 1994, pp. 1-40). Acknowledgments This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Advanced Scientific Computing Research, U.S. Department of Energy, under Contract W-31-109-Eng-38. References [Boyer1984] Boyer, R., and Moore, J S., “Proof checking the RSA public key encryption algorithm”, American Mathematical Monthly 91 (1984) 181-189. [Fitelson2001] Fitelson, B., and Wos, L., “Missing Proofs Found,” J. Automated Reasoning 27, no. 2 (2001) 201-225. [Glickfeld1986] Glickfeld, B., and Overbeek, R., “A Foray into Combinatory Logic,” J. Automated Reasoning 2, no. 4 (1986) 419-431. [Harris2001] Harris, K., and Fitelson, B., “Distributivity in L aleph 0 and other sentential logics”, J. Automated Reasoning 27, no. 2 (2001) 141-156. [Hart1995] Hart, J., and Kunen, K., “Single axioms for odd exponent groups”, J. Automated Reasoning 14, no. 3 (1995) 383-412. [Kunen1992] Kunen, K., “Single axioms for groups”, J. Automated Reasoning 9, no. 3 (1992) 291-308. [McCharen1976] McCharen, J., Overbeek, R., and Wos, L., “Complexity and related enhancements for automated theorem-proving programs”, Computers and Mathematics with Applications B2 (1976) 1-16. [McCune1996] McCune, M., and Padmanabhan, R., Automated Deduction in Equational Logic and Cubic Curves, Lectures Notes in Computer Science 1095, Springer-Verlag, New York, 1996. [McCune1997] McCune, W., “Solution of the Robbins problem”, J. Automated Reasoning 19, no. 3 (1997) 263-276. [Robinson1969] Robinson, G., and Wos, L, “Paramodulation and theorem proving in first-order theories with equality”, pp. 135-150 in Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh University Press, 1969. [Robinson1965a] Robinson, J. A., “Automatic deduction with hyper-resolution”, International J. Computer Mathematics 1 (1965) 227-234. [Robinson1965b] Robinson, J. A., “A machine-oriented logic based on the resolution principle”, J. ACM 12 (1965) 23-41. [Stickel1988] Stickel, M., “A Prolog technology theorem prover”, J. Automated Reasoning 4, no. 4 (1988) 353-380. [Veroff1992] Veroff, R., and Wos, L., “The linked inference principle, I: The formal treatment\*(rq, \fIJ. Automated Reasoning\fR \fB8\fR, no. 2 (1992) 213-274. [Veroff2001] Veroff, R., “Solving open questions and other challenge problems using proof sketches”, J. Automated Reasoning 27, no. 2 (2001) 157-174. [Wos1965] Wos, L., Robinson, G., and Carson, D., “Efficiency and completeness of the set of support strategy in theorem proving”, J. ACM 12 4 (1965) 536-541. [Wos1967] Wos, L., Robinson, G., Carson, D., and Shalla, L., “The concept of demodulation in theorem proving”, J. ACM 14 (1967) 698-709. [Wos1991] Wos, L., and McCune, W., \*(lqAutomated theorem proving and logic programming: A natural symbiosis\*(rq, \fIJ. Logic Programming\fR \fB11\fR, no. 1 (1991) 1-53. [Wos1993] Wos, L., “The kernel strategy and its use for the study of combinatory logic”, J. Automated Reasoning 10, no. 3 (1993) 287-343. [Wos1995] Wos, L., “The resonance strategy”, Computers and Mathematics with Applications”, J. Automated Reasoning 29, no. 2 (1995) 133-178. [Wos1999] Wos, L., with Pieper, G. W., “The hot list strategy”, J. Automated Reasoning 22, no. 1 (1999) 1-44. Directory: pub -> People -> pieper pub -> Baltic Olympiads in Informatics: Challenges for Training Together pub -> Preparation of Papers for ieee transactions on medical imaging pub -> Forthcoming meetings and conferences pub -> Asilomar Conference on Circuits, Systems & Computers, Pacific Grove, ca, November 1978, pp. 55 58 pub -> Forthcoming meetings and conferences pub -> Harmonised compatibility and sharing conditions for video pmse in the 7 9 ghz frequency band, taking into account radar use pieper -> Final Version 2 nd April 2003 Chapter 23 Knowledge and the Grid People -> Introduction to Computer Science Mgr inż. Kamil Kuliberda Batch File Command People -> Laboratory 1 Download 63.18 Kb. Share with your friends:
|