Все выпуски

Эта статья представляет подход к дедуктивному синтезу программ с использованием секвенциального подхода Генцена в рамках логического программирования. Используя секвенциальное исчисление как формальную систему для структурированного логического вывода, наш метод автоматизирует вывод доказуемо корректных программ из спецификаций, выраженных в логике предикатов первого порядка без отрицаний. Мы формализуем синтаксис и семантику секвенциального исчисления, реализуя его основные правила вывода (правила введения и удаления) в виде предикатов в логическом программировании для обеспечения масштабируемого синтеза. Практические примеры демонстрируют преобразование логических спецификаций в исполняемые программы. Подход обеспечивает формальную корректность через конструктивную семантику реализуемости Клини, при этом синтезированные программы работают в субрекурсивном языке, чтобы гарантировать завершение вычислительных процессов. Мы оцениваем сильные стороны метода, включая его надежность для систем с критической безопасностью, и его ограничения, такие как вычислительная сложность для неограниченных конструкций. В сравнении с синтезом, управляемым ИИ, наш подход ставит на первое место формальные гарантии, дополняя современные тенденции. Направления будущих исследований включают оптимизацию вычислительной эффективности и расширение применимости к сложным задачам реального мира.

В данной работе рассматривается подход к программированию, основанный на использовании параметризованных грамматик. Понятия этих грамматик снабжены параметрами, которые также могут быть объектами грамматик. Такие грамматики являются довольно мощным инструментом, их предлагается использовать для формулирования постановок задач преобразования лингвистических данных. Эти грамматики можно использовать непосредственно для обработки информации, но это может оказаться не эффективным. Поэтому выделяется специальный эффективный в применении класс таких грамматик. Предлагается специальная система однозначных (функциональных) параметризованных грамматик, которую можно использовать как эффективный язык программирования лингвистических задач. Описываются идеи дедуктивного синтеза программ в этой системе из постановок задач в общих параметризованных грамматиках с помощью логического вывода с перспективой последующей автоматизации. Демонстрируется практическое применение предложенного инструмента на примерах обработки логических формул и решения других задач. Эта работа продолжает идеи Валентина Турчина в области языка РЕФАЛ.