A deductive database approach to automated geometry theorem proving and discovering

MM Research Preprints,1–20

No.17,Dec.1998.Beijing1

A Deductive Database Approach to Automated

Geometry Theorem Proving and Discovering1)

Shang-Ching Chou Xiao-Shan Gao Jing-Zhong Zhang

Dep.of Computer Science Inst.of Systems Science Inst.of Computer App.

Wichita State University Academia Sinica Academia Sinica

Wichita,KS67260,USA Beijing100080,China ChengDu610015,China

Abstract.We report our e?ort to build a geometry deductive database,which can be used to?nd the?xpoint for a geometric con?guration.The system can?nd all the properties of the con?guration that can be deduced using a?xed set of geometric rules.To control the size of the database,we propose the idea of a structured deductive database.Our experiments show that this technique could reduce the size of the database by one hundred times.We propose the data-based search strategy to improve the e?ciency of forward chaining.We also make clear progress in the problems of how to select good geometric rules,how to add auxiliary points,and how to construct numerical diagrams as models automatically.The program is tested with one hundred sixty nontrivial geometry con?gurations.For these geometric con?gurations,the program not only?nds most of their well-known properties but also often gives unexpected results,some of which are possibly new.Also,the proofs generated by the program are generally short and totally geometric.

Key words.Deductive database,automated geometry theorem proving and discovering, search strategies,redundant deduction,skolemization,structured database.

1.Introduction

1.1Introduction.The aim of this paper is to develop a geometry deductive database which can be used to prove or discover nontrivial geometry theorems by exploring the full strength of forward chaining.For a given geometric con?guration,the program can?nd its?xpoint with respect to a?xed set of geometric rules or axioms;i.e.,it can?nd all the properties of the con?guration that can be deduced using these axioms.

The basic ideas behind the program,such as?xpoints and the treatment of negative clauses,come from the deductive database theory[?].Our contributions are as follows:(1) In the general setting,we propose the idea of the structured deductive database and the data-based search strategy to improve the search e?ciency.(2)In the geometry reasoning setting, we show how to select a good set of rules,how to add auxiliary points,and how to construct numerical diagrams as models automatically.

1)

This work was supported in part by the NSF Grant CCR-9420857and the Chinese NSF.

2S.C.Chou,X.S.Gao,J.Z.Zhang

We tested the program with one hundred sixty geometry con?gurations ranging from well-known geometry theorems such as the centroid theorem,the orthocenter theorem,and Simson’s theorem to problems recently proposed in the problem section of the American Mathematical Monthly.The program not only?nds most of the well-known properties of these con?gurations but also often gives many unexpected results,some of which are possibly new(see Example??).As we know,most of the one hundred sixty theorems can not be proved by the previous programs based on synthetic approaches.The strength of our program is mainly based on the following improvements.

In traditional deductive databases,each n-ary predicate is associated with an n-dimensional relation.Since most of the geometric predicates satisfy special properties such as transitivity and symmetry,the traditional way of representing a database is not suitable for building a geometry deductive database for two reasons:the excessively large database and repetitive representation of information.On average,the databases for the160tested geometry con-?gurations would be of size242,117if using the traditional representation.We solve this problem by using some simple mathematical structures such as sequences and equivalent classes to represent facts in the database.The average size of the structured databases for the160con?gurations is221.So the size of the structured database is one hundred times smaller.

We propose the data-based search strategy as opposed to the previous rule-based search strategy.In the data-based search,we keep a list of“new data”and for each new data the system searches the rule set(or intensional database)to?nd and apply the rules using this data.If using the data-based strategy,the redundant deductions caused by repeated application of a rule to the same facts will be automatically eliminated.In this aspect, the data-based strategy is similar to the semi-naive strategy[?].However,the data-based strategy also uses the combined rules and dynamic database update strategies to further improve e?ciency.Also,the data-based search strategy is particularly e?cient in the case of a structured database,since in such a database a fact could represent a large amount of information.For instance,a fact could be“ten triangles are similar to each other.”

All the previous work based on the synthetic approach[?,?,?,?]uses geometric rules about congruent triangles as its basic geometric rules.Without adding techniques about auxiliary points,these rules can be used to prove a limited number of high school level theorems involving straight lines only.Most of the basic results in geometry such as the centroid theorem,the orthocenter theorem,and Simson’s theorem are beyond the scope of these rules.In Section??,we will discuss three concerns about selecting a set of geometric rules:the number of proof steps,the auxiliary points,and the order relation.We also show how to solve some of the related problems by selecting good rules.

We discuss how to make the adding of auxiliary points or Skolemization in geometry reasoning practically possible.About twenty rules of adding auxiliary points are implemented and thirty nine of the one hundred sixty con?gurations solved by our program need auxiliary points.This is the?rst implementation of a nontrivial set of rules of adding auxiliary points.

Numerical diagrams of geometry statements are used as models to deal with the negative information in the rules.Our program can construct the diagram automatically for a class of linear constructive geometry statements(see Section2.3).In all the previous work using diagrams as models[?,?,?],the diagrams are constructed by the user.

Deductive Database Approach3 1.2Related Work.There are mainly three approaches to automated geometry reasoning: the approach based on synthetic deduction[?,?,?,?,?],the approach based on algebraic computation(mainly Wu’s method and the Gr¨o bner basis method)[?,?,?],and the geometric invariant approach,like the area method[?]and the methods given in[?,?].Other interesting work can be found in[?,?,?].

We will discuss the synthetic approaches below because they are more closely related to this paper.Most of the synthetic approaches to automated geometry theorem proving use backward chaining[?,?,?].In[?],Nevins used a combination of forward chaining and backward chaining with emphasis on the forward chaining.But the?xpoint is not reached. All the synthetic approaches except Nevins’use numerical diagrams as models.The idea of adding auxiliary points is discussed in[?,?]but not implemented.More about this topic can be found in Section5.All previous synthetic work deals with theorems involving straight lines only.The problem of including circles into the program is discussed but not implemented in[?].Our program,using geometric rules with the full-angle congruence as the central concept,can deal with theorems involving circles naturally.

Generally speaking,the algebraic approaches are decision procedures and are more pow-erful.The synthetic approaches,including the one in this paper,are not decision procedures. In theory,all theorems that can be proved with the method reported in this paper can also be proved with algebraic methods such as Wu’s method.Despite its“weakness,”it is still worth improving the synthetic approach because this may lead to techniques useful to automated reasoning in the general case.Even for automated geometry reasoning alone,improving the synthetic method has the following positive aspects:(1)Proofs produced by synthetic methods are generally easier to understand than proofs given by algebraic computations.

(2)Using predicates only(no algebraic computation)makes the reaching of?xpoints possi-ble.As a result,new theorems may be https://www.doczj.com/doc/b17512998.html,ing algebraic methods,one can also discover new geometric facts[?,?],but in a quite di?erent manner.(3)Although algebraic methods can prove a much greater number of theorems,there still exist theorems(Example ??)which can be solved by the synthetic approaches elegantly but have not been solved with the algebraic approaches because to prove them we need excessively large computer memory.

General purpose deductive database systems fail to reach?xpoints for most of our ex-amples within reasonable time because of the large database and the weak strategies for the redundancy control.Some useful general methods of controlling redundancies[?,?,?]and their usage in our case are discussed in Section??.2.

Finally,we should mention that the method in this paper bene?ts from many ideas developed in the algebraic approaches.The idea of using geometric predicates not involving the order relation,such as the full-angle congruent,is initiated by Wu in his algebraic method [?].The concept of non-degenerate conditions and statements of constructive type are also from algebraic methods.

The rest of the paper is organized as follows:The selection of geometric rules is discussed in Section??.The database organization is discussed in Section??.The search strategies are discussed in Section??.Adding auxiliary points is discussed in Section??.Concluding remarks are given in Section??.

2.The Geometric Rules

4S.C.Chou,X.S.Gao,J.Z.Zhang

To select a set of“better”geometric(inference)rules,we need to consider the following issues.

Auxiliary Points.Since most synthetic geometry reasoning systems use Horn clauses as rules,the systems have no ability to generate auxiliary points.Thus it is important that we can prove at least a large portion of the geometry theorems with the chosen geometric rules.The rules about congruent triangles,used by most of the previous work on synthetic automated geometry theorem proving,do not have this property.Most of the commonly used theorems including basic results such as the orthocenter theorem and the centroid theorem can not be proved using these rules without adding auxiliary points.The rules used by us improve a lot in this aspect:most of the160geometry theorems proved by our program without adding auxiliary points can not be proved with the previous programs based on congruent triangles.

Order Relations.The validity of most elementary geometry theorems involving only equalities is independent of the relative order positions of the points involved.Such geom-etry theorems belong to the so-called unordered geometry.This idea originated from Wu’s algebraic method of automated reasoning[?].In unordered geometry,the proofs of these theorems can be very simple.However,the ordinary proofs of these theorems involve the order relation(or inequalities);hence they are not only complicated but also not strict.The method based on congruent triangles is not for unordered geometry.In the work using this method,the order relations needed in the deduction are either derived from a numerical dia-gram or given in the input.As a result,these programs can only be used to prove particular cases of a geometry theorem.On the other hand,the rules used by us are for unordered geometry.

For instance,one proof of the theorem“the two diagonals of a parallelogram bisect each other”in Figure1is based on the congruence of triangles ABO and CDO which is in turn based on the fact that angles OAB and OCD are alternative angles of the parallel lines AB and CD.In this statement,we implicitly assume that points B and D are on di?erent sides of line AC.But this fact is not proved logically in most machine produced proofs.If using a set of rules for unordered geometry,like the one in this paper,a proof of this theorem does not need the fact that points B and D are on di?erent sides of the line AC.

??.1The Geometric Rules.A rule is called a de?nite Horn clause if it has the following form:

Q(x):?P1(x),···,P k(x)meaning

?x[(P1(x)∧···∧P k(x))?Q(x)]

where the x are the points occurring in the geometry predicates P1,···,P k,and Q.Also (P1(x)∧···∧P k(x))and Q(x)are called the body and head of the rule respectively.As in the?eld of deductive bases[?],only de?nite Horn clauses without function symbols are allowed in our program.As a consequence,no algebraic computations are allowed since algebraic computations are actually function symbols and may easily lead to in?nite inference

Deductive Database Approach5 sequences and hence make the reaching of?xpoints impossible.

We use the following predicates:points,coll(collinear),para(parallel),perp(perpendic-ular),midp(midpoint),cyclic,circle,eqangle,cong(congruent of segment),eqratio,simtri (similar triangle),and contri(congruent triangle).

The central concept is eqangle.Here the angle is not the ordinary angle but the full-angle.Intuitively,a full-angle[u,v]is the angle from line u to line v.Note that u and v are not rays as in the de?nition for the ordinary angles.Two full-angles[l,m]and[u,v] are equal if there exists a rotation K such that K(l) u and K(m) v.If A,B and C,D are distinct points on l and m respectively,then[l,m]is also denoted by[AB,CD], [BA,CD],[AB,DC],and[BA,DC].

The introduction of full-angles greatly simpli?es the predicate of the angle congruence. For instance,we have the following rule about parallel lines and angles.

R1.AB CD if and only if[AB,P Q]=[CD,P Q](Figure2).

If using ordinary angles,we need to specify the relations among eight angles and we need to use order relations(inequalities)to distinguish the cases.For instance,we have:“if points B,D are on the same side of line P Q and point P,C are on the di?erent sides of line AB (the order relations),then AB CD?P EB=P F D.”This rule is very di?cult to use and may lead to branchings during the deduction.The following two rules also show why full-angle is crucial to our approach.

R2.[P A,P B]=[QA,QB]:-cyclic(A,B,P,Q)(Figure3).

R3.cyclic(A,B,P,Q):-[P A,P B]=[QA,QB],?coll(P,Q,A,B)(Figure3).

In rule R2,if using the ordinary angle,we need two conditions(Figure3):AP B= AQB or AP B+AQ1B=180?and to distinguish these two cases,we need to know “points P and Q are on the same or di?erent sides of line AB.”This kind of order relations is di?cult to deal with,because for di?erent diagrams of the same theorem,the answer could be di?https://www.doczj.com/doc/b17512998.html,ing full-angles,the two cases can be treated uniformly.Also note that the use of full-angles here is quite di?erent from our previous full-angle method in[?]which uses algebraic computation and backward chaining as the main deduction tools,while here only the concept of angle congruence is used.

The program uses about seventy rules(see the appendix).Some of the rules describe basic properties of the geometry predicates,such as AB CD:-AB P Q,CD P Q.Some of the important rules are listed below.

R4para(E,F,B,C):-midp(E,A,B),midp(F,A,C).

R5midp(F,A,C):-midp(E,A,B),para(E,F,B,C),coll(F,A,C).

R6[OA,AB]=[AB,OB]:-cong(O,A,O,B).

6S.C.Chou,X.S.Gao,J.Z.Zhang

R7cong(O,A,O,B):-[OA,AB]=[AB,OB],?coll(O,A,B).

R8[AX,AB]=[CA,CB]:-circle(O,A,B,C),perp(O,A,A,X).

R9[AB,AC]=[OB,OM]:-circle(O,A,B,C),midp(M,B,C).

R10perp(A,B,P,Q):-cong(A,P,B,P),cong(A,Q,B,Q).

R11perp(P,A,A,Q):-cong(A,P,B,P),cong(A,Q,B,Q),cyclic(A,B,P,Q).

R12simtri(A,B,C,P,Q,R):-[AB,BC]=[P Q,QR],[AC,BC]=[P R,QR],?coll(A,B,C). R13eqratio(A,B,A,C,P,Q,P,R):-simtri(A,B,C,P,Q,R).

R14contri(A,B,C,P,Q,R):-simtri(A,B,C,P,Q,R),cong(A,B,P,Q).

Notice that we also use[AB,CD]=[P Q,UV]and AB=CD to represent full-angle

and segment congruences.Though not axioms in common textbooks,these rules are basic geometric facts that can be proved without di?culty.

In common textbooks and previous synthetic approaches,the three theorems about tri-angle congruence,s.s.s,s.a.s,and a.a.s,are the key deduction rules.In our program,only the

a.a.s(Rule R14)is used.The s.a.s rule is not correct if full-angle is used.For instance,tri-angles AOB and AOD in Figure1satisfy BO=DO,AO=AO,[BO,OA]=[DO,OA],

but they are not congruent.The s.s.s rule is correct but cannot generate new properties about full-angles in the general case.

The rules are highly complicated from the viewpoint of a deductive database:all the predicates are mutually recursive and most of the rules are not linear[?].We should mention

that the rules are not complete in the sense that a valid geometry theorem described using

our predicates may not be proved using our rules.

??.2Non-degenerate Conditions.In some rules such as Rule R3,there are negations

in their bodies.Strictly speaking,these rules are not Horn clauses.We solve this problem using the negation by failure criteria proposed in[?];i.e.,we assume?P to be valid if P can

not be deduced by the program.This may lead to inconsistency,since the rules used by us

are not complete and hence failure to prove P does not mean that?P is valid.We solve this problem in two steps.

First,whenever used,a negative condition will be added to the hypotheses of the state-

ment and called the non-degenerate(ndg)condition of the geometry statement.Adding

the ndg conditions to the geometry statement is acceptable for the following reasons.The original description for most of the geometry theorems in textbooks implicitly assumes some necessary conditions,which are part of the ndg conditions found by our method.For some theorems proved by previous synthetic provers,the necessary ndg conditions are missing.

More about ndg conditions can be found in[?,?,?].

Second,suppose that we have an exact numerical diagram for the statement.When encountering a negative predicate?P in a rule,the prover checks if P is true in the diagram.

This rule can be used only if P is false in the numerical diagram.As a consequence,we avoid the possible proof of“trivially true”statements;i.e.,statements whose hypotheses are inconsistent.

Deductive Database Approach7 ??.3Constructing Exact Numerical Models.The use of exact numerical diagrams as semantic models has been the cornerstone of most of the previous e?orts of synthetic mechanical geometry theorem proving[?,?,?].There are two bene?ts the early provers derive from a numerical diagram:(1)The diagram is used as a?lter to reject goals occurring during a backward chaining which are not consistent with its numerical representation.(2) More importantly,the numerical diagram is used to determine order relations among points and lines.The?rst bene?t is very important to the backward search and is not useful in the forward chaining.The second bene?t is related to the problem of producing diagram independent proofs[?].In this paper,the diagrams are used to treat negative information in the Horn clauses.

In the previous work,the diagram is prepared by the user.In our program,the diagram is generated automatically for a class of linear constructive geometry statements.A geometry statement is said to be linear constructive if the points in the statement can be listed in a sequence such that each point in the sequence can be uniquely constructed from the previous points in the sequence.More precisely,a geometry statement is linear constructive if the points in it can be described by the following constructions:

?Take a free point.

?Take an arbitrary point on a line.

?Take the intersection of two lines.

?Take the intersection of a line and a circle or two circles when the other intersection point of them is already constructed.

For instance,the statement in Figure1is a linear constructive statement.Its points can be introduced as follows:take three free points A,B,and C;take the intersection D of the line passing through point A and parallel to BC and the line passing through point C and parallel to AB;take the intersection O of lines AC and BD.More details can be found in[?].Most of the commonly used geometry statements are linear constructive ones.For example,eighty percent of the512geometry theorems in[?]are in this class.

For a linear constructive geometry statement,the coordinates of each point can be rep-resented as rational expressions in the coordinates of the previous points.Thus by assigning random numbers to the coordinates of the free points in the statement,we can easily com-pute the coordinates of all the points as rational numbers and hence an exact numerical model for the statement.

If a geometry statement is not linear,then to construct its diagram we generally need algebraic numbers to represent the coordinates.Also,if the statement is reducible(see[?] for the de?nition)more than one diagram is needed for the statement.Our program cannot construct an exact numerical model for such statements.

3.Structured Database

??.1Structure of the Database.In the traditional way of representing a relational data-base,each n-ary predicate is associated with an n-dimensional array.Since most geometric predicates used by us satisfy some special properties,building database according to the

8S.C.Chou,X.S.Gao,J.Z.Zhang

traditional way will lead to very large databases.The main aim of this section is to design a structured database whose size can be e?ectively controlled.The main idea is to represent the properties involving a predicate alone using the structure of the database.In other words,we build some rules about predicates into the structure of the database.The following are three such principles:

(1)Use canonical form for predicates .One geometric property can be represented as many predicate forms.For instance,the predicate coll satis?es the following rules:

coll(A,B,C ):-coll(A,C,B ),

coll(A,B,C ):-coll(B,A,C ).

Thus from coll(A,B,C ),we can obtain ?ve “new”facts:coll(A,C,B ),coll(B,A,C ),coll(B,C,A ),coll(C,A,B ),coll(C,B,A ).In order to save space and enhance search speed,we represent predicates as canonical forms by assigning an order to the points in a geometry statement.With such an order,predicates can be represented uniquely.Furthermore,by using the canonical form the above rules are not needed explicitly in the deduction steps.This will reduce the number of rules used in the deduction process.

(2)Use equivalent classes to represent some predicates .We may use sequences to represent certain transitive geometric predicates.For instance,the fact that points A 1,A 2,···,A n are on the same line can be represented by a sequence of points.In predicate form,we need n (n ?1)(n ?2)di?erent forms like coll(A i ,A j ,A k )to represent this fact.

(3)Use representative elements for equivalent classes .Some predicates are essentially geometric relations about equivalent classes.In that case,we will use a representative element to represent the equivalent class.For instance,the fact that the line containing points A 1,...,A n is parallel to the line containing points B 1,...,B k can be represented by l 1 l 2if using l 1and l 2to represent the two lines.If using predicates para(A i ,A j ,B k ,B l )to represent this fact,we need 2n (n ?1)k (k ?1)predicates.

We will now give the structure of the database.At the top level,the facts satisfying each predicate are represented by a list of structures which will be de?ned below.

coll.The structure is a list of points on the same line.Let n be the number of points on

the line.We need n (n ?1)(n ?2)predicate forms to represent this fact.

para.The structure is a pair of line pointers l 1and l 2meaning that l 1 l 2.Let l 1and l 2

contain n 1and n 2points respectively.Then we need 2n 1(n 1?1)n 2(n 2?1)predicate

forms.

perp.The structure is a pair of line pointers l 1and l 2meaning that l 1⊥l 2.Let l 1and l 2

contain n 1and n 2points respectively.Then we need 2n 1(n 1?1)n 2(n 2?1)predicate

forms.

eqangle.The structure is a four tuple of line pointers [l 1,l 2,l 3,l 4]meaning that [l 1,l 2]=[l 3,l 4].Let l i contain n i points.Then we need 8 4i =1

n i (n i ?1)predicate forms.cong.The structure is a list of pairs of points.If the list contains n pairs of points then we

need 4n (n ?1)predicate forms.

eqratio.The structure is a four tuple of cong pointers [c 1,c 2,c 3,c 4]meaning that c 1/c 2=c 3/c 4.Let c i contain n i points.Then we need 16 4i =1n i (n i ?1)predicate forms.

Deductive Database Approach9 midp.The structure is a three tuple of points[M,A,B]meaning that M is the midpoint of AB.We need two predicate forms to represent this fact.

circle.The structure is a list of points[O,P1,···,P n]meaning that points P1,···,P n are on a circle with center O.We need n(n?1)(n?2)(n?3)predicate(cyclic)forms.

simtri(contri).The structure is a list of three-tuple of points.If the list contains n tuples then we need6n(n?1)predicate forms.

De?nition3.1An element in the database described above is called a data or a fact of the corresponding predicate.If d is a fact of predicate P then we also call P the predicate of d. Facts in the traditional sense such as coll(A,B,C)and para(A,B,C,D)for concrete points A,B,C,and D are called simple facts.

We also need to know how to trace the deduction route to give a proof for a given fact in the database.For this reason,when updating a fact in the database we?rst copy the old fact to a new position and update the new one,leaving the old fact intact.For each fact,we also need to save the information such as which lemma and what conditions are used to get this fact.The real structure of a fact in the structured database is as follows:

[TYPE,LEMMA,COND,DATA,LINK]

where TYPE tells whether this fact is an“old”one in the sense that it has been updated; LEMMA contains the rules or axioms used to obtain this fact;COND contains the facts used to obtain this fact;DATA is the fact in structured form;LINK points to the next data in the database.

The above structure is not optimized for size control.We could further reduce the size of the database by introducing more complicated structures.But the more complicated the database structure the more complicated the program needed to handle it.Here we need to consider a tradeo?between the size of the database and the di?culty of implementation. From the following facts,we know that the above structure already reduces the database size signi?cantly.

For the160geometry con?gurations solved by our prover,the average size of the data-bases is221if the above structure is https://www.doczj.com/doc/b17512998.html,ing the predicate form,the average size would be242,117;i.e.one hundred times larger.For many con?gurations such as Example??,we can not reach the?xpoint within reasonable time if the above structure is not used. ??.2Generating Proofs.After a?xpoint is reached,we can generate a proof for each fact in the database.This task is not trivial mainly because we use a database with complicated structures.A straightforward print of the deduction steps is not easy to understand.

We have mentioned in Section??.1that for each fact in the database,we save the name of the lemma and the conditions used to derive this fact.So a proof step has the following form

(R):C:?P1,···,P k

where C is a simple fact(see De?nition??)and the P i are either facts or simple facts.C is always a simple fact for the following reasons:at?rst step,C is the geometry statement the user want to prove,and at the following steps this is ensured by our tracing procedure described below.

10S.C.Chou,X.S.Gao,J.Z.Zhang

To print the deduction R above,we?rst print the simple fact C.For each P i,if P i is a simple fact then we print it and?nd the?rst fact(there might be more than one fact)in the database which implies P i;if P i is not a simple fact then we need to?nd a simple fact which can be deduced from P i and is relevant to deduction R(see(2)below).After printing deduction R,we repeat the process for each P i until P i is in the hypotheses of the geometry statement.

The following three strategies are used in the above tracing process.

(1)Finding missing conditions.Because of the structured database,some conditions are implicitly assumed and hence missed in the database.In the tracing process,we need to bring them back to make the proofs easy to understand.The most often missed condition is collinear.For instance,in the following deduction in Example??

perp[AB,CG]:-perp[BC,AF],[BC,AF]=[AB,CH].

a condition coll[GCH]is missed.This condition will be added to the proof in this step.

(2)Finding proper conditions.If a predicate is represented by a sequence,then its facts can be very large.In the tracing process,we need to?nd the proper simple facts from them. For instance,the following deduction

AB=P Q:-AB=CD,CD=EF=XY=P Q

can be simpli?ed to

AB=P Q:-AB=CD,P Q=CD.

(3)Avoiding redundancies.Before printing a fact P i in a deduction,we?rst check whether it has been printed before.If so,we only need to point to the fact printed before. In the machine proof for Example??,Step4is used by Steps2and7.

4.Search and Control Strategies

??.1Data-Based Search.Since we want to reach the?xpoint,breadth-?rst forward chain-ing is the natural choice for us.The geometric rules are highly complicated:all the predicates are mutually recursive and most of the rules are not linear.This makes it impossible to use some of the more specialized search strategies in[?]which are designed for certain special situations.

Basically speaking,the breadth-?rst forward chaining search works as follows: D0R?D1R?...R?D k(Fixpoint)

where D0is the hypotheses of the geometry statement and R is the rule set.For each rule r in R,apply it to D0to obtain new facts.Let D1be the union of D0and the set of new facts obtained.Repeat the above process for D1to obtain D2,etc.If at certain step D k=D k+1, then we say that a?xpoint for D0and R is reached.In the case of a deductive database[?] (i.e.,when we assume that the rules are Horn clauses without function symbols)the?xpoint can always be reached if the rule set R(i.e.,the intensional database)and the initial fact set D0(i.e.,the extensional database)are?nite.

Since D1contains D0as a subset,the derivation of D2from D1clearly repeats all the previous deductions used to derive D1from D0.The semi-naive evaluation is proposed to solve this problem[?].The basic idea is that the input fact for at least one of the predicates in the body of the rule must be a new one;i.e.,a fact in D1?D0.Note that in the semi-naive and all the forward chaining searches,the main loop of process is to search the rule set R.

Deductive Database Approach11 We call such search strategies rule-based search strategies.In what follows,we present a data-based search strategy,in which we keep a new-fact-list and for each fact d in the list we ?nd and apply all the rules whose bodies contain the predicate of d.

The Data-Based Search Algorithm.

Step1.Set the hypotheses of the statement to be initial new-fact-list and the initial database. While the new-fact-list is not empty do Step2.

Step2.Let d be the?rst new fact in the list.Delete it from the list,add it to the database, and do Step3.

Step3.Let r be a rule whose body contains a predicate P0of the fact d.To apply the rule r,we need to instantiate other predicates in r.Since predicate P0will be instantiated as the new fact d,other predicates in r need to be instantiated for all the facts in the database. For all the predicate forms of fact d(notice that a fact could have many predicate forms) and for all the facts of the other predicates in r,do step4.

Step4.Apply rule r to obtain a fact d .If d is in the database,do nothing.Otherwise,add it to the end of the new-fact-list.

Since the hypothesis set of a geometry statement is?nite and we use a?nite rule set without function symbols,a?xpoint will always be reached.It is clear that the?xpoint is unique and does not depend on the search strategies and the order of the applications of the rules.

Generally speaking,the breadth-?rst search is extremely expensive.However,our imple-mentation of it for geometry reasoning performs quite well.This is due to several factors.We use the structured database to reduce the size of the database drastically and to reduce the number of rules which are built into the structure of the database.Also,our implementation using the C language is specially targeted toward the geometry case.

An interesting fact about the data-based search is that the order of application of the rules is determined by the order of the facts in the new-fact-list:rules are selected according to the type of the fact on the top of the new-fact-list.The user may assign an order of importance to the predicates.Those predicates used more frequently,such as middle points, parallel,and perpendicular,will have higher orders.During the search,the program will sort the new fact list according to this order so that the fact with the highest order will be the?rst data of the list.In this way,the order of application of rules can be determined automatically.

Another related improvement of the data-based search is to form combined rules.Let d be the new fact on the top of the new-fact-list.There are rules like

P∧f1?Q1,···,P∧f s?Q s

where P is the predicate of fact d and f i are conjunctions of other predicates.Then we can form a new combined rule

P∧(f1?Q1,∨···∨,f s?Q s).

In the new rule we need only search fact d once.Since a fact in our database could be very large(e.g.,it might be a sequence of similar triangles)the new rule will clearly save time. We can go further to combine the rules f1?Q1,···,f s?Q s recursively to obtain multiple

12S.C.Chou,X.S.Gao,J.Z.Zhang

combined rules.For instance,the following multiple combined rule is formed from rules R6, R10,and R11

cong(O,A,O,B)∧[?[OA,AB]=[AB,OB],

cong(U,A,U,B)∧[?perp(A,B,O,U),

cyclic(A,B,O,U)?perp(O,A,A,U)]].

To further improve the search e?ciency,we can update and use the database dynamically. In the traditional approaches,the facts are clearly divided into levels and to obtain a fact at k-level,only the facts at(k-1)-level will be used.A better way seems to be that new facts will be stored into the database and used immediately.This makes the program using a combination of the breadth-?rst search and the depth?rst search.

??.2Avoiding Redundant Deductions.A deduction is redundant if it generates a fact that is already in the database.The redundant deduction is a major hurdle for speeding up the search and eliminating redundancies is proposed as a basic research problem by L. Wos[?].It is proved that in general cases,the problem of eliminating all redundancies is undecidable[?].So the best we can do is to design strategies reducing the redundancies.

There are three kinds of redundant deductions.First,repeated use of the same rule to the same fact will generate the same result.These kind of redundancies can be solved by the semi-naive search or our data-based search.

Second,some redundant deductions are logically guaranteed.For example,if a rule r in a rule set R is a logical consequence of R?{r}then each fact deduced using rule r will also be deduced by other rules in R.For a given rule set,the problem of obtaining a minimal and logically equivalent rule set is undecidable[?].Many useful partial methods are given in[?,?,?].Since the rule set used by us is?xed,we try to remove the redundant rules based on our geometric intuition.The diagram based standard rules explained below can be considered special cases of these methods.

Third,two logically irrelevant deductions may give the same fact if the input facts satisfy certain conditions.We call these kind of redundancies the conditional redundancies.There seems no general method to control conditional redundancies.In our program,the heuristic (1)explained below is designed for this purpose.

The following heuristics are used to control redundant deductions in our program: (1)Checking Results Before Searching.During the execution of a rule:

Q:?P1,···,P s,

if all the variables in Q are instantiated and predicates P1,···,P k,(k

(2)Avoiding Tautologies.If the composition of rules is an identity then the successive deductions by these rules will give the same fact as the input.A special but often encountered

Deductive Database Approach13 case is the composition of a rule and its reversed rule such as rules R2and R3.For each deduced fact in our database,the program always remembers the lemma used to deduce it (Section??).Thus it is easy to detect and delete these kind of redundancies.

(3)Avoiding Empty Fact.We call a fact empty if no new information can be derived from it.An example of empty fact is contri(O,A,B,O,B,A)if OA=OB,because all the information we can get from this fact is already known.We could have many such congruent triangles if there are circles in the geometry statement.For instance,in a circle

with center O and passing through points P1,...,P n,there exist n(n?1)

2empty facts of the

form contri(O,P i,P j,O,P j,P i).In our program,we do not store empty facts in the database

to reduce the database size and to reduce redundancies in later steps.

(4)Diagram Based Standard Forms.Many rules generating redundancies are related

to a diagram.In this case,we can eliminate some rules to avoid redundancies.We use the following example to illustrate how to do this.

In Figure4,we have?ve properties:midp(M,A,B),perp(O,M,A,B),cong(O,A,O,B), eqangle(A,O,M,M,O,B),and eqangle(O,A,B,A,B,O).By rules R6and R7,cong(O,A,O,B) and eqangle(O,A,B,A,B,O)are equivalent,so we need only consider one of them.The in-teresting fact about this?gure is that any two of the four statements implies the rest three. We thus could have twelve rules.These rules clearly lead to many redundant deductions.

To avoid this,we choose a set of standard rules,say

S1.cong(O,A,O,B):-midp(M,A,B),perp(O,M,A,B).

S2.eqangle(A,O,M,M,O,B):-midp(M,A,B),perp(O,M,A,B).

For the ten rules left,we only keep those whose head is either midp(M,A,B)or perp(O,M,A,B). As a result,only six rules are left.

5.Constructing Auxiliary Points and Skolemization

In logic,constructing new points corresponds to the Skolemization of the existential quanti?ers.Even before the?rst geometry theorem prover was developed,A.Robinson suggested that the auxiliary points and lines needed in a proof can be constructed as elements

of the Herbrand universe for the problem[?].Based on similar ideas,Reiter presented a deductive method that can generate new points[?].But both of the above ideas are not implemented.It is clear that constructing auxiliary points may lead to in?nite geometric objects and prevent the reaching of?xpoints.Also,introducing new points may drastically increase the size of the database.We use two strategies to control the adding of new points

to achieve e?ectiveness.

Our?rst strategy is to separate the process of adding new points from the process of reaching the?xpoints.The program works precisely as follows.For a geometry theorem, we?rst?nd a?xpoint for the corresponding con?guration of the theorem without adding auxiliary points.If the conclusion of the statement is already in the database then the program terminates.Otherwise,the program will try to construct an auxiliary point,add

14S.C.Chou,X.S.Gao,J.Z.Zhang

the facts related to the auxiliary point to the new-fact-list,and?nd a new?xpoint.The program will repeat the above process until either the conclusion is in the new database or there exist no new auxiliary points.

If the above strategy is not used then we may encounter the unpleasant situation that the conclusion of the statement can be deduced without adding auxiliary points,but in the process of?nding the?rst?xpoint,many auxiliary points will still be constructed. Construction of many irrelevant points may dramatically drag down the searching speed.

Our second strategy is to use two heuristics to control the constructing of too many auxiliary points.(1)After an auxiliary point is added and a new?xpoint is reached,we will check whether new properties about the original diagram are found.If they are,we will keep this auxiliary point;otherwise,the auxiliary point will be deleted.(2)No recursive auxiliary points are allowed;i.e.,to construct an auxiliary point,we can only use points occurring in the original statement.The second condition guarantees that the program will terminate.

A rule of constructing auxiliary points is actually the modi?cation of a rule given in Sec-tion??in which a universal quanti?er is changed to an existential quanti?er.The following are four rules of constructing auxiliary points.Rules A1and A2are related to Rules S1and R3.

A1:[perp(O,M,M,A)and[XO,MO]=[MO,AO]]?

?B[coll(B,A,M)and coll(B,O,X)and cong(O,B,O,A)and midp(M,A,B)].

A2:[[AP,BP]=[AX,BY]and?coll(A,B,P)]?

?Q[[AP,BP]=[AQ,BQ]and cyclic[A,B,P,Q].]

A3:[midp(M,A,B)and midp(N,C,D)]?

?P[midp(P,A,D),para(P,M,B,D),and para[P,N,A,C].]

A4:[cong(O,C,O,D)and perp(A,B,B,O)]?

?P[cong(O,C,O,P),para(P,C,A,B),cong[B,C,B,P].]

The negative statement used in rule A2is treated similarly to the negative information in Section??.3.In rules A1and A2,the new point is introduced as the intersection of two non-parallel lines.In rule A3,the new point is introduced as the midpoint of a line segment. In rule A4,the new point is introduced as the intersection of a line and a circle.

Totally,we have about twenty rules of constructing auxiliary points.The most often used experimental“methods”of adding auxiliary points are selected as rules.These rules are not complete.Of the160geometry con?gurations solved by our program,39of them need the construction of auxiliary points.Two of them are Examples??and??.

In[?,?],two constructions are considered:construction of new points and construction of new lines between two existing points.In our program,lines connecting all possible pairs of points will be stored into the database if more than two points are on them or they are used in one of the following predicates:para,perp,and eqangle.In other words,lines connecting any pair of points in the diagram are considered to exist in our program and do not need to be added.

6.Conclusion

??.1Implementation.The method reported in this paper is actually one of the proving methods implemented in our geometry reasoning system:Geometry Expert,which is available

Deductive Database Approach15 via ftp at https://www.doczj.com/doc/b17512998.html,:pub/geometry/software/gex sparc.tar.Z.First,you need to select the“Deductive Database Method”item in the“Parameter”menu to use the?xpoint approach.The default proving method of the program is the area method[?].For a given geometry statement,the program works as follows:

??.2Applications.The current program has the following applications.

(1)Automated Theorem Proving and Discovering.It is clear that the program can be used to prove a given geometry theorem.A more interesting application is to discover“new”facts about the geometric con?guration.Anything obtained in the forward chaining may be looked at as a“new”result.Our experiments show that our program can discover most of the well-known results and often some unexpected ones.Take the simple con?guration(Figure 6)related to the orthocenter theorem as an example.Our program discovered the most often mentioned properties about this con?guration:(1)the three altitudes are concurrent and

(2)[EG,CG]=[CG,F G].The program also?nds105essentially di?erent ratios in such

a simple con?guration!In Example??,the program even discovered some new results.

(2)Served as the Basis for Other Reasoning Methods.We plan to develop a geometry reasoning system having the merits of both the synthetic and algebraic approaches.For a geometry theorem,the system?rst forms a database using the synthetic approach.If the conclusion is in the database,then a synthetic proof for it can be produced.Otherwise,the system proves the theorem using the decision procedures such as the area method[?],and the database may help these decision methods to produce more elegant proofs.

(3)Geometry Education.Starting from the hypotheses of a geometry statement reasoning forward to prove the conclusion is one of the basic proving techniques in geometry.Our

16S.C.Chou,X.S.Gao,J.Z.Zhang

program mechanizes this approach and gives it more power.By adding a nice interface, the program can teach a student how to prove a speci?c theorem with the forward chaining or to show the student how to explore interesting properties of a given con?guration.For another application,since the current program can generate almost all the properties for a con?guration within seconds,a geometry teacher can use it to select exercises for the students or examples for a geometry textbook.

??.3Experiment Results and Examples.The160geometry con?gurations are mainly from[?,?].All the theorems in[?]and the non-trivial theorems in[?,?]are also included. There are about600theorems in[?,?]which are solved with Wu’s method or the area method.We can?nd?xpoints for each of the600theorems,but only about160of them can be proved in this way.Some well-known theorems such as Pappus’theorem and Pascal’s theorem are beyond the scope of our program,although the?xpoints can be reached for both of them.For Pappus’theorem,the?xpoint is the set of original hypotheses.For Pascal’s theorem,the?xpoint contains89facts.Therefore,although it might be the most powerful synthetic approach,our deductive database approach is still much less powerful in scope than the algebraic approaches.On the other hand,our approach has the following advantages: (1)it can be used to discover theorems automatically;(2)the proofs produced are more intelligible;(3)for some theorems(we have two such examples),the deductive database method can produce elegant proofs while no algebraic method can even prove them because exceedingly large amount of computer memory and computing time are required.While using the geometric rules adopted by us,there do exist short proofs for these theorems.

The following table contains the timing and database size statistics for the160geometry theorems solved by the program.The timing is collected on a NeXT workstation.

Proving Time(seconds)Size of structured DB Size of predicate DB

Time Theorems Size Theorems Size Theorems

≤0.130%≤5016%≤10,00011%

≤169%≤10042%≤50,00043%

≤1094%≤20066%≤100,00059%

≤6098%≤50091%≤1,000,00095%

≤650100%≤4021100%≤5,041,102100%

8.37(average)221(average)242,117(average)

The predicate that has the largest database is eqratio.Without this predicate,the size of the database will reduce signi?cantly.So a heuristic might be:?rst obtain a?xpoint without considering predicate eqratio and if the conclusion is not in the database then obtain a new ?xpoint including eqratio.

Example6.1(The Orthocenter Theorem)Show that the three altitudes of a triangle are concurrent.

Deductive Database Approach17 The hypotheses(extensional database)are:points(A,B,C),coll(E,A,C),perp(B,E,A,C), coll(F,B,C),perp(A,F,B,C)coll(H,A,F),coll(H,B,E),coll(G,A,B),coll(G,C,H).

Reaching the?xpoint costs the program0.75second.The size of the?xpoint is146if the structured database is used.In predicate form,the size of the?xpoint would be56,940. The following is the breakdown of the?xpoint into predicates:coll9(36in predicate form), perp3(216),cyclic6(144),eqangle19(29376),simtri4(288),eqratio105(26880).

The?xpoint contains two of the most often encountered properties of this con?guration: perp(C,G,A,B)(the conclusion)and[GF,GC]=[GC,GE].Another amazing fact is that this simple con?guration contains105nontrivial ratios!We list those ratios involving segment HC below.

HC?BE=EC?BA,HC?EA=BA?HE

HC?HG=F H?HA=HE?HB,

HC?AF=EF?AC=BA?CF,

HC?F B=HB?F E=F H?BA,

HC?F G=CF?HB=F H?AC,

HC?BG=EC?HB=F H?BC,

HC?CG=BC?F C=EC?CA,

HC?AG=HE?AC=HA?CF,

HC?EG=HE?BC=HA?EC.

The following is the proof for the fact perp(C,G,A,B),which is automatically generated by our prover.In the proof(hyp)means that the corresponding fact is from the hypotheses. The Machine Proof

1.perp[CG,AB]:-(hyp)perp[BC,AF],(hyp)coll[GCH],(2)[BC,AF]=[AB,CH].

2.[BC,AF]=[AB,CH]:-(3)[BC,AB]=[AF,CH].

3.[BC,AB]=[AF,CH]:-(4)[BC,AB]=[F E,AC],(5)[AF,CH]=[F E,AC].

4.[BC,AB]=[F E,AC]:-(hyp)coll[CBF],(hyp)coll[CEA],(6)[BF,BA]=[EF,EA].

5.[AF,CH]=[F E,AC]:-(hyp)coll[AHF],(hyp)coll[AEC],(7)[HF,HC]=[EF,EC].

6.[BF,BA]=[EF,EA]:-(8)cyclic[AF BE].

7.[HF,HC]=[EF,EC]:-(9)cyclic[CF EH].

8.cyclic[AF BE]:-(hyp)perp[F B,F A],(hyp)perp[EB,EA].

9.cyclic[CF EH]:-(hyp)perp[F H,F C],(hyp)perp[EH,EC].

Example6.2(The Five Circle Theorem2))As in Figure7,P0P1P2P3P4is a pentagon. Q i=P i?1P i∩P i+1P i+2,M i=circle(Q i?1P i?1P i)∩circle(Q i P i P i+1)(the subscripts are understood to be mod5).Show that points M0,M1,M2,M3,M4are cyclic.

The?xpoint is reached in3.89seconds and contains541(220,680in predicate form)facts. Besides the fact that M0,M1,M2,M3,and M4are cyclic,our program?nds the following new result:the following ten groups of lines

{P i+1M i+1,Q i?1M i?1,Q i+2M i?2},{P i?1M i?2,P i M i+1,Q i?1M i+2},i=0,1,2,3,4

2)This problem was proposed in the news group sci.math by Noam D.Elkies of Harvard University in 1992.The theorem was proved by Gerald A.Edgar of Ohio State University with Maple.However,for the general-purpose geometry theorem provers based on the algebraic methods,the proofs require exceedingly large amount of computer memory which are currently not available on most computer systems.Wen-Ts¨u n Wu was later able to give a simple synthetic proof.Our program can discover his result totally automatically.

18S.C.Chou,X.S.Gao,J.Z.Zhang

are concurrent and the ten intersection points of them are on the circle determined by M0, M1,M2,M3,and M4,i.e.,this circle contains15points.The three dotted lines in Figure7 represent one group of concurrent lines.

Example6.3In the right triangle ABC,A=90?;AH⊥BC;S is the midpoint of AH; KN AB;P L AC;QM BC.Show that six points P,Q,K,L,M,N are on the same circle.(Figure8)

It takes the program461.06seconds to reach the?xpoint which contains1326(5,041,102 in predicate form)facts.Without using the structured database,the?xpoint is too big to be reached within reasonable time.

Example6.4ABCD is a trapezoid such that AB CD.M and N are the midpoints of AC and BD.Let E be the intersection of MN and BC.Show that E is the midpoint of BC.(Figure9)

This example is originally given in[?]and used in[?,?].In[?,?],an auxiliary point K=CN∩AB is added by the user.In[?],it is reported that the same auxiliary point will be added based on Skolemization.But the method does not implemented.Our program solves this problem by adding a di?erent auxiliary point using rule A3:A0is the midpoint of AD.With this auxiliary point,the proof of the conclusion seems easier using rules R4 and R5.

The Machine Proof

1.midp[E,BC]:-(2)para[CD,EN],(hyp)midp[N,BD].

2.para[CD,EN]:-(3)coll[ENMA0],(4)para[CD,MA0].

3.coll[ENMA0]:-(hyp)line[MNE],(5)line[MNA0].

4.para[CD,MA0]:-(hyp)midp[M,AC],(hyp)midp[A0,DA].

5.line[MNA0]:-(6)para[A0M,A0N].

6.para[A0M,A0N]:-(7)para[A0M,AB],(8)para[A0N,AB].

7.para[A0M,AB]:-(4)para[CD,MA0],(hyp)para[AB,CD].

8.para[A0N,AB]:-(hyp)midp[N,BD],(hyp)midp[A0,DA].

Example6.5(The Butter?y Theorem)P,Q,R,and S are on the same circle with center O.A is the intersection of P Q and SR.The line passing through A and perpendicular to OA meets P R and QS in N and M respectively.Show that A is the midpoint of NM. (Figure10)

The conclusion is not in the?rst?xpoint.The program automatically adds an auxiliary point A0(using rule A4)which is the intersection of the line passing through S and parallel to AN and the circle O.With the point A0,it takes the program0.4second to reach the?xpoint which contains the conclusion.The key steps in the proof are:(1)NAA0=

Deductive Database Approach19 SA0A,SA0A=ASA0=RSA0,and RSA0=RP A0imply NAA0=NP A0.

(2)NAA0=NP A0implies cyclic(A,N,P,A0).(3)cyclic(A,N,P,A0)implies AA0N= AP N=QP R=QSR=MSA.(4)MSA=AA0N,MAS=NAA0,and AS=AA0imply AMS～= ANA0.(5) AMS～= ANA0implies AM=AN.(6) AM=AN implies midp(A,M,N).Note that this step uses the technique mentioned in Section2.2.We need to check whether M=N numerically.Since this is not true,we can deduce midp(A,M,N)from AM=AN.

Acknowledgment.We would like to thank Prof.D.Kapur for providing many valuable suggestions on this paper.

References

[1] F.Bancilhon&R.Ramakrishnan,An Amateur’s Introduction to Recursive Query Processing

Strategies,Proc.of ACM SIGMOD Conference,edited by C.Zanioilo.,p.16-52,1986.

[2]W.Buntine,Generalized Subsumption and Its Application to Induction and Redundancy,Arti-

?cial Intelligence,Vol.36,No.2,Sept.1988,p.149-179.

[3]S.C.Chou,Mechanical Geometry Theorem Proving,D.Reidel Publishing Company,Dordrecht,

Netherlands,1988.

[4]S.C.Chou&X.S.Gao,Mechanical Formula Derivation in Elementary Geometries,Proc.ISSAC-

90,ACM,New York,1990,pp.265–270.

[5]S.C.Chou,X.S.Gao,&J.Z.Zhang,Machine Proofs in Geometry,World Scienti?c,1994.

[6]S.C.Chou,X.S.Gao,&J.Z.Zhang,Automated Generation of Readable Proofs with Geometric

Invariants,I.Multiple and Shortest Proof Generation.(accepted by J.of Automated Reasoning) [7]S.C.Chou,X.S.Gao,&J.Z.Zhang,Automated Generation of Readable Proofs with Geomet-

ric Invariants,II.Proving Theorems with Full-Angles,WSUCS-94-3,CS Dept,Wichita State University,March1994.(accepted by J.of Automated Reasoning)

[8]H.Coelho&L.M.Pereira,Automated Reasoning in Geometry Theorem Proving with Prolog,

J.of Automated Reasoning,vol.2,p.329-390,1986.

[9]M.Bulmer&D.Fearnley-Sander,The Kinds of Truth of Geometry Theorems,(submitted to J.

of Automated Reasoning).

[10]H.Gallaire,J.Minker,&J.M.Nicola,Logic and Databases:A Deductive Approach,ACM

Computing Surveys,vol.16,No.2,p.153-185,1984.

[11]H.Gerlentner,J.R.Hanson,and D.W.Loveland,Empirical Explorations of the Geometry-

theorem Proving Machine,Proc.West.Joint Computer Conf.,143-147,1960.

[12]T.Havel,The Use of Distance as Coordinates in Computer-Aided Proofs of Theorems in Euclid-

ean Geometry,IMA Preprint,No.389,University of Minnesota,1988.

[13]R.Helm,On the Elimination of Redundant Derivations During Execution,Proc.of1990North

American Conference on Logic Programming,p.551-568,The MIT Press,1990.

[14] D.Kapur,Geometry Theorem Proving Using Hilbert’s Nullstellensatz,Proc.of SYMSAC’86,

Waterloo,1986,202–208.

[15]K.R.Koedinger&J.R.Anderson,Abstract Planning and Perceptual Chunks:Elements of

Expertise in Geometry,Cognitive Science,14,511-550,(1990).

[16]Li Hong-Bo,Cli?ord Algebra and Area Method(Submitted to J.Automated Reasoning).

[17] A.J.Nevins,Plane Geometry Theorem Proving Using Forward Chaining,Arti?cial Intelligence,

6,1-23,1975.

[18]Recio-Velez,Automatic Discovery of Theorems in Elementary Geometry,(submitted to JAR).

20S.C.Chou,X.S.Gao,J.Z.Zhang

[19]R.Reiter,A Semantically Guided Deductive System for Automatic Theorem Proving,IEEE

Tras.on Computers,vol C-25,No.4,p.328-334,1976.

[20]R.Reiter,On the Closed World Data Bases,in Logic and Data Bases,H.Gallaire and J.Minker

(eds),p.55-76,Plenum Press,New York,1978.

[21] A.Robinson,Proving a Theorem(as done by Man,Logician,or Machine),in Automation of

Reasoning,ed.by J.Siekmann and G.Wrightson,p.74-78,1983,Springer-Verlag.

[22]Y.Sagiv,Optimizing Datalog Programs,in Foundations of Deductive Databases and Logic Pro-

gramming,Ed.J.Minker,p.659-698,Morgan Kau?mann,1988.

[23] D.M.Wang,Reasoning About Geometric Problems Using an Elimination Method,in Automated

Practical Reasoning,eds.J.Pfalzgraf and D.M.Wang,pp.148-185,Springer-Verlag,1995.

[24]N.L.White&T.Mcmillan,Cayley Factorization,Proc.of ISSAC’88,p.4-8,1988,ACM Press.

[25]L.Wos,Automated Reasoning:33Basic Research Problems,Prentice-Hall,Englewood Cli?s,

New Jersey,1988.

[26]Wu Wen-ts¨u n,Basic Principles of Mechanical Theorem Proving in Geometries,Volume I:Part

of Elementary Geometries,Science Press,Beijing(in Chinese),1984.English version,Springer-Verlag,1993.

《数据库原理及应用》模拟试卷答案

《数据库原理及应用》模拟试卷答案 1.填空题（每格1分，总分20分） （1）数据库的保护功能主要包括确保数据的安全性、__________________、________________、__________________四方面的内容。 数据的完整性并发控制数据库恢复 （2）事务的性质：原子性、__________、__________、持久性。一致性隔离性（3）在SQL中，CREATE VIEW 语句用于建立视图，如果要求今后对视图用UPDATE语句更新数据时必须满足于查询中的表达式，则应当在CREATE VIEW 语句中使用 ________________________短语。WITH CHECK OPTION （4）视图是一个虚表，它是从____________中导出的表，在数据库中只存放视图的____________，不存放视图的____________。 基本表或视图定义数据 （5）数据库设计应包括两方面的内容：一是___________特性的设计，二是_____________特性的设计。结构行为 （6）关系数据操作语言(DML)的特点是：操作对象与结果均为关系、操作的非过程性强、语言一体化、并且是建立在数学理论基础之上。DML包括数据查询和________两种数据操作语句。数据更新 （7）使用游标的步骤为：定义游标、打开游标、__取出记录____________、关闭游标（释放游标）。 （8）信息的三种世界是指__________________、__________________和数据世界，其中数据世界又称为计算机世界。信息的现实世界信息世界 （9）从关系规范化理论的角度讲，一个只满足1NF的关系可能存在的四方面问题是：数据冗余度大、__________________异常、__________________异常和 __________________异常。插入修改删除 （10）在SQL中，通配符%表示__________________，下划线_表示 __________________。任何长度的字符串一个任意字符 2.单选题（每题2分,总分20分） （1）以下____B___采用了自底向上的设计分析方法 A)需求分析B)概念结构设计 C)逻辑结构设计D)物理结构设计 （2）在视图上不能完成的操作是( D )。 A、在视图上定义新的视图 B、查询操作

将数据库从Access2003升级到Sql Server 2000

将数据库从Access 2003 升级到Sql Server 2000 将数将数据库从Access 2003 升级到Sql Server 2000，原本以为不是很麻烦（开始时以为就改改数据库的连接代码就行了），但在这次的操作中，虽然在操作前也在网上查了一些相关的资料，但还是感觉有些不够。在这里，我就将本次的升级过程中所遇到的问题，怎么去解决写出来，供以后的各位参考一下。 在进行升级时候，一定要先去查阅一些资料，最后你得对整个过程有一个大体的了解，不然到时到了哪步应该作些什么都忘了，也就无处升级了。 一、好了，在升级前，首先要安装Sql Server 2000。至于怎么去安装我就不讲了，网上的资料很多，在这里只是提醒两点： 1）安装的版本：Sql Server 2000一共分为两个版本，专业版和家庭版，在安装的时候一定要注意到你的操作系统。因为很多人在进行网页制做和调试的时候一般情况下都用的是windows xp 系统，所在这里就不能安装专业版，专业版都是针对于服务器的操作系统，比如说：winNT，win 2000，win2003等。windows xp去安装专业版是不能安装服务端的，所以在安装Sql Server 2000的时候一定要注意版本的选择。 2）数据的导入：安装完后就是要进行数据的导入了（可以参考另一篇文章《Access数据库升级成Sql Server 2000 开发文档》），也就将Access 2003数据库中原有的数据导入到Sql Server 2000里去。在导入的时候首先要在Sql Server 2000里面新建一个数据库，数据表是存在数据库中的。 一般来说呢，在进行数据导入时候不会有什么问题，但也不例外。如果你的Access数据有密码的话，我建议在进行数据导入前先把密码去掉，我不知道你们能不能，反正我是没成功，如果遇到了问题就去掉，没遇到就算了。如果Access2003数据库中的表太多了的话，在导入后一定要检查一下是不是所有的表都导入到Sql Server 2000里面了……还有，在将Access2003中的数据导入以Sql Server 2000的时候因为有一个数据转换，也就是说要将Access2003的数据格式转换成Sql Server 2000里的数据格式，如果在Access2003数据库中一个表中有一条数据不满足Sql Server 2000里的格式，则这个表里面的所有数据都不导入到Sql Server 2000中。这个时候你不防打开Sql Server 2000（这个时候已经有这个表名存在了，只是表里没有数据而已），找到相应的表，打开设计视图，将其中的ntxt字段改成txt，再试一下，如果还不行话，就证明你Access2003数据库中中表里面的数据就真有的问题了。比例说：时间字段不可能出现9999-12-12这样的数据，导入出错了有相应的提示，会提示你说在…数据库中….表…第几行有问题。但这个时候你要注意了，提示中的第多少行并不是我们直接打开表中的多少行。具体是多少行我也不是很清楚。数据库在进行数据转换的时候打开数据表的排列方式和我们直接打开数据表的排列方式是不一样的。 二、数据导入完了这个时候还要做一件事，就是修改Sql Server 2000数据库中各个表的字段类型。当我们把数据从Access2003中导入到Sql Server 2000中你会发现。在Access2003中字段为自增型（一般都为ID字段）的在Sql Server 2000中没了，也就是说以前在向Access数据库中插入数据中，有一个字段是自增型的，但把表导入到Sql Server 2000后，这个字段的类型是int，不是自增型，你这个时候你要手动添加上去；要把Sql Server 2000中的smalldatetime字段改成datetime；以前在Access2003数据库，字段有默认值的，在导入Sql Server 2000后就没有了，也要手动添加上去。比如，时间字段有默认值[now()]在Sql Server 2000中没了，要添加上去，但不能写成now()函数了，将其改成getdate()；将ntxt 字段类型改成txt类型；在Access2003中，有些字段会有一些说明，比如说InsertTime是指数据的写入时间，但导入到Sql Server 2000就没了，你觉得有必要的话就添加上去，没有必要也可以不添，这对于数据库的操作来说没什么影响的。 三、数据库的修改到上面就完了，下面是代码。开始的时候我以为数据库升级了，只是修改一下连接代

数据库原理试题及答案

全国2001年10月自学考试数据库原理试题及答案2 作者：ryan 点击：时间：2003-10-11 上午 23:05:00 来源： 第一部分选择题 (共30分) 一、单项选择题 (本大题共15小题，每小题2分，共30分) 在每小题列出的四个选项中只有一个是符合题目要求的，请将其代码填在题后的括号内。错选或未选均无分。 1. 单个用户使用的数据视图的描述称为【】 A. 外模式 B. 概念模式 C. 内模式 D. 存储模式 2. 子模式DDL用来描述【】 A. 数据库的总体逻辑结构 B. 数据库的局部逻辑结构 C. 数据库的物理存储结构 D. 数据库的概念结构 3. 在DBS中，DBMS和OS之间的关系是【】 A. 相互调用 B. DBMS调用OS C. OS调用DBMS D. 并发运行 4. 五种基本关系代数运算是【】 A. ∪，-，×，π和σ B. ∪，-，∞，π和σ C. ∪，∩，×，π和σ D. ∪，∩，∞，π和σ 5. 当关系R和S自然联接时，能够把R和S原该舍弃的元组放到结果关系中的操作是【】 A. 左外联接 B. 右外联接 C. 外部并 D. 外联接 6. 下列聚合函数中不忽略空值 (null) 的是【】 A. SUM (列名) B. MAX (列名) C. COUNT ( * )

D. AVG (列名) 7. 设关系模式R (A，B，C)，F是R上成立的FD集，F = {B→C}，则分解ρ = {AB，BC}相对于F 【】 A. 是无损联接，也是保持FD的分解 B. 是无损联接，但不保持FD的分解 C. 不是无损联接，但保持FD的分解 D. 既不是无损联接，也不保持FD 的分解 8. 关系模式R分解成ρ = {R1，…，Rk}，F是R上的一个FD集，那么R中满足F的每一个关系r，与其投影联接表达式mρ(r) 间的关系满足【】 A. rí mρ(r) B. mρ(r) í r C. r = mρ(r) D. r≠mρ(r) 9. 在数据库设计中，将ER图转换成关系数据模型的过程属于【】 A. 需求分析阶段 B. 逻辑设计阶段 C. 概念设计阶段 D. 物理设计阶段 10. SQL中，下列涉及空值的操作，不正确的是【】 A. AGE IS NULL B. AGE IS NOT NULL C. AGE = NULL D. NOT (AGE IS NULL) 11. 如果事务T获得了数据项Q上的排它锁，则T对Q 【】 A. 只能读不能写 B. 只能写不能读 C. 既可读又可写 D. 不能读不能写 12. DBMS中实现事务持久性的子系统是【】 A. 安全性管理子系统 B. 完整性管理子系统 C. 并发控制子系统 D. 恢复管理子系统 13. SQL的全局约束是指基于元组的检查子句和【】 A. 非空值约束 B. 域约束子句 C. 断言

1.1- EBS R12.1.1 升级12.1.3 数据库升级 11.2.0.3

EBS R12.1.1 升级12.1.3 数据库升级 11.2.0.3 安装说明书 编制：长安铃木信息系统课王川 2012-11-21

目录 目录 (2) 1 概述 (5) 1.1升级内容 (5) 1.2准备的补丁 (5) 2 升级应用 (6) 2.1停止应用。 (6) 2.2ADADMIN进入维护模式 (7) 2.3追加补丁 (9) 2.4执行DB节点应用CODE LEVEL (9) 2.5追加应用补丁 (10) 3 升级数据库 (10) 3.1升级数据库准备 (10) 3.2创建NLS/DA TA/9IDATA目录 (13) 3.3安装数据库补丁 (13) 3.4P REPARE U PGRADE (14) 3.5执行DBUA (14) 3.6初始化参数文件和监听文件 (19) 3.6.1 参数文件 (19) 3.6.2 监听文件 (19) 3.6.3 运行脚本 (20) 4 初始化数据库节点 (20) 4.1应用层生成生成新的APPSUTIL (20) 4.2生成数据库上下文文件 (20) 5 ADADMIN重建权限和同义词 (21) 6 分别重启数据库和应用。 (22)

7 校验升级结果。 (22)

文档版本记录 版本编号变更内容变更人日期

EBS R12.1.1 Enterprise5.7 64bit 安装说明书 1概述 1.1 升级内容 1、应用从R12.1.1升级到R12.1.3。 2、数据库升级到11.2.0.3。 1.2 准备的补丁 1、APP升级补丁 p1*******_R12.BIV.B_R12_GENERIC.zip p1*******_R12.TXK.B_R12_GENERIC.zip p1*******_R12.TXK.B_R12_GENERIC.zip p8919489_R12.TXK.B_R12_GENERIC.zip p8919489_R12.TXK.B_R12_zhs.zip p9062910_12.1.0_R12_GENERIC.zip p9151516_R12.ECX.B_R12_GENERIC.zip p9239089_R12.AD.B_R12_LINUX.zip p9239090_R12_LINUX_1of6.zip p9239090_R12_LINUX_2of6.zip p9239090_R12_LINUX_3of6.zip p9239090_R12_LINUX_4of6.zip p9239090_R12_LINUX_5of6.zip p9239090_R12_LINUX_6of6.zip p9239090_R12_zhs.zip p9239095_R12_GENERIC.zip p9583541_R12.TXK.B_R12_GENERIC.zip p9738085_R12.TXK.B_R12_GENERIC.zip p9817770_R12.ATG_PF.B_R12_LINUX.zip p9852070_R12.TXK.B_R12_GENERIC.zip p9868229_R12.BOM.C_R12_GENERIC.zip p9966055_R12.FND.B_R12_GENERIC.zip 2、数据库升级到11.2.0.3的安装包 p1*******_112030_Linux-x86-64_1of7.zip … p1*******_112030_Linux-x86-64_7of7.zip

数据库原理-期末考试试题及答案

数据库原理-期末考试试题及答案 （本大题共15小题，每小题2分，共30分) 在每小题列出的四个备选项中只有一个是符合题目要求的，错选、 多选或未选均无分。 1. 要保证数据库的数据独立性，需要修改的是（） A．三层模式之间的两种映射B．模式与内模式 C．模式与外模式D．三层模式 2. 下列四项中说法不正确的是（） A．数据库减少了数据冗余B．数据库中的数据可以共享 C．数据库避免了一切数据的重复D．数据库具有较高的数据独立性 3. 公司中有多个部门和多名职员，每个职员只能属于一个部门，一个部门可以有多名职员， 从职员到部门的联系类型是（） A．多对多B．一对一 C．多对一D．一对多 4．将E-R模型转换成关系模型，属于数据库的（） A．需求分析B．概念设计 C．逻辑设计D．物理设计 5．五种基本关系代数运算是（） A．∪，—，×，π和σB ．∪，—，，π和σ C．∪，∩，×，π和σD ．∪，∩，，π和σ 6．下列聚合函数中不忽略空值 (NULL) 的是（）。 A．SUM (列名) B．MAX (列名) C．COUNT ( * ) D．AVG (列名) 7. SQL中，下列涉及空值的操作，不正确的是（）。 A. AGE IS NULL B. AGE IS NOT NULL C. AGE = NULL D. NOT (AGE IS NULL) 8. 已知成绩关系如表1所示。 执行SQL语句： SELECT COUNT（DISTINCT学号） FROM成绩 WHERE分数＞60 查询结果中包含的元组数目是（） 表1 成绩关系

A. 1 B. 2 C. 3 D. 4 9． 在视图上不能完成的操作是（ ） A. 更新视图 B. 查询 C. 在视图上定义新的基本表 D. 在视图上定义新视 图 10. 关系数据模型的三个组成部分中，不包括（ ） A. 完整性约束 B. 数据结构 C. 恢复 D. 数据操作 11. 假定学生关系是S （S ＃，SNAME ，SEX ，AGE ），课程关系是C （C ＃，CNAME ，TEACHER ）， 学生选课关系是SC （S ＃，C ＃，GRADE ）。 要查找选修“COMPUTER ”课程的“女”学生姓名，将涉及到关系（ ） A ．S B ．S C ，C C ．S ，SC D ．S ，SC ，C 12. 关系规范化中的删除操作异常是指（ ） A ．不该删除的数据被删除 B ．不该插入的数据被插入 C ．应该删除的数据未被删除 D ．应该插入的数据未被插入 13. 从E-R 模型关系向关系模型转换时，一个m:n 联系转换为关系模式时，该关系模式的码 是（ ） A ．M 端实体的码 B ．N 端实体的码 C ．M 端实体码与N 端实体码组合 D ．重新选取其他属性 14．已知关系R={A ，B ，C ，D ，E ，F}，F={A →C ，BC →DE ，D →E ，CF →B}。则(AB)F + 的闭包 是（ ） A ．ABCDEF B ．ABCDE C ．ABC D ．AB 15．设有关系R （A ，B ，C ）和S （C ，D ）。与SQL 语句select A,B,D from R,S where R.C=S.C 等价的关系代数表达式是（ ） A ．σR.C=S.C (πA,B,D (R×S)) B ．πA,B,D (σR,C= S.C (R×S)) C ．σR.C=S.C ((πA,B (R))×(π D (S))) D ．σR,C=S.C (πD ((πA,B (R))×S)) 二、多项选择题 （本大题共5小题，每小题2分，共10分） 在每小题列出的四个备选项中有多个是符合题目要 求的，多选、少选、错选、不选均无分。

%BD-数据库软件升级及数据库迁移方案

数据库软件升级及数据库迁移方案 根据本次项目需求，此次项目实施除硬件设备安装调试外，还包括对已有管理系统所用Oracle数据库的升级和管理系统数据的迁移工作，实施方案如下： 一、数据库软件升级 1.1操作系统AIX安装 新购P550小机自带AIX5.3操作系统，用启动光盘安装并打好相应补丁； 设置相应环境参数，如：语言环境为简体中文等； 挂载IBM DS4700存储，并设成开机自动加载。 1.2 Oracle 10G安装 在存储上安装10g系列中的稳定版本：10.2.0.1.0； 配置两台小机上所装Oracle的RAC，满足数据库的高可用性，保证一台down机的情况下，另一台能自动接管数据库服务。 二、数据库迁移 2.1迁移前期调研 1、迁移任务的目标 本次项目数据迁移的目的是:将现有综合业务系统的四个子系统数据，从低版本到高版本、跨操作系统的方式进行迁移升级，升级后的目的数据库环境在继承现有数据库所有功能基础上，性能及稳定性需更为完善，从而更好的满足对警务系统各方面性能的支持。 2、新旧环境分析

2.2迁移各类资源准备 1、人员技术准备 甲方：业务系统管理员； 软件开发商：提供系统维护手册，以搭建模拟应用系统测试数据； 乙方：网络工程师、数据库维护工程师。 2、系统环境准备 正式环境：2台P550操作系统及Oracle集群安装正常； 中转环境：服务器1台、高档PC机2台，数据迁移中转及应用系统 模拟部署及测试用。 3、安装和调测相关软件 操作系统：Windows（临时中转环境） 数据库：Oracle8.1.7、Oracle10.2.0.1； 中间件：Websphere5.1； 工具软件：PL/SQL、LoadRun等。 2.3数据迁移方案设计 1、时间安排 模拟环境测试：8月28-8月31 模拟结果观察：9月1日-9月3日 正式数据迁移：9月4日-9月6日 2、迁移方案 经过综合分析众多数据迁移相关资料，结合项目经验，本次数据迁移总体方案如下： A、迁移过程通过8.1.7进行过渡 Oracle验证矩阵中强调8.1.6为Oracle中间过渡产品，升级到10g必须先过渡升级到中间稳定版本，推荐方式是：8.1.n—>8.1.7.4 —>10.2。 B、采用传统的EXP/IMP方式迁移 本次迁移非本机环境升级，涉及到Windows到AIX操作系统的跨

联发科和高通骁龙哪个好_高通和联发科处理器的优缺点对比

联发科和高通骁龙哪个好_高通和联发科处理器的优缺点对比现如今的手机越来越跟电脑一样了，其性能也在近些年与电脑的差距不再那么大了，手机处理器和电脑处理器一样，开始和多核发展，但手机处理器市场却不和电脑处理器市场一样，是高通和联发科的天下，自然对比的话也是它们两个来比拼。 联发科cpu和高通骁龙cpu哪个好联发科CPU和高通CPU相比，总体来看，高通CPU更胜一筹，高通CPU要好一些。他们的区别在于：高通CPU在高端手机产品中，高通都有着不小的优势，这是联发科短期内无法超越的。在低端CPU中，联发科目前的战略就是主打低端市场，中低端产品联发科有着绝对的优势。 高通骁龙系列一贯的优势就是性能，而联发科的优势则是性价比。 具体到你说的这两款CPU，高通骁龙Snapdragon APQ8064 Pro其实就是常说的骁龙600，四个Krait 300核心，很多2013年上半年的旗舰手机用的都是这个U。而MT6592则是最近联发科主推的8核CPU，具备8个A7架构的核心，由于小米的缘故，最近搭配这个U 的千元手机很火。具体到这两者的性能来看，参照安兔兔的纯理论跑分的话，MT6592比骁龙600稍高，但低于骁龙800。但是注意这只是理论跑分，并且现在很多手机也针对安兔兔做了特别的优化，以至于安兔兔的参考价值有所下降。 具体到实际使用中，骁龙600由于其Krait 300核心架构的优势，还是表现得更加好一些。目前能充分利用4个核心的软件尚且不多，更不用说8核了，更应该看重的是单核的性能如何，而在单核性能方面，骁龙600明显占优，所以MT6592到性能我认为还是要低于骁龙600的，8核更多的还是一种噱头，当然从性价比的角度看，还是很不错的，毕竟市场是最好的检验场。而市场需要卖点和噱头，8核心不失为一个好的选择，联发科很聪明。下面就为大家带来高通/联发科CPU优缺点解析，希望能对你的选购有所帮助。 一、入门级CPU大比拼一款CPU好不好，我们是要从多个方面考虑的，并不是说简简单单看一个主频、几个核心数就完了，更重要的是它的综合实力到底有多强，这里面当然也会牵扯到价格问题，性能相似当然是便宜的获胜，这是毋庸置疑的。 可能有人网友喜欢研究智能手机，平常手机处理器的官网。就拿高通官网举例，我们可以

(完整word版)数据库原理试卷带答案

数据库原理试卷A 一、单选题（本题共20个小题，每题1分，共20分。答案唯一，多选或少选均不得分。请将答案按对应的题号写在下面的表格中） 1.下述关于数据库系统的正确叙述是( A )。 A. 数据库系统减少了数据冗余 B. 数据库系统避免了一切冗余 C. 数据库系统中数据的一致性是指数据类型一致 D. 数据库系统比文件系统能管理更多的数据 2. 数据库（DB），数据库系统（DBS）和数据库管理系统（DBMS）之间的关系是( A )。 A. DBS包括DB和DBMS B. DBMS包括DB和DBS C. DB包括DBS和DBMS D. DBS就是DB，也就是DBMS 3. 描述数据库全体数据的全局逻辑结构和特性的是( A )。 A.模式 B. 内模式 C. 外模式 D. 用户模式 4. 要保证数据库的逻辑数据独立性，需要修改的是(A )。 A. 模式与外模式的映射 B. 模式与内模式之间的映射 C. 模式 D. 三层模式 5. 数据库系统的数据独立性体现在( B )。 A.不会因为数据的变化而影响到应用程序 B.不会因为系统数据存储结构与数据逻辑结构的变化而影响应用程序 C.不会因为存储策略的变化而影响存储结构 D.不会因为某些存储结构的变化而影响其他的存储结构 6. 在一个关系中如果有这样一个属性存在，它的值能惟一地标识关系中的每一个元组，称这个属性为( C )。 A. 关键字 B. 数据项 C. 主属性 D. 主属性值 7. 现有如下关系： 患者（患者编号，患者姓名，性别，出生日起，所在单位） 医疗（患者编号，患者姓名，医生编号，医生姓名，诊断日期，诊断结果） 其中，医疗关系中的外码是( D )。 A. 患者编号 B. 患者姓名 C. 患者编号和患者姓名 D. 医生编号和患者编号 8. 自然连接是构成新关系的有效方法。一般情况下，当对关系R和S使用自然连接时，要求R或S含有一个或多 个共有的( D )。 A. 元组 B. 行 C. 纪录 D. 属性 9. 有关系SC（S_ID，C_ID，AGE，SCORE），查找年龄大于22岁的学生的学号和分数，正确的关系代数表达式是( D )。 ⅰ. πS_ID，SCORE (σAGE >22 (SC) ) ⅱ. σAGE >22 (πS_ID，SCORE (SC) ) ⅲ. πS_ID，SCORE (σAGE >22 (πS_ID，SCORE，AGE (SC) ) ) A.ⅰ和ⅱ B. 只有ⅱ正确 C. 只有ⅰ正确 D. ⅰ和ⅲ正确

MySQL升级的3种方法

MySQL数据库的版本更新很快，新的特性也随之不断的更新，更主要的是解决了很多影响我们应用的BUG，为了让我们的MySQL变得更美好，我们有必要去给它升级，尽管你会说它现在已经跑得很好很稳定完全够用了。下面我们来看看几种常用的升级方法。 介绍之前，我们先做一些声明，MySQL采用二进制包来安装，升级都是在同一台DB Server 上操作。 第一种，很简单，适用于任何存储引擎。 1. 下载并安装好新版本的MySQL数据库，并将其端口改为3307（避免和旧版本的3306冲突），启动服务。 2. 在新版本下创建同名数据库。 # mysqldump -p3307 -uroot create mysqlsystems_com 3. 在旧版本下备份该数据库。 # mysqldump -p3306 -uroot mysqlsystems_com > mysqlsystems_com.bk Note: 你也可以加上–opt选项，这样可以使用优化方式将你的数据库导出，减少未知的问题。 4. 将导出的数据库备份导入到新版本的MySQL数据库中。 # mysql -p3307 -uroot mysqlsystems_com < mysqlsystems_com.bk 5. 再将旧版本数据库中的data目录下的mysql数据库全部覆盖到新版本中。 # cp -R /opt/mysql-5.1/data/mysql /opt/mysql-5.4/data Note: 大家也都知道这个默认数据库的重要性。 6. 在新版下执行mysql_upgrade命令，其实这个命令包含一下三个命令： # mysqlcheck –check-upgrade –all-databases –auto-repair # mysql_fix_privilege_tables # mysqlcheck –all-databases –check-upgrade –fix-db-names –fix-table-names Note: 在每一次的升级过程中，mysql_upgrade这个命令我们都应该去执行，它通过 mysqlcheck命令帮我们去检查表是否兼容新版本的数据库同时作出修复，还有个很重要的作用就是使用mysql_fix_privilege_tables命令去升级权限表。 7. 关闭旧版本，将新版的数据库的使用端口改为3306，重新启动新版本MySQL数据库。到此，一个简单环境下的数据库升级就结束了。

数据库原理试卷(有答案)

综合应用题之一 (每小题3分，共30分) 设有如下表所示的三个关系： S（SID，SN，AGE，SEX，DEPT） C（CID，CN，TEACHER） SC(SID，CID，GRADE) 其中：SID为学号，SN为姓名，AGE为年龄，SEX为性别，DEPT为系别，CID为课程号，CN为课程名，TEACHER为任课老师，GRADE为成绩。 1、试用关系代数完成如下查询 （1）查找年龄小于18岁男同学的学号和姓名。 πSID，SN (σAGE<18 ∧SEX = “男”(S)) 1分2分 （2）查找系别为“信息工程”的学生姓名、学号和选修的课程号。 πSID，SN，CID (σDEPT = “信息工程”(S∞SC)) 1分2分 或： πSID，SN，CID (（σDEPT = “信息工程”(S)）∞SC) 1分2分 （3）查找选修了课程名为“C语言程序设计”的学生学号和姓名。 πSID，SN (σCN = “C语言程序设计”(S∞C∞SC)) 1分2分 或： πSID，SN ((σCN = “C语言程序设计”(C))∞S∞SC)) 1分2分

2、写出下列操作的SQL语句 （1）在S表中增加一条学生信息：（AP0000001，张成，19，男，交通工程）。 INSERT (1分) INTO S（SID，SN，AGE，SEX，DEPT）(1分) V ALUES(…AP0000001?，?张成?，19，?男?，?交通工程?)(1分) 或： INSERT (1分) INTO S (1分) V ALUES(…AP0000001?，?张成?，19，?男?，?交通工程?)(1分) （2）查询选修了课程名为“C语言”的学生学号和姓名。 SELECT S.SID，SN (1分) FROM S，C，SC (1分) WHERE S.SID=SC.SID AND SC.CID = C.CID AND https://www.doczj.com/doc/b17512998.html, = “C语言”；(1分) （3）查询每个学生的学号、选修的课程门数和平均成绩。 SELECT SID，COUNT(*) AS 课程门数，A VG（GRADE）AS 平均成绩(1分) FROM SC (1分) GROUP BY SID；(1分) （4）将学号为“AP0000001”同学所选修的“数据库原理”成绩改为88分。 UPDATE SC(2分) SET GRADE= 88 WHERE SID=‘AP0000001’AND CID IN（SELECT CID FROM C WHERE CN=‘数据库原理’）；(1分) （5）把查询SC表的权限授给用户U1。 GRANT SELECT (1分) ON TABLE SC (1分，表前不加TABLE不扣分) TO U1；(1分)

数据库高并发升级方案1

XXXXXXXXXXXX平台数据库升级方案 XXXXXXXXXXXXXXX有限公司2016年11月28日

目录 1. 概述 (4) 1.1. 背景 (4) 1.2. 目标与目的 (4) 1.3. 可行性分析 (4) 1.4. 参考依据 (5) 2. 数据库高并发方案 (5) 2.1. 数据库均衡负载(RAC) (5) 2.2. 数据库主从部署 (8) 2.3. 数据库垂直分割 (9) 2.4. 数据库水平分割 (10) 3. 二代办公平台数据库优化设计 (11) 3.1. 数据库集群 (11) 3.2. 重点业务表分区 (11) 3.3. 任务表历史数据分割 (12) 3.4. 数据库表结构优化 (12) 3.5. 数据访问优化 (12) 4. 实施方案 (13) 5. 工作量及预算评估 (14) 5.1. 工作量及预算评估 (14) 5.2. 其他费用 (15)

1.概述 1.1.背景 随着XXXXXX平台及其他子系统业务量增多，且用户已面向各地州市，用户数量增大，现有的二代办公平台及其他子系统在单一环境下的架构体系和数据库架构体系也无法高效的满足这样的场景。 当前XXXXXX平台及其子系统通过搭建多台WEB服务器和双机热备份的方式进行部署运行。虽已提高了整体效率，但对于部分的业务处理还是未解决。部分业务量并发处理多，业务关联多等因素，导致对数据库并发处理的业务量大，读写量大等也无法用双机热备份进行解决。 因此，在此背景下提高数据库访问效率，增大访问吞吐量等将成为二代办公平台及其子系统运行顺畅的关键因素。 1.2.目标与目的 目标：依托现有系统服务和设备环境，建立可扩容、高并发、高吞吐量的数据库架构体系。 目的：为缓解当前XXXXXX平台机器及其他子系统对数据库访问过大，造成的访问效率低下的问题，提升数据库访问效率和并发效率。对部分业务繁杂的表和访问进行优化设计，缓解因此造成的使用效率低下问题。 1.3.可行性分析 数据库性能分析：根据当前的数据库性能分析，当前硬件设备的提高也无法满足数据库性能的提升，因此应考虑数据库访问控制和数据访问方面进行优化。现有的数据库虽也实现双机热备份，但访问的效率未较大改善，因此应考虑各健全的数据库高并发访问方案。 数据库优化分析：当前的数据库采用的ORACLE数据库，同时，现有的均衡负载、读写分离、数据分割技术较为成熟，在对系统进行适当调整和优化的情况下，能保证系统的正常运行。

数据库原理试题及答案

汕头职业技术学院 2009—2010学年度第二学期期中考试试卷 课程名称数据库原理与应用拟题人审题人_____________ 系（校区）计算机系班级姓名学号____________ 一、单项选择题：（将正确答案的编号填在下表中，每小题1.5分，共18分） 1．任何一个满足2NF但不满足3NF的关系模式都不存在（） A）主属性对主码的部分依赖 B）非主属性对主码的部分依赖 C）主属性对主码的传递依赖 D）非主属性对主码的传递依赖 2．相对于非关系模型，关系数据模型的缺点之一是（） A）查找记录的速度最慢 B）数据结构简单 C）数据独立性高 D）有严格的数学基础 3．创建一个用户数据库时，（）数据库的内容（表和视图）就会自动地复制到新创建的数据库中。 A）master B）model C）msdb D）tempdb 4．下列聚合函数中不忽略空值（null）的是（） A）sum(列名) B）max(列名) C）count(*) D）avg(列名) 5．关于唯一约束的叙述，错误的是（） A）一个表可以定义多个唯一约束 B）唯一约束的值不能重复 C）唯一约束的值不能为null D）一个唯一约束可以施加到多个属性中 6．下列涉及空值的操作，不正确的是（） A）age is null B）age is not null C）age=null D）not(age is null) 7．层次模型不能表示（）的联系 A）多对多 B）一对多 C）多对一 D）一对一 8．下列关系运算中，（）运算不属于专门的关系运算。 A）选择 B）连接 C）投影 D）广义笛卡尔积 9．数据库系统的体系结构是（） A）两级模式结构和一级映射 B）三级模式结构和一级映射 C）三级模式结构和两级映射 C）三级模式结构和三级映射 10．单个用户使用的数据视图的描述称为（）

军卫一号信息系统数据库升级的实现

军卫一号信息系统数据库升级的实现 目的通过升级来提高军卫一号信息系统的运行效率，以适应医院医疗业务的发展。方法通过在测试服务器上进行操作系统和Oracle升级的模拟演练制定了详细的升级方案。根据既定方案完成正式服务器上的升级。结果该方法实现了操作系统和数据库系统的成功升级。结论操作系统与数据库的升级极大地提高了信息系统处理事务的能力，达到了预期目标。 Abstract：ObjectiveTo enhance the operation efficiency ofNo.1 Medical Project information system by upgrade to adapt to the development of the hospital medical business. MethodsBy means of the simulation exercises of operating system and oracle system upgrade on the test server making the upgrade program in detail and according to the established program to complete the upgrade on the formal server. ResultsThe operating system and database upgrade has been achieved successfully by this method. ConclusionOperating system and database upgrade improved the ability to handle affairs of the information system greatly and achieved the expected goal. Key words：No.1 Military Medical Project;Information system; Database upgrade武警北京总队医院是一所中型综合性医院。近年来，随着医院各项业务的不断发展，我院已跨入三甲医院的行列。随之而来的科室医疗业务扩大和收治的急速增加导致了信息系统客户端数量成倍的增长，而服务器所能连接的客户端数量却是有限的，从而使得数据库响应时间延迟。而面对急剧增加的数据量，软件系统较低的性能和管理能力一方面造成部分硬件资源的浪费，另一方面也使得整个信息系统的安全稳定面临严峻的挑战。在这种情形下，我们经过反复测试论证制定了详细的升级方案，在各科室的协同努力下，实现了了信息系统数据库从Windows2003 Server Enterprise X32+Oracle 8.16 X32到Windows2003 Server R2 Enterprise X64 +Oracle 11.2.0.3.0 X64的升級，突破了原来32位操作系统和Oracle 8.16管理使用内存的瓶颈，使得服务器硬件得到充分利用，同时极大地提高了数据库处理复杂事务的能力,为医院的医疗业务的持续发展奠定了良好的基础。 1模拟测试 1.1搭建模拟测试环境①准备一台支持64位操作系统的性能相对较高的测试服务器。由于受到经费影响，我们将原来存储数据库备份文件的服务器作为此次测试服务器，将数据库备份文件存储到集群中的一台服务器的本地硬盘上。②在测试服务器上安装操作系统Windows2003 Server R2 Enterprise X64和Oracle 11. 2.0. 3.0 X64。 1.2升级演练和测试 1.2.1在测试机上创建空数据库安装好Oracle 11.2.0.3.0 X64后，创建空数据库。创建空数据库时要注意以下几点：①空数据库的数据库名、SID以及字符集必须和原数据库一致；②数据库文件的存储位置必须与原数据库一致；③应结合

数据库原理试卷带答案

数据库原理试卷带答案

数据库原理试卷A 一、单选题（本题共20个小题，每题1分，共20分。答案唯一，多选或少选均不得分。请将答案按对应的题号写在下面的表格中） 1.下述关于数据库系统的正确叙述是( A )。 A. 数据库系统减少了数据冗余 B. 数据库系统避免了一切冗余 C. 数据库系统中数据的一致性是指数据类型一致 D. 数据库系统比文件系统能管理更多的数据 2. 数据库（DB），数据库系统（DBS）和数据库管理系统（DBMS）之间的关系是( A )。 A. DBS包括DB和DBMS B. DBMS包括DB 和DBS C. DB包括DBS和DBMS D. DBS就是DB，也就是DBMS 3. 描述数据库全体数据的全局逻辑结构和特性的是( A )。 A.模式 B. 内模式 C. 外模式 D. 用户模式 4. 要保证数据库的逻辑数据独立性，需要修改的是(A )。 A. 模式与外模式的映射 B. 模式与内模式之间的映射 C. 模式 D. 三层模式 5. 数据库系统的数据独立性体现在( B )。 A.不会因为数据的变化而影响到应用程序 B.不会因为系统数据存储结构与数据逻辑结构的变化而影响应用程序

C.不会因为存储策略的变化而影响存储结构 D.不会因为某些存储结构的变化而影响其他的存储结构 6. 在一个关系中如果有这样一个属性存在，它的值能惟一地 标识关系中的每一个元组，称这个属性为( C )。 A. 关键字 B. 数据项 C. 主属性 D. 主属性值 7. 现有如下关系： 患者（患者编号，患者姓名，性别，出生日起，所在单位） 医疗（患者编号，患者姓名，医生编号，医生姓名，诊断日期，诊断结果） 其中，医疗关系中的外码是( D )。 A. 患者编号 B. 患者姓名 C. 患者编号和患者姓名 D. 医生编号和患者编号 8. 自然连接是构成新关系的有效方法。一般情况下，当对关 系R和S使用自然连接时，要求R或S含有一个或多个共有的( D )。 A. 元组 B. 行 C. 纪录 D. 属性 9. 有关系SC（S_ID，C_ID，AGE，SCORE），查找年龄大于22岁的学生的学号和分数，正确的关系代数表达式是( D )。 ⅰ. πS_ID，SCORE (σAGE >22 (SC) ) ⅱ. σAGE >22 (πS_ID，SCORE (SC) ) ⅲ. πS_ID，SCORE (σAGE >22 (πS_ID，SCORE，

PDMS数据库的升级步骤(详细)

PDMS数据库升级教程如下： 如果需要把PDMS11.5的项目数据升级到PDMS12.0项目,需要执行以下的步骤。 第一步：把PDMS11.5的项目数据升级到PDMS11.6项目，具体请参考以下的步骤： 1.请您确保没有用户访问当前需要升级的项目 2.清理驻留用户（Expunge - all user processes） 3.对所有数据库执行DICE（Database Integrity Check）操作看是否报错，如果有报错请及时修复，然后才进行下一步。 Utilities> Integrity Check 4.对需要升级的项目进行备份 5.以FREE权限用户登录，进入monitor模块，打开命令行输入： $M D:\AVEVA\PDMS11.6.SP4\PDMSUI\dra\upgrade\upgradeMac (请注意：如果安装的PDMS版本和路径不同请自行修改。) 项目升级的方式，详细请查看随机安装的文档PDMS User Bulletin11.6的第2.5 Upgrading from PDMS 11章节。 第二步：把PDMS11.6的项目数据升级到PDMS12.0项目，具体请参考以下的步骤： 6.请您确保没有用户访问当前需要升级的项目 7.进入11.6的Admin模块，清理驻留用户（Expunge - all user processes） 8.对所有数据库执行DICE（Database Integrity Check）操作看是否报错，如果有报错请及时修复，然后才进行下一步。 Utilities> Integrity Check 9.对需要升级的项目进行备份

高通最强CPU骁龙835可运行完整的Windows 10

高通最强CPU骁龙835可运行完整的 Windows 10 高通公司在拉斯维加斯CES 2017大会上推出了全新的Snapdragon骁龙835处理器，该公司确认了这款新芯片可以运行完整版的Windows 10。微软在2016年底宣布，它正在与高通公司合作，在ARM处理器上推出完整的Windows 10系统，能够延长电池寿命而不影响设备的性能。 总部位于雷德蒙德的软件巨头也演示了高通骁龙820处理器运行Adobe Photoshop，微软两款Windows 10 Mobile 旗舰智能手机已经采用骁龙820处理器。然而，微软表示，虽然骁龙820确实能够运行完整的Windows 10，但骁龙835是第一将此功能带到零售市场的高通处理器。 今天，高通在其新闻声明中确认这是真的，骁龙835处理器旨在为高级消费者和企业设备（包括智能手机，VR / AR 头戴式显示器，IP摄像机，平板电脑，移动PC和其他设备）提供下一代娱乐体验和云连接服务，这些设备运行各种操作系统，包括Android和Windows 10，支持传统的Win32应用程序。 骁龙835支持完整的Windows 10对微软及其用户来说是好消息，特别是对那些非常渴望坚持使用Windows手机的

用户。这种新的仿真系统使微软有可能发明一个新的产品类别，并构建一个更高级的Windows手机，能够运行Win32应用程序，连接到一个更大的屏幕。这可能是微软传闻当中的Surface Phone，预计将在今年晚些时候推出，它将采用高通骁龙835处理器。当然，其他一些制造商也预计在他们的设备上使用该芯片，包括三星的旗舰Galaxy S8。