Правила вывода исчисления предикатов первого порядка
Типичное правило вывода имеет следующий вид: из утверждений а ^ b и b ^ с можно получить утверждение а ^ с.
Формально же данное правило вывода записывается следующим образом:
Правила вывода позволяют строить набор всех утверждений, которые могут быть произведены или доказаны на основе исходного набора утверждений: такие утверждения имеют истинные значения, если верны оригинальные утверждения. Например, первые пять утверждений о млекопитающих (из предыдущего подраздела) позволяют получать следующие утверждения: ноги (лошадь, 4). ноги (человек, 2). руки (человек, 2).
Заявленные на языке логики, эти три утверждения становятся теоремами, полученными из первых пяти утверждений (или аксиом) о млекопитающих. Заметьте, что доказательство утверждений (на базе исходных утверждений) может рассматриваться как вычисление числа рук и ног лошади или человека.
Таким образом, набор исходных утверждений задает потенциальные вычисления всех логических последствий данных утверждений.В этом заключается сущность логического программирования: набор утверждений принимается в качестве аксиом, а желаемый факт производится путем автоматического применения к аксиомам правил вывода. Таким образом, следует определить:
Язык логического программирования — это система для записи логических утверждений вместе с определенными алгоритмами для реализации правил вывода.
Набор логических утверждений в качестве аксиом может рассматриваться как логическая программа, а утверждения о производстве результатов считаются вводами, которые инициируют вычисления.
Такие вводы предоставляются программистами и называются запросами или целями. Например, для набора аксиом о млекопитающих, при желании узнать, сколько ног у человека, мы обеспечили бы следующий запрос: Существует ли такое значение у, которое равно числу ног у человека?или, в терминах исчисления предикатов: there exists у, ноги (человек, y)?
а система ответила бы примерно так: да: у 2
652 |
Глава 21. Логическое программирование |
Поэтому системы логического программирования иногда называют дедуктивными базами данных, то есть базами данных, состоящими из набора утверждений и дедуктивной системы, которая может отвечать на запросы. Заметьте, что они отличаются от обычных баз данных, так как содержат не только факты, такие как млекопитающее (человек) или natural (0), но также и более сложные утверждения, такие как natural(x) natural (successor (x)). Кроме того, система может отвечать не только на запросы по фактам, но и на запросы, требующие логических выводов. |