Язык предикатов

Теоретические исследования математических моделей вычислений играют важную роль в формировании технологии использования компьютерной техники. Каждая такая модель вносит свой вклад в реальную технологию. Развитие технологии в обход теоретических исследований часто приводит к неуклюжим, трудным для восприятия и, в конечном счете, малопроизводительным видам деятельности.

Исследования универсальных методов доказательства в рамках логики предикатов дают повод для разработки на их основе новых языков программирования. Опыты, проведенные в 70-х годах прошлого века, показали перспективность использования этих методов в реальных технологиях автоматической переработки информации.

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

Формулы языка предикатов строятся из предикатных и функциональных символов с помощью логических связок, кванторов и некоторых вспомогательных символов. Набор предикатных и функциональных символов заранее не фиксируется, а выбирается из содержательных соображений, связанных с желанием строить высказывания о тех или иных объектах или их свойствах и отношениях между ними. С каждым предикатным символом связывается натуральное число, его арность (число аргументов).

"Строительные материалы", из которых конструируются формулы и предложения языка предикатов:

Логические связки и кванторы:
Символы для конструирования переменных: по традиции латинская буква и (штрих). Отдельную букву или с несколькими штрихами будем считать переменной. Делая такой выбор, мы подчеркиваем то обстоятельство, что используем всего два символа для образования любого конечного множества переменных. На практике, конечно, это неудобно, поэтому используются и другие символы, возможно, с индексами.

Содержание Назад Вперед