Издательство СО РАН

Издательство СО РАН

Адрес Издательства СО РАН: Россия, 630090, а/я 187
Новосибирск, Морской пр., 2

soran2.gif

Baner_Nauka_Sibiri.jpg


Яндекс.Метрика

Array
(
    [SESS_AUTH] => Array
        (
            [POLICY] => Array
                (
                    [SESSION_TIMEOUT] => 24
                    [SESSION_IP_MASK] => 0.0.0.0
                    [MAX_STORE_NUM] => 10
                    [STORE_IP_MASK] => 0.0.0.0
                    [STORE_TIMEOUT] => 525600
                    [CHECKWORD_TIMEOUT] => 525600
                    [PASSWORD_LENGTH] => 6
                    [PASSWORD_UPPERCASE] => N
                    [PASSWORD_LOWERCASE] => N
                    [PASSWORD_DIGITS] => N
                    [PASSWORD_PUNCTUATION] => N
                    [LOGIN_ATTEMPTS] => 0
                    [PASSWORD_REQUIREMENTS] => Пароль должен быть не менее 6 символов длиной.
                )

        )

    [SESS_IP] => 3.238.132.225
    [SESS_TIME] => 1632739538
    [BX_SESSION_SIGN] => 9b3eeb12a31176bf2731c6c072271eb6
    [fixed_session_id] => 0a3adbd598d4fadde6fcf7eaa3ef9222
    [SALE_USER_ID] => 0
    [UNIQUE_KEY] => a4c6a59b1eb8be84dbe90bb7c9d7db96
    [BX_LOGIN_NEED_CAPTCHA_LOGIN] => Array
        (
            [LOGIN] => 
            [POLICY_ATTEMPTS] => 0
        )

)

Поиск по журналу

Философия науки

2020 год, номер 1

ИНТЕРАКТИВНОЕ ДОКАЗАТЕЛЬСТО: ВЕРИФИКАЦИЯ И ГЕНЕРИРОВАНИЕ НОВОГО МАТЕМАТИЧЕСКОГО ЗНАНИЯ

А.В. Хлебалин
Института философии и права СО РАН, 630090, г. Новосибирск, ул. Николаева, 8
sasha_khl@mail.ru
Ключевые слова: компьютерное доказательство, автоматизированные системы верификации в математике, гомотопная теория типов, доказательство, вычисление, computer-assisted proof, automate verification systems in mathematics, homotopy type theory, proof, calculation
Страницы: 87-95

Аннотация

В статье рассматриваются классические вопросы эпистемологии математики в связи с применением компьютерных систем в математическом исследовании. Показано, что зачастую проблемы эпистемологической характеристики математических результатов, полученных с помощью компьютера, связаны с непроясненностью содержания традиционных концепций эпистемологии математики, таких как доказательство, вычисление, истины и верификация. На примере характеристики логико-теоретических оснований интерактивных компьютерных систем, созданных на базе теории типов, демонстрируется их потенциал в области экспликации традиционных концепций эпистемологии математики.

DOI: 10.15372/PS20200105
Добавить в корзину
Товар добавлен в корзину