Все выпуски

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

В работе формализуется задача оптимизации сопутствующего производства на гибких или реконфигурируемых производствах. В рассматриваемой постановке на входе задан набор обязательных изделий, требуется решить две взаимосвязанные подзадачи: 1) для каждого изделия из набора обязательных сформировать группу дополнительных изделий, которые могут быть произведены без изменения состояния производства, и 2) определить порядок переналадок производства между группами дополнительных изделий, а также «точки входа и выхода» в каждую из групп. В настоящей работе указанные подзадачи рассматриваются последовательно: первая подзадача сведена к задаче поиска клики максимального веса в ориентированном графе, вторая - к кластерной задаче коммивояжера. В ходе масштабных вычислительных экспериментов изучен выигрыш от применения эффективных современных методов решения обеих подзадач в сравнении с жадным решением, моделирующим рациональные действия человека-оператора в условиях большой размерности исходной комплексной задачи и ограниченного времени, имеющегося для ее решения.

Хорошо известно, что методы сопряженного градиента полезны при решении масштабных задач нелинейной оптимизации без ограничений. В данной работе мы рассматриваем объединение лучших свойств двух методов сопряженного градиента. В частности, мы даем новый метод сопряженного градиента, основанный на гибридизации полезных методов DY (Dai-Yuan) и HZ (Hager-Zhang). Параметры гибрида выбираются таким образом, чтобы предложенный метод удовлетворял условиям сопряженности и достаточного спуска. Показано, что новый метод сохраняет свойство глобальной сходимости двух вышеупомянутых методов. Описаны численные результаты для набора стандартных тестовых задач. Показано, что в большинстве случаев эффективность предложенного метода выше, чем у DY и HZ.