(scroll down for Russian version; русская версия в нижней части страницы)
Project Description (Résumé):
The proposed research project is focused on a particular problem in Formal Epistemology, namely the problem of justification and verification of knowledge. Presently this problem stands open in Computer Science and Digital Technologies as well as in the Philosophical Logic. While the traditional epistemology draws a sharp distinction between true belief and knowledge as justified true belief, this conceptual distinction is hardly taken into consideration in the Knowledge Representation as a CS discipline. As a practical outcome the existing KR systems don’t provide their users with means for a routine checking and verification of knowledge. Recent results obtained on boaderlines between computational mathematical logic, formal epistemology and CS give new promising possibilities for developing formal justificatory procedures. The aim of the present project is to use up-to-date formal logical tools and bearing in mind current digital KR systems, to lay out a foundation of formal epistemological theory, which can be used for developing of a new generation of KR systems supporting a large spectrum of justificatory procedures available to their users.
supported by RFBR grant 19-011-00799
Participants:
Vladimir Vasyukov (IP RAS)
Sergei Titov (IP RAS)
Sergey Kovalyov (ICS RAS)
Danya Rogozin (MSU)
Andrei Rodin (IP RAS, PI)
George Shabat (RSUH)
Recent publications:
Truth and Justification in Knowledge Representation (with Serge Kovalyov) (pdf) to appear in the Proceedings of the 7th Workshop “What can Formal Concept Analysis do for Artificial Intelligence?” (August 10-17, 2019, Macao, China) , in CEUR Workshop Proceedings
Models of HoTT and the Constructive View of Theories, in: Stefania Centrone, Deborah Kant and Deniz Sarikaya (eds.) Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts, Springer, Synthese Library vol.407., pp. 191-219
(FOMUS Proceedings). (pdf)(on PhilSci) DOI: 10.1007/978-3-030-15655-8_9
Formal Proof-Verification and Mathematical Intuition: the Case of Univalent Foundations, in: 16th INTERNATIONAL CONGRESS ON LOGIC, METHODOLOGY AND PHILOSOPHY OF SCIENCE AND TECHNOLOGY BRIDGING ACROSS ACADEMIC CULTURES (Prague, August 5-10, 2019), Book of Abstracts, p. 418 (pdf)
Recent Talks: Seminar Constructive Knowledge
Проблема обоснования знаний в формальной эпистемологии
поддержан РФФИ, грант 19-011-00799
Проект посвящен конкретной проблеме теории и практики формализации знаний, а именно проблеме формализации процедур обоснования и верификации знаний. Эта проблема остается на сегодняшний день открытой как в компьютерных науках и цифровых технологиях, так и в философской логике. В то время как традиционная философская эпистемология проводит четкое различие между истинным мнением и знанием (как обоснованным истинным мнением), формализация этого различия с помощью стандартных логических средств оказывается затруднительной. В теории представления знаний как разделе компьютерной науки это важное понятийное различие на сегодняшний день, как правило, вовсе не учитывается. В практическом плане это приводит к тому, что существующие системы цифрового представления знаний не предоставляют пользователям никаких специальных средств для рутинной проверки тех знаний, к которым пользователи данной системы получают доступ.
Полученные в последние годы результаты исследований на стыке вычислительной математической логики, формальной эпистемологии и компьютерной науки предоставляют новые возможности для эффективной формализации и вычислительной реализации обосновательных процедур. Цель настоящего проекта состоит в том, чтобы используя современные формально-логические средства и ориентируясь на существующую практику использования цифровых систем представления знаний, заложить основы формальной эпистемологической теории которая в будущем сможет быть использована для построения цифровых систем представления знаний нового поколения, которые будут предоставлять пользователям широкий спектр обосновательных процедур.
Участники:
Владимир Васюков (ИФ РАН)
Сергей Титов (ГАУГН и ИФ РАН)
Сергей Ковалёв (ИПУ РАН)
Даниил Рогозин (МГУ)
Андрей Родин (ИФ РАН, руководитель),
Георгий Шабат (РГГУ)
Truth and Justification in Knowledge Representation (with Serge Kovalyov) (pdf) to appear in the Proceedings of the 7th Workshop “What can Formal Concept Analysis do for Artificial Intelligence?” (August 10-17, 2019, Macao, China) , in CEUR Workshop Proceedings
Models of HoTT and the Constructive View of Theories, in: Stefania Centrone, Deborah Kant and Deniz Sarikaya (eds.) Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts, Springer, Synthese Library vol.407., pp. 191-219
(FOMUS Proceedings). (pdf)(on PhilSci) DOI: 10.1007/978-3-030-15655-8_9
Formal Proof-Verification and Mathematical Intuition: the Case of Univalent Foundations, in: 16th INTERNATIONAL CONGRESS ON LOGIC, METHODOLOGY AND PHILOSOPHY OF SCIENCE AND TECHNOLOGY BRIDGING ACROSS ACADEMIC CULTURES (Prague, August 5-10, 2019), Book of Abstracts, p. 418 (pdf)
Свежие доклады: Семинар Конструктивное Знание