2014 dxdy logo

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

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




Начать новую тему Ответить на тему
 
 О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 16:00 


08/03/11
273
Здравсвуйте !
Представляет ли научную ценность результаты в математике, где значительно использованы средства автоматической дедукции ?
Модель и методы - это человек. А все бремя логического вывода - творению человека - логическому пруверу на пути к механической математике :shock:

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 16:15 
Аватара пользователя


11/06/12
10390
стихия.вздох.мюсли
Представляют ли ценность дороги, проложенные с помощью бульдозеров и асфальтоукладчиков? Представляют ли ценность тоннели, проложенные с помощью проходческих щитов? Представляет ли ценность рагу, приготовленное в мультиварке?
Человек придумал множество инструментов, облегчающих ему жизнь. Автоматические доказыватели ничуть не хуже.

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 16:33 
Заслуженный участник
Аватара пользователя


31/01/14
11017
Hogtown
Aritaborian в сообщении #988765 писал(а):
Представляют ли ценность дороги, проложенные с помощью бульдозеров и асфальтоукладчиков?

Пока эти самые автоматические доказыватели подобны бульдозеру без бульдозериста и AI и работаю по принципу: где проедет там и дорога будет. Разумеется, речь идет о чисто computer proof, не computer assisted proof. В посленем случае некий трудоёмкий перебор или расчёт осуществляется компьютером.

Пока в своей области (анализ и около) я не видел ничего доказанного компьютером самостоятельно (включая что-либо тривиальное)

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 16:53 
Аватара пользователя


21/09/12

1871
Проблема четырёх красок ещё в 1976 году была решена на ЭВМ. И с тех пор простого "короткого" доказательства не получено. Поворчали немного и успокоились. Решена так решена. - На компе.

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 16:58 
Аватара пользователя


11/06/12
10390
стихия.вздох.мюсли
Кажется, мы говорим об одном и том же.

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 17:19 
Аватара пользователя


21/09/12

1871
Aritaborian в сообщении #988782 писал(а):
Кажется, мы говорим об одном и том же.

Да. Ваш лозунг, а у меня пример к нему.

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 17:20 
Аватара пользователя


11/06/12
10390
стихия.вздох.мюсли
И Red_Herring о том же говорит. Комп без человека точно так же ничего не может, как бульдозер, асфальтоукладчик и мультиварка.

 Профиль  
                  
 
 Posted automatically
Сообщение11.03.2015, 17:25 


20/03/14
12041
 i  Тема перемещена из форума «Дискуссионные темы (М)» в форум «Беседы на околонаучные темы»

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение11.03.2015, 17:38 
Заслуженный участник


31/12/05
1406
atlakatl в сообщении #988778 писал(а):
Проблема четырёх красок ещё в 1976 году была решена на ЭВМ. И с тех пор простого "короткого" доказательства не получено. Поворчали немного и успокоились. Решена так решена. - На компе.

Доказательство 1976 года было типичным computer-assisted proof, то есть была написана какая-то программа, которая произвела какой-то перебор, и к ней было приделано полуформальное доказательство, что перебор полный и программа верна.
В 2005 году доказательство (точнее, вариант Робертсона-Сандерса-Сеймура-Томаса 1997 года) было полностью формализовано в Coq и теперь уже является компьютерным.

В 2012 году та же команда формализовала доказательство теоремы Фейта-Томпсона о разрешимости групп нечетного составного порядка. Естественно, пришлось формализовать не только 255-страничное доказательство, но и пару книжек по алгебре и анализу.

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение14.03.2015, 08:01 


08/03/11
273
У меня возникло убеждение, что существует класс проблем, которые человек в принципе никогда без средств автоматизации решить не сможет.

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение14.03.2015, 10:37 


19/05/10

3940
Россия
Со средствами или без средств - это, в принципе), одно и тоже. Средства автоматизации человек делает или инопланетяне?

 Профиль  
                  
 
 Re: О ценности доказат. в математ. с использ. автом.дедукции
Сообщение14.03.2015, 10:52 


08/03/11
273
Даже если какие-то математические результаты реально очень существенно были получены с помощью средств автоматизации,
при публикации эти средства претерпевают переоценку - их называют экспериментами; плюс - приводится традиционное доказательство, явно не имеющей
достаточной строгости.

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

Модератор: Модераторы



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

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


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

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