Аннотация:
В логике первого порядка осмысленна следующая задача: для заданной
теории и формулы, называемой в этом контексте запросом, найти все
такие константы, называемые ответами на данный запрос относительно
данной теории, для которых результат подстановки этих констант в
формулу вместо свободных переменных следует из теории. Для некоторых
теорий эту задачу можно решить при помощи построения
так называемого переписывания запроса относительно теории — формулы
первого порядка, позволяющей находить ответы на данный запрос
относительно данной теории. Доклад посвящен связи между построением
переписывания запроса относительно теории и построением булевых формул
и схем для определенных булевых функций и получению с использованием
этой техники экспоненциальных нижних оценок длины переписывания.
|