GeometricTheoremProver.jl
Pkg Info | Build status | Documentation | Citation | Contributing |
---|---|---|---|---|
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
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
- Author: Luca Ferranti
- License: MIT