Заседание научного совета РАН по методологии искусственного интеллекта
19 января 2016
ЗАСЕДАНИЕ НАУЧНОГО СОВЕТА РАН ПО МЕТОДОЛОГИИ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА
26 января 2016 г., 16.00-19.00, 6 этаж, Красный зал
В институт можно попасть только по пропускам.
Желающие посетить заседание НСМИИ должны прислать на новый электронный адрес Совета свои данные (Фамилию, Имя, Отчество).
Новый адрес электронной почты Совета: scmaintel@mail.ru
Сопредседатели: академик С.Н. Васильев, профессор Д.И. Дубровский,
академик В.А. Лекторский, академик В.Л. Макаров
Координатор научных программ: А.Ю.Алексеев
Координатор молодежных программ: Е.А.Никитина
Ученый секретарь: Д.В. Иванов
16.00-17.00
Заседание совета
1. Об организации Всероссийской междисциплинарной конференции "Философия искусственного интеллекта", посвященной 60-летию научного направления «искусственный интеллект», 17-18 марта 2016 г., философский факультет МГУ имени М.В.Ломоносова, г.Москва
В.А.ЛЕКТОРСКИЙ
2. План мероприятий, посвященных 60-летней годовщине исследований искусственного интеллекта
АЛЕКСЕЕВ А.Ю.
3. Об итогах 9-й Всероссийской конференции студентов, аспирантов и молодых ученых «Искусственный интеллект: философия, методология, инновации»
НИКИТИНА Е.А.
4. Перспективы работы секции «Управление знаниями»
Ю.Ю.ПЕТРУНИН
5. О Центре по изучению проблем информатики, ИНИОН РАН
К.К.КОЛИН, Ю.Ю.ЧЕРНЫЙ
74-е заседание междисциплинарного научно-теоретического семинара "Философско-методологические проблемы искусственного интеллекта"
17.00-19.00
Обсуждение доклада
ИДЕЯ ВНУТРЕННЕЙ ЛОГИКИ, АКСИОМАТИЧЕСКИЙ МЕТОД И КОНСТРУКТИВНОЕ ПРЕДСТАВЛЕНИЕ ЗНАНИЙ
Докладчик: кандидат философских наук, старший научный сотрудник Института философии РАН (г.Москва), доцент кафедры проблем конвергенции естественных и гуманитарных наук Санкт-Петербургского государственного университета (г.Санкт-Петербург)РОДИН Андрей Вячеславович
Содокладчик-оппонент: доктор физико-математических наук, Институт проблем управления РАН (г.Москва) КОВАЛЁВ Сергей Протасович
Тезисы доклада
Идея внутренней логики, аксиоматический метод и конструктивное представление знаний
А.В.Родин
Аксиоматическое представление теорий - это основной способ представления теоретических знаний, который был разработан в докомпьютерную эпоху. Хотя история аксиоматического метода восходит, по крайней мере, к Евклиду, современная форма аксиоматического метода, которая на сегодняшний день продолжает считаться стандартной, была впервые предложена и использована в 1899-м году Давидом Гильбертом. В 20-м веке этот новый аксиоматический подход был принят на вооружение логиками и философами, которые с его помощью смогли получить ряд важных результатов, включая знаменитые теоремы Геделя о неполноте аксиоматических представлений арифметики и теорему Коэна о независимости континуум-гипотезы от аксиом теории множеств Цермело-Френкеля. В то же время успехи этого нового метода как инструмента для представления знаний, который мог бы быть использован не только в логической теории, но и в исследовательской и образовательной практике любой данной области знаний (математики, физики, биологии и т.д.), оказались гораздо более скромными. В начале компьютерной эры многим казалось, что использование быстродействующих электронных компьютеров поможет уменьшить разрыв между тем, что стандартный аксиоматический метод обещает в теории, и тем, что он дает на практике. Однако уже самые ранние попытки использования аксиоматического подхода в системах искусственного интеллекта вообще и в системах представления знаний в частности, наоборот, сделали эти трудности еще более явными. Поэтому, если в контексте ИИ не отказываться от идеи аксиоматического представления знаний вообще - что на наш взгляд было бы неоправданно - то необходимо использовать более адекватное понятие об аксиоматической теории, которое, с одной стороны, допускало бы компьютерную реализацию, и, с другой стороны, могла бы лучше учитывать специфические требования конкретных научных и технических дисциплин.
Проблема, о которой идет речь, является одновременно технической и концептуальной. Концептуальная часть проблемы состоит в том, что используемое в стандартном аксиоматическом методе и общепринятое в современной логике понятие (аксиоматической) теории на самом деле сильно отличается от того, что называют теориями математики, физики и другие исследователи. Техническая часть проблемы состоит в том, что для целей компьютерной реализации любое альтернативное понятие теории должно быть описано с такой же (или большей) математической строгостью, как и стандартное понятие. Возможное решение концептуальной части проблемы я вижу в том, чтобы переосмыслить роль и место логики в научных теориях и использовать понятие о внутренней логике, которое (в точном техническом смысле этого термина) впервые предложил Лавер в рамках своей аксиоматической теории топосов. Идея состоит в том, чтобы при построении аксиоматической теории не фиксировать базовое логическое исчисление заранее, а использовать более гибкую формальную схему, которая позволяет рассуждать содержательно, пользуясь особой геометрической семантикой и одновременно строить логическое исчисление, жестко связанное с используемой в данном рассуждении геометрической конструкцией. С математической и эпистемологической точки зрения такое понятие о внутренней логике полезно сравнить с понятием о внутренней геометрии пространства, которое впервые появилось в трудах Римана и затем было использовано Эйнштейном в Общей теории относительности. Идея о том, что данная научная теория или область знаний, вообще говоря, имеет “собственную внутреннюю логику” определяемую своим предметом, не только лучше отражает существующую научную практику, чем стандартный аксиоматический подход, но и имеет глубокие эпистемологические основания. В качестве такого эпистемологического основания я укажу на конструктивный характер научных и технических знаний, который исключает редукцию “знания как” к пропозициональному “знанию что”. Пользуясь понятием внутренней логики, я сформулирую новое понятие об аксиоматической теории, которое я предлагаю называтьконструктивной аксиоматической теорией.
В качестве примера технической реализации конструктивного аксиоматического подхода в докладе будет рассмотрена гомотопическая теория типов и тесно связанный с этой теорией, предложенный В. Воеводским, проектунивалентных оснований математики, который предполагает компьютерное представление математических утверждений и доказательств.