https://github.com/mirefek/geo_logic
Tip revision: 80598a9ddc0ad7e7c7c92a49c29def7322372c72 authored by Mirek Olšák on 04 June 2024, 21:34:41 UTC
bugfix
bugfix
Tip revision: 80598a9
todo
0.3 (during following months, ideally until ICMS-2020 13.7. -- deeper connection between GUI and logic)
Main objectives for 0.3:
* (1) ability to create custom tools / lemmata
* (1a) level creation
* (1b) more flexible step editing
* (2) level solving
* (2a) capture basic solving steps (problem reformulation, partial goal)
* (2b) detect solved level (including sublemmata)
* (3) support for problems without direct construction
* (3a) (re)capturing objects by a construction
* examples
* three points, circumcenter, and a point on it
-> first a circle, then 4 points on it
* triangle ABC, its incenter I
-> first triangle ABI, constructing C out of it
* given X,Y on a line so that XA = YB, make X movable and Y constructed using compass
Co je obecný stav?
* (1,3) (nehýbatelné) vstupní objekty
* (1) předpoklady (postulate)
* (1) proof (check, nevadí, když jednotlivý krok selže)
* (1,1b) závěry (check, možnost vytvořit pouze pár typů)
* Dorozmyslet (!):
* Pravidla přechycení,
a jak zajistit kompatibilitu s původním levelem
Akce:
* (3a) "zafixovat" objekt závislý jenom na vstupních objektech
* (přidat předpoklady)?
* (3a) Jak něco odfixovat?
* TODO
* (1a) fact tool (pro začátek funkčnost jako v geogebře -- numerický check)
* přidat předpoklad, přidat cíl
* odebrat předpoklad / cíl
* (1b) přesunout / smazat krok
* (1b) analýza, proč krok selhal
* (1b) otevřít krok
* (1b,2a) přehled lemmat, která nejsou dokázaná
* (2b) reset input, check všech důkazů
* (1b) editace, k čemu je chycený průsečík
* (2a)
* stanovení podcíle
* vybrat vstupní objekty
* vybrat předpoklady
* podcíl
* (export podcíle jako nástroje)
* reformulace cíle
* TODO
* jak zkombinovat fix / unfix a editaci předpokladů s řešením levelu?
* undo / redo v rámci komplexnějšich akcí
Remained
* more straightforward drawing of lies_on, computation of missing line:
* own implementation of line / circle cut for points not contained by them
-> cleaner exported picture, less drawing moves
* completely movable objects line / circle
long-term (more features)
* display equations
* geometrical mappings
* general similar mapping without exceptions (copy_triangle does not support collinear points)
* transferring objects, facts
* automatic proof of compatibility of a symmetry and a tool
* separate logic and automatization
* trace the assumptions used for a proof
* other intersection options?
* So that XOO' has the same orientation as ABC
* with a line AB firther in the direction AB
(both cases can be emulated using current tools)
* more sophisticated tools
* hidden construction
* so there are less known facts in the end
* non-expanding composed predicated (such as tangent)
* num_check optimisation
(find the propositions in a proof that should be checked without
executing the entire proof from scratch)
* alternative proofs (if the original proof fails)
* allow proof more mixed with conclusions?
* rigid check of elementary facts (topological reasoning)
* case split
* proof by contradiction
* inequalities -> linear programming?
* predicates:
* ordered: P P P, P L P, P P L
* oriented_as as a predicate about directions (Angle)
* axioms / lemmata?
* COMPLEMENTARY: A == B, A not_eq B
* COMPLEMENTARY: A lies_on pc, A not_on pc
* INCOMPATIBLE:
oriented_as a0 a1 a2 b0 b1 b2
oriented_as a0 a1 a2 b0 b2 b1
* COVERING:
oriented_as a0 a1 a2 b0 b1 b2
oriented_as a0 a1 a2 b0 b2 b1
a0 == a1
a1 == a2
a2 == a0
b0 == b1
b1 == b2
b2 == b0
* COVERING:
A == B
B == C
C == A
l = line A B, C not_on l
ordered A B C
ordered A C B
* A not_on l, B lies_on l -> A != B
* ordered A p B -> A != B, intersecting (line A B) p
* A not_on (line B C) -> B not_on (line A C)
* M = midpoint A B -> ordered A M B
* ordered: transitivity + symmetry
* ordered A B C -> not_eq A B, not_eq A C
* ordered A p B -> not_on A p, not_eq A B
* ordered A B p -> not_on A p, not_on B p
* ordered A B C, B lies_on p, A not_on p -> diff_side A p C
+ similar analogous
* oriented_as: transitivity + symmetry
* A not_on p, B C D on p, ordered B C D
-> oriented_as A B C A B D
* angle_pred a == (const != 0) + b -> not_eq a b
* (direction_of l1) != (direction_of l2) -> intersecting l1, l2