Страница публикации

Метод трансляции первопорядковых логических формул в позитивно-образованные формулы

Тип публикации: Статья в журнале

Тип материала: Текст

Авторы: Давыдов А.В., Ларионов А.А., Черкашин Е.А.

Журнал: Программные продукты и системы

Язык публикации: russian

Том: 32

Номера страниц: 197–206

Количество страниц: 10

Номер: 4

Год публикации: 2019

Отчетный год: 2019

DOI: 10.15827/⁠0236-⁠235X.128.197-⁠206

Аннотация: В статье рассматриваются логическое исчисление позитивно-образованных формул (ПОФ-исчисление) и построенный на его основе метод автоматического доказательства теорем. ПОФ-исчисление впервые появилось в работах академиков РАН С.Н. Васильева и А.К. Жерлова в результате рассмотрения и решения задач теории управления и было описано как логический формализм первого порядка. Имеются примеры описания и решения задач теории управления, эффективно (с точки зрения выразительности языка и производительности средств доказательств теорем) решенных с помощью ПОФ-исчисления, например, управление группой лифтов, наведение телескопа на центр планеты, находящейся в неполной фазе, управление мобильным роботом. ПОФ-исчисление выгодно отличается от возможностей других, логических, средств формализации предметной области и поиска логических выводов выразительностью в сочетании с компактностью представления знаний, естественным параллелизмом их обработки, крупноблочностью и меньшей комбинаторной сложностью выводов, высокой совместимостью с эвристиками и широкими возможностями для интерактивного доказательства...

Индексируется WOS: Нет

Индексируется Scopus: Нет

Индексируется УБС: Нет

Индексируется РИНЦ: Да

Индексируется ВАК: Нет

Индексируется CORE: Нет