Формализация геометрии Тарского

Проект

Наш проект посвящен формализации геометрии Тарского в системах Isabelle/HOL и Coq. Репозиторий проекта: github.com/usr345/tarski_geo.

Геометрические свойства последовательно выводятся из аксиом и фиксируются в виде машинно-проверяемых доказательств.

В геометрии Тарского есть один базовый тип объектов — точка. 2 базовых отношения:

Свойства конгруэнтности отрезков и равенства длин.

Основные свойства тернарного отношения расположения точек между друг другом.

Аксиомы, задающие размерность геометрической структуры.

Принцип непрерывности, используемый в формальной разработке.

ФОРМАЛЬНАЯ РАЗРАБОТКА

ТЕКУЩИЕ РЕЗУЛЬТАТЫ

Результат Статус

congr_refl Доказано

congr_reverse Доказано

bet_sym Доказано

between_inner_trans Доказано

bet_inner_conn В работе

ФОРМАЛИЗАЦИЯ