О применении композиционно-номинативных логик в инсерционном моделировании

Abstract

Рассмотрена возможность применения композиционно-номинативных логик как инструмента проведения формально-логических рассуждений в рамках технологии инсерционного моделирования. Обоснована теоретическая база такого применения – сформулирована задача проверки выполнимости формул в многосортных композиционно-номинативных логиках первого порядка. Предложен редукционный подход к ее решению.

The possibility is considered of using the composition-nominative logics as an instrument for formal reasoning in the insertion modeling technology. Theoretical foundations are established for such an application: we formulate the satisfiability problem for the first-order many-sorted composition-nominative logics and suggest a reductional approach for solving this problem.

Розглянуто можливість застосування композиційно-номінативних логік як інструменту проведення формально-логічних суджень в рамках технології інсерційного моделювання. Обґрунтовано теоретичну базу такого застосування – сформульовано задачу перевірки виконуваності формул у багатосортних композиційно-номінативних логіках предикатів першого порядку та подано редукційний підхід до її розв’язання.