Deductive Database Method based on Full-Angle

Given a geometry statement of the equality type, each hypothesis is considered as a fact (a property). All hypotheses of the statement form the initial database D0 of facts. Then we apply the rule set R to D0 to get new facts. We expand the database D0 by adding the new facts to D0 to have the enlarged database D1. We repeat the process for D1 to have an enlarged database D2. Since the number of points is finite, the numbers of segments, of angles, of triangles, and of circles are also finite. This process will finally terminate, i.e., there is k ≥ 0 such that Dk = Dk+1. Then we call Dk the fixpoint of the given geometric configuration. This process can be expressed by the following diagram:

JGEX uses breadth first forward chaining method to find new properties of this diagram. The naive form of breadth- rst forward chaining is notorious for its inefficiency. But, in the case of geometry, by using techniques from the theory of deductive database [6] and by introducing new search techniques, we manage to build a very effective prover based on this simple idea

Since the rule set R and the structured database are built into the source code, the prover is very efficient and the fixpoint can be generally reached within a fraction of a second even for an antique Pentium machine. If the conclusion (a fact also) is in the fixpoint, then we prove the statement to be true and the proof can be generated.


In JGEX, there are only 43 rules instead of 75 rules in [5], because some rules have been built into the structure of the deductive database. Please see Rules for Deductive Database Method.

For detail of this method please read our paper >>

 

Showing the Fixpoint.

Generally, the fixpoint has surprisingly rich amounts of information even for a very simple configuration. We can classify the facts in the fixpoint into several classes according to the geometric predicates: collinear, parallel, perpendicular, segment equal, cyclic, (full) angle equal, triangle
congruence, etc.


After the fixpoint is reached, we organize the database as an two-level tree. In this way, the user can explore the database to find some interesting facts.

For a theorem, please use the tabbed pane with "Fix" highlighted to see the fixpoint of the theorem.

 

JGEX Help