https://github.com/mirefek/geo_logic

Skip to content
 
Sign up

  * Product
      + Features
      + Mobile
      + Actions
      + Codespaces
      + Copilot
      + Packages
      + Security
      + Code review
      + Issues
      + Discussions
      + Integrations
      + GitHub Sponsors
      + Customer stories
  * Team
  * Enterprise
  * Explore
      + Explore GitHub
      + Learn and contribute
      + Topics
      + Collections
      + Trending
      + Skills
      + GitHub Sponsors
      + Open source guides
      + Connect with others
      + The ReadME Project
      + Events
      + Community forum
      + GitHub Education
      + GitHub Stars program
  * Marketplace
  * Pricing
      + Plans
      + Compare plans
      + Contact Sales
      + Education

[                    ] 

  *  
    #
    In this repository All GitHub |
    Jump to |

  * No suggested jump to results

  *  
    #
    In this repository All GitHub |
    Jump to |
  *  
    #
    In this user All GitHub |
    Jump to |
  *  
    #
    In this repository All GitHub |
    Jump to |

Sign in
Sign up
{{ message }}
mirefek / geo_logic Public

  * Notifications
  * Fork 4
  * Star 16

Tool for euclidean geometry aware of logic

16 stars 4 forks
Star
Notifications

  * Code
  * Issues 0
  * Pull requests 0
  * Actions
  * Projects 0
  * Wiki
  * Security
  * Insights

More

  * Code
  * Issues
  * Pull requests
  * Actions
  * Projects
  * Wiki
  * Security
  * Insights

mirefek/geo_logic

This commit does not belong to any branch on this repository, and may
belong to a fork outside of the repository.
master
Switch branches/tags
[                    ]
Branches Tags
Could not load branches
Nothing to show
{{ refName }} default View all branches
Could not load tags
Nothing to show
{{ refName }} default
View all tags
2 branches 1 tag
Code

Latest commit

@mirefek
mirefek bugfix
...
c8c9b71 Jul 25, 2021
bugfix
c8c9b71

Git stats

  * 98 commits

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
article
update levels with solutions, article acknowledgement update
Mar 26, 2020
images
change cursor for hide / unhide
Mar 26, 2020
pictures
add svg directory
Feb 19, 2020
saved
add flower level
Mar 29, 2020
README.md
typo
Jul 9, 2020
angle_chasing.py
source code comments
Mar 19, 2020
basic.gl
added Morley's Miracle
May 29, 2020
basic_tools.py
source code comments
Mar 19, 2020
cairo_textedit.py
label tool
Mar 3, 2020
debug.gl
lies_on visualisation
Jan 23, 2020
file_chooser.py
source code comments
Mar 19, 2020
geo_logic.py
escape as cancel (same as right click)
Sep 22, 2020
geo_object.py
source code comments
Mar 19, 2020
graphical_env.py
bug fixes
Feb 26, 2021
gtool.py
change cursor for hide / unhide
Mar 26, 2020
gtool_constr.py
source code comments
Mar 19, 2020
gtool_general.py
source code comments
Mar 19, 2020
gtool_label.py
bugfix -- label tool + undo
May 9, 2020
gtool_logic.py
drawing method of lies_on changed (with the same visual outcome),
bug...
Jul 28, 2020
gtool_standalone.py
Combined GUI tools, selection highlighting
Feb 7, 2020
gui_tool_icons.py
GUI tuning -- toolbar
Feb 13, 2020
knowledge_visualisation.py
bugfix with visualisation of invisible parallels
Sep 22, 2020
label_visualiser.py
source code comments
Mar 19, 2020
logical_core.py
typo
Sep 22, 2020
macros.gl
bug fixes
Feb 26, 2021
movable_tools.py
typo
Sep 22, 2020
num_duplicities.py
lies_on visualisation
Jan 23, 2020
parse.py
save label positions, fix save level solution
Mar 19, 2020
primitive_constr.py
added Morley's Miracle
May 29, 2020
primitive_pred.py
source code comments
Mar 19, 2020
primitive_tools.py
source code comments
Mar 19, 2020
relstr.py
source code comments
Mar 19, 2020
segment_union_diff.py
added file
Jul 28, 2020
sparse_elim.py
bug fixes
Feb 26, 2021
sparse_row.py
source code comments
Mar 19, 2020
step_list.py
source code comments
Mar 19, 2020
stop_watch.py
source code comments
Mar 19, 2020
technical_doc.txt
change cursor for hide / unhide
Mar 26, 2020
todo
update todo
Mar 27, 2020
tool_step.py
start_out obligatory
Sep 22, 2020
tool_step_utils.py
simple functions for manipulating steps
Sep 22, 2020
toolbar.py
source code comments
Mar 19, 2020
tools.py
support for some geogen theorems, double angle display bug fix
Aug 4, 2020
triggers.py
source code comments
Mar 19, 2020
uf_dict.py
source code comments
Mar 19, 2020
uf_set.py
initial commit
Sep 10, 2019
view_port_ori.py
progress on enhanced visualization
Feb 3, 2020
viewport.py
bugfix
Jul 25, 2021
View code
[                    ]
GeoLogic Dependencies Data types Semi-formal logic Automation
Controls Ambiguous objects Point (Parallel) Line Perpendicular Line
Circle Circumcircle Reason Label

README.md

 GeoLogic

Tool for euclidean geometry aware of logic

For studying the source code, start here.

GeoLogic Screenshot

 Dependencies

  * Python3
  * pyGtk3
  * numpy (on Windows: "pacman -S mingw-w64-x86_64-python3-numpy")

 Data types

GeoLogic can handle five types of objects: Point (P), Line (L),
Circle (C), Angle (A) (which include a direction of a line or a
"length" of an arc), and Ratio (D) (ratio of products of lengths,
including a length itself). From these five data types, only three of
them can be matipulated using the GUI -- points, lines and circles.
Every object in the GL file is of one of these types, the types of
input and output objects are in the header of every tool.

 Semi-formal logic

The background logical system requires proofs of exact statements
(e.q. line contain a point, two angles are identical, ...) but for
topological facts (two circles intersect each other, two triangles
are identically oriented) it only checks numerically.

It is possible to write lemmata for GeoLogic -- some are in the file
macros.gl. However, whenever a lemma is used, GeoLogic also checks
whether the proof of the lemma works in this particular numerical
setting.

It is not possible to create lemmata in the user interface yet (it is
a planned feature).

 Automation

As an interactive theorem prover, GeoLogic intentionally does not
possess much automation, especially if it can be circumvented with
visual steps. There are basically four ways in which GeoLogic makes
automatic decisions:

  * Gaussian elimination for angles: GeoLogic uses "oriented angle
    chasing" for deriving facts about angles (similar to Full Angle
    Method). Every angle is defined as a difference between the
    directions of corresponding lines. Whenever an equality (modulo
    rational multiple of pi) can be infered, GeoLogic recognizes it.
  * Gaussian elimination for log-distances: Whenever an equality of
    the form of a ratio of products of certain lengths can be
    infered, GeoLogic recognizes it. Note that GeoLogic cannot "add"
    distances, only multiply, as it is the more common operation with
    them.
  * Extensionality: Whenever x0=y0, x1=y1, ..., xn=yn, then f
    (x0,...,xn) = f(y0,...,yn) for any f being a primitive command /
    defined macro.
  * Equality triggers: Besides extensionality, there are a few extra
    ways how GeoLogic automatically detect identical objects: two
    lines passing two disting points are equal, two points lying on
    two intersecting clines are equal, etc.

 Controls

All non-movable logical tools which take only graphical objects
(Point / Line / Circle) on input can be reached using the entry-area
in the up right corner of the window.

Tools that can turn out to be useful:

  * (triangle centers) centroid, orthocenter, circumcenter, incenter,
    excenter
  * (lemma) midsegment -- recognizes that the midsegment of a
    triangle is parallel and half long
  * (lemma) midpoint_uq -- recognizes that a point on line having the
    same distances is a midpoint
  * copy_triangle, copy_triangle_r -- constructions of similar /
    congruent triangles
  * sim_, cong_ -- lemmata about similar / congruent triangles

There are also six "smart" graphical tools that automaticaly run the
appropriate logical tool, and can be used for constructing movable
objects. Right click resets the current tool.

 Ambiguous objects

If two numerically identical objects are about to be shown, GeoLogic
shows only one of them. They can be swapped using shift-click. During
holding shift, the ambigous object turn slightly red.

 Point

  * Free point: click into space
  * Point on line / circle: click on it
  * Intersection: click near intersection
  * More detailed intersection of clines 'a', 'b': drag from 'a' to
    'b'
  * Midpoint: click on two points
  * Circle center: drag from circle to its center
  * Foot: click on point, then line / circle near foot
  * Foot: click to point, then drag from one point to another
  * Opposite point on circle: click on point X, then on circle
    containing X near the opposite point
  * Midpoint on an arc: select point X, circle containing X, the arc
    direction, and the second point

 (Parallel) Line

  * Line through two points: click the points (can be free if the
    second click is into space)
  * Parallel: click on a line (of drag between points), and then
    click on a point (or into space)
  * Tangent: click on point, and then on circle near possible
    touchpoint.
  * Angle bisector A B C: select B, drag A->C

 Perpendicular Line

  * Perpendibular bisector: click two points
  * Perpendicular line: click on a line (of drag between points), and
    then click on a point (or into space)
  * External Angle bisector A B C: select B, drag A->C

 Circle

  * Circle with center O: select O, then click to space / to a point
    / to a line near possible touchpoint
  * Compass: select circle / drag between points, then select another
    point / click into space

 Circumcircle

  * Free circle through 1 or 2 points: click the point(s), then into
    space
  * Circle with diameter: select the diameter, and confirm by
    clicking on one of the two points
  * Circumcircle: select three points

 Reason

  * Given point X lies on a circle w, infer its distance from center:
    Select X w
  * Given point X has the right distance from the center of w, infer
    that w contains X: Select w X
  * Given X Y see the segment A B at the same angle, infer they are
    concyclic: Select X Y, drag A->B
  * Given X Y A B are concyclic, infer angle equality AXB = AYB: Drag
    A->B, select X Y
  * Inscribed angle theorem about AXB: Select X, drag A->B
  * Inverse inscribed angle theorem about AXB on a circle w, infer w
    contains X: Drag A->B, then select X and w
  * Given X lies on a perpendicular bisector l of AB, infer AX=BX:
    Drag A->B, select l, then X
  * Given AX=BX, infer X lies on a perpendicular bisector l of AB:
    Drag A->B, select X, then l
  * Given two arcs AB, CD of the same circle w are equal, infer equal
    distances: select w, drag A->B, drag C->D (in the same direction)
  * Given AB=CD on a circle w, infer equal arcs: select w, then
    select consecutively A, B, and C, D (in the same direction)

 Label

  * Hide / Show label
  * drag -> change label position
  * when appears, labels captures the keyboard and allows editing,
    confirmed by enter / click
  * In the label, everything can be in subscript or in the main text.
    It tries to figure out automatically how it should be, eventually
    it can be adjusted by adding underscores.

About

Tool for euclidean geometry aware of logic

Resources

Readme

Stars

16 stars

Watchers

3 watching

Forks

4 forks

Releases 1

 
GeoLogic 0.2 Latest
Mar 27, 2020

Packages 0

No packages published

Languages

  * Python 84.6%
  * TeX 15.4%

Footer

 (c) 2022 GitHub, Inc.

Footer navigation

  * Terms
  * Privacy
  * Security
  * Status
  * Docs
  * Contact GitHub
  * Pricing
  * API
  * Training
  * Blog
  * About

You can't perform that action at this time.
You signed in with another tab or window. Reload to refresh your
session. You signed out in another tab or window. Reload to refresh
your session.