GeometricTheoremProver.jl

A Julia library for automated deduction in Euclidean geometry.
Author lucaferranti
Popularity
20 Stars
Updated Last
27 Days Ago
Started In
January 2022

GeometricTheoremProver.jl

Pkg Info Build status Documentation Citation Contributing
versionlicense: MIT CIcodecov docs-stabledocs-dev zenodo contributions guidelines

Overview

A Julia package that can prove theorems in Euclidean geometry. Currently, it supports only Ritt-Wu method. For a brief overview check this video at JuliaCon2022.

Installation

Install the package with

julia> using Pkg; Pkg.add("GeometricTheoremProver")

then import the package with

julia> using GeometricTheoremProver

now you are ready to go.

Documentation

  • STABLE -- Documentation of the latest release
  • DEV -- Documentation of the current version on main

Quickstart Example

Let us prove that Apollonius circle theorem. First we state hypothesis and thesis

hp = @hp begin
    points(A, B, C)
    C := Segment(A, B)  Segment(A, C)
    M₁ := Midpoint(A, B)
    M₂ := Midpoint(A, C)
    M₃ := Midpoint(B, C)
    H := A  Segment(B, C)
    O := Circle(M₁, M₂, M₃)
end
POINTS:
------------
A : free
B : free
C : semifree by (1)
M₁ : dependent by (2)
M₂ : dependent by (3)
M₃ : dependent by (4)
H : dependent by (5)
O : dependent by (6)

HYPOTHESIS:
------------
(1) AB ⟂ AC
(2) M₁ ∈ AB ∧ AM₁ ≅ M₁B
(3) M₂ ∈ AC ∧ AM₂ ≅ M₂C
(4) M₃ ∈ BC ∧ BM₃ ≅ M₃C
(5) H ∈ BC ∧ AH ⟂ BC
(6) OM₁ ≅ OM₂ ≅ OM₃
th = @th H  Circle(O, M₁)
THESIS:
------------
OH ≅ OM₁

now the theorem can be proved with the prove function

prove(hp, th)
Assigned coordinates:
---------------------
A = (0, 0)
B = (u₁, 0)
C = (x₁, u₂)
M₁ = (x₂, x₃)
M₂ = (x₄, x₅)
M₃ = (x₆, x₇)
H = (x₈, x₉)
O = (x₁₀, x₁₁)

Goal 1: success

Nondegeneracy conditions:
-------------------------
u₁ ≠ 0
-u₁² + 2u₁x₁ - u₂² - x₁² ≠ 0
u₂ ≠ 0
4x₂x₅ - 4x₂x₇ - 4x₃x₄ + 4x₃x₆ + 4x₄x₇ - 4x₅x₆ ≠ 0
-2x₃ + 2x₇ ≠ 0

Contributing

If you spot something strange (something doesn't work or doesn't behave as expected), please open a bug issue.

If have an improvement idea (a new feature, a new piece of documentation, an enhancement of an existing feature), you can open a feature request issue.

If you feel like your issue does not fit any of the above mentioned templates (e.g. you just want to ask something), you can also open a blank issue.

Pull requests are also very welcome! For small fixes, feel free to open a PR directly. For bigger changes, it might be wise to open an issue first. Also, make sure to checkout the contributing guidelines.

Acknowledgement

Used By Packages

No packages found.