From 6e99a258e9ca6a8f73dfbef81906c2fa5b34ad9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=D0=9C=D0=B0=D0=BA=D1=81=D0=B8=D0=BC=20=D0=A1=D0=BE=D1=85?= =?UTF-8?q?=D0=B0=D1=86=D1=8C=D0=BA=D0=B8=D0=B9?= Date: Wed, 26 Feb 2025 10:52:07 +0200 Subject: [PATCH] =?UTF-8?q?Create=20=D0=90=D0=92=D0=A2=D0=9E=D0=A0=D0=95?= =?UTF-8?q?=D0=A4=D0=95=D0=A0=D0=90=D0=A2.md?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...20\244\320\225\320\240\320\220\320\242.md" | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 "\320\220\320\222\320\242\320\236\320\240\320\225\320\244\320\225\320\240\320\220\320\242.md" diff --git "a/\320\220\320\222\320\242\320\236\320\240\320\225\320\244\320\225\320\240\320\220\320\242.md" "b/\320\220\320\222\320\242\320\236\320\240\320\225\320\244\320\225\320\240\320\220\320\242.md" new file mode 100644 index 0000000..7e81e46 --- /dev/null +++ "b/\320\220\320\222\320\242\320\236\320\240\320\225\320\244\320\225\320\240\320\220\320\242.md" @@ -0,0 +1,27 @@ + +

+ + + + +

+ +

Перша формальна система

+ +

Формальне середовище виконання AXIO.PRO, система вищих мов та базові бібліотеки для програмування, доведення теорем і формальної філософії.

+ +

У роботі розказується про новий формальний підхід до математичної верифікації та спробу автора у цій парадигмі + побудувати замкнену уніфіковану систему формальних мов для програмування, математики та філософії. В процесі + розробки моделі такої системи автору довелося апробувати частини її імплементації для головних SML-подібних + формальних академічних мов, мови Erlang та інших (загалом 7 мов). За 10 років автором було проаналізовані + синтаксис та семантика основних мов програмування (більше 50 мов) з різних промислових та академічних доменів, + 8 мов з яких були особисто реалізовані автором. В роботі описані 8 мов уніфікованої мовної системи (концептуальна модель) +та представлені 2 їх імплементації, зокрема N2O.DEV. +Головним чином, натхнення було почерпнуте з LISP-машин минулого, APL-систем, перших систем доведення теорем таких як AUTOMATH, віртуальних маших паралельної та узгодженої обробки + нескінченних процесів, таких як BEAM, та кубічних MLTT-пруверів. Робота буде корисною всім аспірантам чистої та прикладної математики, теоретичної інформатики, а також інженерам цих спеціальностей для розуміння природи обчислень.

+ +

+Монографія — +Інститут — +Бібліотека +