Homogenization: Preparing Equations for Change of Unknown
Proceedings of the Seventh International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 551-552.
© 1981 International Joint Conferences on Artificial Intelligence
Abstract
PRESS is a computer program for solving symbolic, transcendental, non-differential equations, [3]. We describe a new equation solving method, called Homogenization, which we have implemented in PRESS. Homogenization prepares equations, so that they can be solved by the Change of Unknown method. It does this by causing different occurrences of the unknown to occur within identical subterms. The method has application, outside equation solving, to the problem of generalizing expressions.
- REFERENCES Aubin, R. Some generalization heuristics in proofs by induction. In Huet, G. and Kahn, G., editor,~~ Collogue Construction: Amelioration ~ verification~ Prggra;mes. , 1975.
- Boyer, R.S. and Moore, J.S . A&M monograPh ~. A Computational ~. Academic Press, 1979.
- Bundy, A. and Welham, B. Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation. Artificial Intelligence 16(2), 1981.
- Silver, B. and Bundy, A. Homogenization: Preparing Equations ~ ~ .Q.( Unknown. Research Paper 159, Dept. of Artificial Intelligence, Edinburgh, June, 1981.
References were extracted automatically from the PDF and may contain errors.
Full text extracted automatically from the PDF; figures, tables and equations may differ. The PDF is the version of record.
ABSTRACT
PRESS is a computer program for solving symbolic, transcendental, non-differential equations, [3]. We describe a new equation solving method, called Homogenization, which we have implemented in PRESS. Homogenization prepares equations, so that they can be solved by the Change of Unknown method. It does this by causing different occurrences of the unknown to occur within identical subterms. The method has application, outside equation solving, to the problem of generalizing expressions.
I INTRODUCTION
A common method of change the unknown, e.g. solving equations is if the equation is to
then the equation may be solved by substituting y = log 2 x and solving the resulting disguised quadratic
Unfortunately, things are seldom as simple as this. Equations, which can be solved by Change of
Unknown, are more likely to appear in the form
in which the occurrences of the unknown, x, appear within dissimilar subterms., namely logx2 and log2x. Some preparation of the equation is required before the unknown can be changed. In the case of our example, the subterm logx2 must first be converted
to 1/log 2 x, with the aid of the rewrite rule
We call this preparation step Homogenization, because it makes the occurrences of x appear in identical subterms. In this paper we describe the implementation of a version of Homogenization.
II SOME TERMINOLOGY
Before we can describe the Homogenization method
we mus.t introduce some terminology.
- The original equation, prior to
This research GR/B 2925.2 and Silver. was an supported by SRC grant no SRC studentship to Bernard
Alan Bundy and Bernard Silver
Department of Artificial Intelligence University of Edinburgh
Homogenization, will be called the input equation, and the resulting equation will be called the output equation.
- The output equation belongs to a class of
- equation which we will call the base class. We have restricted the base class to Algebraic equations, 1. e those involving only the functions +, -, ·, I and exponentiation to a rational number power. This covers all the examples we have found in text books and exam papers. In fact most output equations are (sometimes disguised) quadratics. Any class of equations could be used as the base class, but the idea is to pick a class whose members are relatively easy to solve.
- The input equation can always be regarded as an Algebraic equation .1n ~ ~ 2f. non-Algebraic subterms in x, e.g. equation (i) above can be regarded as an Algebraic equation in the set {logx2, log 2 xJ. These subterms are called the offending terms and the set of them is called the offenders set. The idea is that this is a set of subterms preventing the equation being Algebraic: a class of equations which PRESS knows a lot about.
- The essence of the Homogenization method is to
- replace each of the offending terms by some Algebraic function of a single term, called the reduced term. In the example above the reduced term is log 2 x.
III THE HOMOGENIZATION METHOD
The Homogenization method is as follows:
- (a) The offenders set is found by trying to parse the input equation as an Algebraic equation. When the parse is blocked, because the current subterm is x or a non-Algebraic subterm containing x, then this is added to the offenders set and the parse forced to continue.
- (b) If the offenders set is a singleton then we
- must distinguish three cases.
- ( 1 ) The singleton is the unknown, x. The
- equation is already algebraic so exit.
- The singleton is a function of x, f(x)
- say, which occurs at least twice in the
input equation. Exit with success as now the Change of Unknown method can be applied to the output equation,
substituting y for f(x).
- ( 3) The singleton is a function of x as above, but occurs only once in the equation. In this case again the Change of Unknown method cannot be used so exit with failure. This case includes examples like
- (c) Classify the input equation according to its offenders set. For example, if all the offenders are trigonometric terms, then the equation is of type trigonometric. The types currently used are: trigonometric, exponential, hyperbolic, logarithmic and mixed (the miscellaneous type). The classification scheme is explained in more detail in the long version of this paper, [ 4].
- (d) A reduced term is selected. The type of the input equation determines how this term is chosen, different techniques are needed for trigonometric equations than for exponential equat-ions, for example. For mixed type, where the special techniques fail, the reduced term is chosen from the offenders set on the basis of a simple simplicity measure.
- (e) Now an attempt is made to rewrite each term in the offenders set as an Algebraic function of the reduced term. In order to avoid the inefficiences of random search, we have designed the program to make maximum use of its syntactic analysis of the input equation. Thus a special rewrite rule set is used for each of the equation types (see [4] for details). For mixed types each rewrite must be done in single step: with a rule of the
- form
ot => af(rt)
where ot matches the offending term, rt matches the reduced term and af is an Algebraic function. If some of the offending terms cannot be rewritten, then backtrack to choose a new reduced term if this is
possible, otherwise fail.
- (f) Substitute the rewrites for the offending terms in the input equation to give the output equation. This equation is now an Algebraic equation of the reduced term, i.e. it is homogenized, so exit with success. Change of Unknown can now be successfully applied, substituting y for the reduced term
- in the output equation.
IV RESULTS AND EXAMPLE EQUATIONS
During our survey of exam papers we discovered 27 questions on which the Homogenization method could be used, although in some examples other,
better, methods could be used. Of these 27, 25
were successfully processed by our implementation of Homogenization, that is the correct output equation was found. The rest of PRESS was then able to solve 11 of these output equations. The 2 examples where Homogenization failed are discussed in the long version of this paper.
Here are some examples of equations which have been solved using Homogenization:
9.cosh(x) - 6.sinh(x) = 7
(A level London 1976)
(A level London 1977)
(A level London 1977)
(A level A.E.B. 1975)
cos(x) + cos(3x) + coa(5x) = 0 . (A level A.E.B. 1976)
V GENERALIZATION
Change of Unknown is very similar to the method of Generalization in the program-property theorem-prover of Boyer and Moore, [ 2]. Before proving a theorem by induction, the Boyer-Moore theorem-prover is able to generalize it by replacing several occurrences of the same subterm by a new skolem constant, e.g. (rev a) in
(equal (append (rev a) (append b c)) (append (append (rev a) b) c))
is replaced by d to produce
(equal (append d (append b c)) (append (append d b) c))
which is then solved by induction.
Work by Boyer, Moore and Aubin, [1], has concentrated on the question of when Generalization is to be done, which occurrences of a subterm are to be replaced and what additional assumptions may need to be introduced to prevent over-generalization. These are not issues in equation solving. There is never a danger of over-generalization and all occurrences of a subterm should always be generalized (i.e. changed to a new unknown).
The method of Homogenization described above is complementary to the work done by Boyer, Moore and Aubin, because it suggests how an expression may be prepared for Generalization: subterms which were not previously identical may be made so, in order to allow Generalization to proceed.
VI CONCLUSIONS
We have described the Homogenization method, which prepares equations for solution by Change of Unknown. This work further illustrates the role of meta-level inference in algebraic manipulation (see
- [3]). Meta-level inference consists of a syntactic analysis of the input equation to determine appropriate algebraic solution steps. In this case the syntactic analysis reveals the offenders set, picks a reduced term and, hence, suggests what rewrite rules to apply.
We have found that the problem of selecting the reduced term is one that requires something more than a general purpose metho~. Although the simplicity method, used for equations of mixed type is often successful on any equation, there are many problems for which it is inadequate. Thus we have implemented special purpose methods for some types of equations, and these have proved to be of great value. Similar remarks apply to the rewriting of offending terms. We are continuing the development of these methods.
@inproceedings{ijcai1981p103,
title = {Homogenization: Preparing Equations for Change of Unknown},
author = {Bundy, Alan and Silver, Bernard},
booktitle = {Proceedings of the Seventh International Joint Conference on
Artificial Intelligence, {IJCAI-81}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Patrick J. Hayes},
pages = {551--552},
year = {1981},
month = {8},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1981/103},
}
TY - CPAPER TI - Homogenization: Preparing Equations for Change of Unknown AU - Bundy, Alan AU - Silver, Bernard T2 - Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81 PB - International Joint Conferences on Artificial Intelligence PY - 1981 SP - 551 EP - 552 UR - https://ijcai.org/proceedings/1981/103 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
Welcome
Future Conferences
AI Journal Division
IJCAI Proceedings
About IJCAI
IJCAI Awards