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

Рассматривается выразительный логический язык LF и основанное на нем исчисление. Формулы этого языка состоят из некоторых крупно-блочных структурных элементов, таких как ти́повые кванторы. Язык LF содержит всего два логических символа — $\forall$ и $\exists$, которые составляют множество логических связок языка. Рассматривается логическое исчисление JF и полные стратегии автоматического поиска выводов, основанные на единственном унарном правиле вывода. Это исчисление обладает рядом других особенностей, благодаря которым достигается уменьшение комбинаторной сложности при поиске выводов в сравнении с такими известными системами автоматического доказательства теорем (АДТ), как метод резолюций и генценовские исчисления. Рассмотрены вопросы об эффективной реализации нового исчисления в виде программной системы для автоматического доказательства теорем.