geometer / sandbox Goto Github PK

In the current version, essentiality is a property attribute and only depends on the property type and value. Should also depend on the reason.

See #19 for an explanation of what is the level.

If the idea of the project works, re-write most important parts in a low-level language (C++?) for performance

The idea is to convert a sketch (e.g., in Geogebra format) into a problem description. A literal translation of Geogebra scene into a problem does not work as expected. E.g., if in Geogebra we take a segment AB, then a perpendicular line through B, a circle with centre B with radius BA, then an intersection point C of the perpendicular and the circle, etc. In the problem description, there should be just "ABCD is a square".

The keywords in this task are "pattern recognition". There are several approaches to this task:

• "Classical" pattern recognition like implemented in https://geometry.allenai.org
• Usage of hunter to find patterns, then of explainer to prove them
• Or even usage some neural network-based pattern recognition (actually, I do not expect this way makes a sense)

Because it uses pairs of angles as keys; use pair of (congruent) angle families instead.

For each property, introduce a negated property. E.g., for “two triangles are similar”, there should be “two triangles are not similar”. This would be useful for detecting contradictions as soon as possible, and also for speeding up the algorithm. There is no need to test for similarity again and again on each iteration if it is already known, but also if its negation is already known. Of course, there is no need to generate all possible negated properties. Only the negations that are found in a natural way (i.e., during looking for “positive” properties) should be stored.

At the moment, it is not possible to express equality like |AB| * |CD| = 2 * |EF|^2

Create/collect/find a large problem set in machine-readable form (using own task format, or python, or some existing format + parser)

All computational rules, like SumAndRatioOfTwoAnglesRule or EqualSumsOfAnglesRule should be replaced by a single "computational core", that will store the facts (= equalitities and maybe inequalities) and generate new facts with explanations by request.

As the first step, it would be possible to implement a "linear facts set" for the angles.

It would be nice if it is possible to use solvers from sympy library. Not sure there is a chance to extract some kind of explanation from the solver.

Use https://www.mathjax.org/ to present math objects and formulas in the web presentation.

This is a meta-task that completes when all property creation calls are moved from explainer.py to separate classes in sandbox/rules

The new system, based on Comment class instead of obsolete LazyComment is

1. More flexible: we can define printers for strings, and we do use it to implement MathJax text processing on the server
2. Safer: there is parameter type checking in this new version
3. Again, more flexible: it can be used for strings localisation as the order of the parameters does not matter in this new solution

The migration is not complete yet. LazyComment must die!

At the moment, it is not possible to express properties like "Angle A < 45 degree" or "|AB| > |CD|"

Introduce new properties that reflect geometric facts related to circles:

• A point belongs to a circle (done)
• A point lies inside (outside) a circle
• A point is the centre of a circle
• A straight line intersects (does not intersect) a circle
• A straight line tangents a circle
• Two circles intersect one to another
• Two circles tangent one to another (inside or outside)
• A circle lies inside (outside) a circle

In the explainer, introduce ContradictionException, that raises if the reason generates a contradiction. This is an important part of the explainer with assumptions described in #7

At the moment, there is no way to express a property of an external angle of the triangle, because the external angle (a supplementary to "normal" angle of a triangle) has no point on its outer side. This causes it is impossible to write a number of problems.

Currently, only boolean value essential/not essential stored per property. Should be replaced with integer value in range 0..5 or 0..10. The checkbox in the web view to be replaced with a range control.

New suggested properties are

• IsSquareProperty
• PointIsIntersectionOfTwoLinesProperty
• PointIs(Incentre,Orthocentre,Circumcentre,Centroid)OfTriangleProperty
• PointIsCentreOfEquilateralTriangleProperty
• PointInsideTriangleProperty

This would be a significant step to #17
Additionally, implementing of this property resolves "centre of degenerate equilateral" problem

If the app that generates solution trees is (more or less) complete, one of the possible next steps is to implement some algorithms to select key steps in proofs. The proof tree is typically too big, and most of the branches are not interesting for a human.

Maybe, the algorithm should be personalised (different people might feel different steps as essential).

We only use the shortest path (for a graph with weighted edges) algorithm from the library. Currently, this is the slowest part of the prover algorithm.

With an exhaustive search of possible additional constructions (there should be a set of such constructions) implement a prover that tries to add construction and deduct the goal in the new extended scene. It should be combined with "prover with assumptions" (#7) to make a final product.

In a real planimetry task, there should be enough to add a very limited number of assumptions and/or constructions to deduct the goal.

This rule should be replaced with auto-generator than generates similar properties for all segments on the same line

PropertySet.coincidence_property is a more accurate replacement

The current design makes impossible to try non-trivial rule order experiments like "run the rule once per three iterations" or "run the rule several times per iteration". Moreover, the new technique can guarantee that each rule is applied only once to the data (in the current design it can be applied once or twice).

For design reasons, the app uses two parallel structures that describe geometric properties: the properties, used by hunter and explainer, and constraints, used by scene creator. Originally, the constraints system was richer than the properties. It seems like the properties are now powerful enough to express all the facts currently presented by the constraints. It would be great to drop the constraints and use the properties everywhere.

Seems like it belongs to the way more than to the fact; sometimes coincidence of angles is a thing we have to prove. E.g., to prove that a point belongs to a line.

On the other hand, this makes text representation of a property depending on the reason.

It is rarely used and can be replaced with more clear solutions.

If the direct prover fails (i.e., stops with no proof for the goal), it should

• select a fact that could have different answers, e.g. "the point lies on the circle", "the point lies inside the circle", and "the point lies outside of the circle";
• consequentially run direct provers starting with the property set + one of the assumptions;
• each run generates one of the following results: (1) the goal is proven, (2) a contradiction found, (3) no result, and (4) failure: the prover generates an assertion error;
• if all the results are of type (1) or (2), and at least one of them is of type (1), we have proof;
• otherwise, select or add another fact.

See also #10 for the next step.

It should be human-readable and writeable and machine-readable. That would be nice to use an existing format if any.

Re-write explainer rules from python into some compact language, that describes the source properties, the target property, and the matching rules

Currently, there are "paired" transitivity sets: one containing cycle ABC, another one containing cycle ACB. The sets contain the same information, but it is computed twice. Should be fixed for performance optimisation. (On 4.1.1 it takes ~10% of overall computational time.)