- Автоматизированная поддержка рассуждений для Standpoint-OWL 2 (arXiv)
Автор: Флориан Эммрих, Лусия Гомес Альварес, Ханнес Штрасс.
Аннотация: Мы представляем инструмент для моделирования и рассуждений со знаниями с различных (и, возможно, конфликтующих) точек зрения. Теоретические основы обеспечиваются расширением базовой логики точками зрения в соответствии с недавно введенным формализмом, который мы также помним. Инструмент работает путем перевода расширенной точки зрения версии логики описания SROIQ в ее простую (то есть классическую) версию. Существующие механизмы рассуждений можно затем напрямую использовать для обеспечения автоматизированной поддержки рассуждений о различных точках зрения.
2.Вероятностные соотношения для моделирования эпистемической и алеаторической неопределенности: ее семантика и автоматизированные рассуждения с доказательством теорем (arXiv)
Автор: Канфэн Е, Джим Вудкок, Саймон Фостер.
Аннотация :: Вероятностное программирование — это парадигма программирования, которая сочетает в себе общее компьютерное программирование, статистический вывод и формальную семантику, чтобы помочь системам принимать решения в условиях неопределенности. Вероятностные программы распространены повсеместно и, как считается, оказывают большое влияние на машинный интеллект. Хотя многие вероятностные алгоритмы использовались на практике в различных областях, их автоматическая проверка, основанная на формальной семантике, все еще остается относительно новой областью исследований. В последние два десятилетия он вызывает большой интерес. Однако многие проблемы все еще остаются. Наша работа, представленная в этой статье, вероятностные отношения, делает шаг к нашему видению решения этих проблем. Наша работа, по сути, основана на предикативно-вероятностном программировании Хенера, но есть несколько препятствий для более широкого внедрения его работы. Наш вклад здесь включает (1) формализацию его синтаксиса и семантики путем введения нотации скобок Айверсона для отделения отношений от арифметики; (2) формализация отношений с использованием унифицирующих теорий программирования (UTP) и вероятностей вне скобок с помощью суммирования по топологическому пространству действительных чисел; (3) конструктивная семантика вероятностных петель с использованием теоремы Клини о неподвижной точке; (4) обогащение его семантики от распределений к субраспределениям и суперраспределениям, чтобы иметь дело с конструктивной семантикой; (5) единственная теорема о неподвижной точке, значительно упрощающая рассуждения о вероятностных петлях; и (6) механизация нашей теории в Isabelle/UTP, реализация UTP в Isabelle/HOL для автоматизированного рассуждения с использованием доказательства теорем. Мы демонстрируем шесть интересных примеров, и среди них один касается локализации роботов, два — проблемы классификации в машинном обучении и два содержат вероятностные циклы.
