2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Язык компилирования доказательств
Сообщение21.04.2016, 02:33 


08/09/13
210
Существуют ли языки типа языков программирования (с соответствующими компиляторами), позволяющие формально записать доказательство как последовательность выводов, использовать уже выведенные утверждения, составлять что-то вроде программистских библиотек?
То есть такой язык, на котором можно было бы более-менее удобно записать доказательство и автоматически проверить? Как в учебниках по логике приводят "4=ModusPonenus(2,3)". Понятно, что формальные доказательства всегда ужасно длинные (и единица от Бурбаки, и всё такое...), но ведь можно, наверное, выделить те шаблоны, те очевидные утверждения, которыми мы пользуемся (их, может, много, но конечно), вынести их в отдельный файл такого языка и просто подключать. И потом наращивать аппарат доказательств...

У меня вообще первым делом возникла мысль такой язык создать (никогда ни о чём таком не слышал, а идея пришла), но потом решил поинтересоваться, наверняка, хотя бы попытки уже делались.

Просто странно как-то, что компьютер, использующий основным своим инструментом всё-таки математику, научился уже, кажется, хорошо решать сложные математические задачи, типа интегралов или чего ещё, а про системы формального вывода (который, по идее, должен быть проще) как-то нигде не упоминается. Мне на глаза, по крайней мере, не попадало.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 02:38 
Заслуженный участник
Аватара пользователя


11/12/05
9953
Пролог?

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 02:49 
Заслуженный участник
Аватара пользователя


23/07/05
17973
Москва
https://ru.wikipedia.org/wiki/Coq

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 03:03 


08/09/13
210
Dan B-Yallay
Пролог, насколько я его мельком видел, всё-таки всегда решает какую-то задачу, вычисляет. Ну, если угодно, ищет доказательства. А я говорю о том, чтоб не программа искала доказательство, а сама программа была доказательством и в дальнейшем анализе/переборе/вычислении не нуждалась.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 03:12 
Заслуженный участник
Аватара пользователя


23/07/05
17973
Москва
Непонятно тогда, чего Вы хотите.
Берите язык формальной математической логики, пополняйте его необходимыми элементами и пишите себе.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 03:16 


08/09/13
210
Я как раз и хочу узнать, что подобного уже сделано, чтобы велосипед не изобретать. Вот про Coq узнал, очень интересно, буду разбираться.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 09:02 
Модератор


19/10/15
1196
Есть много таких языков, например, Coq, Agda, Mizar, Isabelle, Lean.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 09:44 


14/01/11
2916
MetaMath ещё. Вообще, на этой страничке перечислено некоторое количество таких систем. Их можно найти, например, в категориях "proof checker" и "prover".

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 09:49 
Заслуженный участник
Аватара пользователя


19/12/10
1546
Упомяну ещё интересный российский проект языка Russell на основе Metamath.

Кстати, проект Mizar издаёт журнал Formalized Mathematics в котором публикуются доказательства проверенные этой системой.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение21.04.2016, 14:51 
Заслуженный участник


27/04/09
28128
Тут пока не сказали, так что добавлю: такие языки — часто часть системы, в которую входит ещё и proof assistant, сопоставляющий предлагаемую для доказательства формулу с базой уже доказанных теорем и некоторым набором правил и подсказывающий, как может выглядеть доказательство и заполняющий некоторые места самостоятельно.

 Профиль  
                  
 
 Re: Язык компилирования доказательств
Сообщение06.05.2016, 00:17 
Аватара пользователя


21/08/12

37
В любой системе с логикой высших порядков (HOL) можно определять новые понятия, их семантику, грамматику выражений, правила логики и тактики доказательств, потом все это выполнять. Хоть в JavaScript можно. Есть российский Refal, тоже работа с символами. Во всех математических пакетах есть средства символьной алгебры, хотя бы скобочки раскрывать, да выразить x через y где всё обращается. В metamath есть большой файл с теоремами, там вроде по Бурбаки много математики выстроено, любопытно посмотреть как практически с нуля всё начинается. Но там только верификация уже имеющихся доказательств. Про креатив есть работы по доказательству в HOL средствами логики первого порядка, строятся какие-то счетные множества теорем. Проблема как из всбесившегося принтера выловить практически ценные теоремы. Над всем довлеет проблема неразрешимости, то есть доказано, что в некоторых формальных системах не существует алгоритма доказательства любого выражения.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 11 ] 

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group