Аннотация:
Разработаны логические позитивно-образованные средства представления знаний и автоматизации дедуктивного вывода: типово-кванторные язык и исчисление. В них типовые условия кванторов могут содержать отрицания, а исчисление обладает полнотой относительно выводимости в классическом исчислении предикатов.
Ключевые слова:
представление знаний, логический вывод, автоматическое доказательство теорем.
УДК:
51.01+517.11
Поступило: 12.05.2025 После доработки: 10.06.2025 Принято к публикации: 10.06.2025
