Rifat писал(а):
Начал смотреть на книгу Кушниренко и Лебедева "Программирование для математиков" немного под другим углом. Во многих книгах в качестве предусловия, постусловия, инварианта обычно выступают какие-то арифметические выражения. Но многие вещи очень сложно записать формально, поэтому необходимо записывать эти утверждения как-то неформально на естественном языке. Одно время я искал в гугле и в яндексе и на русском и на английском какие-нибудь источники, где бы были примеры утверждений на естественном языке. В этом плане данная книга - это как раз то, что я искал. Там большинство алгоритмов содержат дано (предусловие), получить (постусловие) и инвариант на естественном языке и служат примером как можно использовать естественный язык для описания утверждений.
Всё-таки, без формального бэкграунда все проблемы корректности, непротиворечивости, полноты и т.д., как и сама процедура рассуждений/верификации полностью возлагаются на человека.
А то, что гуглы молчат про "естественный математический", но формальный язык -- не удивительно. Единственные известные (относительно) исследования в этой области были (ну и есть) у Глушковцев в контексте "алгоритма очевидности" -- системы автоматизированного доказательства теорем (где построение выводов представляется в форме, "очевидной" для человека, предполагалось и для машин по мере развития искусственного интеллекта):
оф. сайт:
http://nevidal.orgкраткий истор. экскурс:
Алгоритм очевидности ГлушковаПостановка задач и определение фактов осуществляется на математическом языке, близком к естественному языку математических публикаций:
Спецификация:
http://nevidal.org/download/forthel.pdfКраткое описание:
Особенности обработки математических текстов в системе автоматизированной дедукцииНа сегодня доступен английский вариант, про русский и украинский, с их проблематикой, необходимо искать публикации тех лет. В основе язык имеет особенности согласно своей первичной предметке, но тезаурус расширяемый.
Вход
FAQ
Поиск
