Основные понятия и определения дисциплины

Логическое программирование.

Логи́ческое программи́рование — парадигма программирования, основанная на автоматическом доказательстве теорем, а также раздел дискретной математики, изучающий принципы логического вывода информации на основе заданных фактов и правил вывода. Логическое программирование основано на теории и аппарате математической логики с использованием математических принципов резолюций.
Самым известным языком логического программирования является Prolog.
Первым языком логического программирования был язык Planner, в котором была заложена возможность автоматического вывода результата из данных и заданных правил перебора вариантов (совокупность которых называлась планом). Planner использовался для того, чтобы понизить требования к вычислительным ресурсам (с помощью метода backtracking) и обеспечить возможность вывода фактов, без активного использования стека. Затем был разработан язык Prolog, который не требовал плана перебора вариантов и был, в этом смысле, упрощением языка Planner.
От языка Planner также произошли логические языки программирования QA-4, Popler, Conniver и QLISP. Языки программирования Mercury, Visual Prolog, Oz и Fril произошли уже от языка Prolog. На базе языка Planner было разработано также несколько альтернативных языков логического программирования, не основанных на методе поиска с возвратами (backtracking), например, Ether.

24. 
    Дедуктивные теории.
    

Дедуктивная теория считается заданной, если:

1. 
   Задан алфавит (множество) и правила образования выражений (слов) в этом алфавите.
   
2. 
   Заданы правила образования формул (правильно построенных, корректных выражений).
   
3. 
   Из множества формул некоторым способом выделено подмножество T теорем (доказуемых формул)
   

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

Задание только аксиом Задаются только аксиомы, правила вывода считаются общеизвестными.При таком задании теорем говорят, что задана полуформальная аксиоматическая теория. Примеры Геометрия Задание только правил вывода

Аксиом нет (множество аксиом пусто), задаются только правила вывода.
По сути, заданная таким образом теория — частный случай формальной, но имеет собственное название: теория естественного вывода.

25.