Любит (х, конфеты)àсластена (х).

Таблица истинности импликации:

Свойства импликации:

П1: «Импликация А à В ложна,

когда посылка А истинна, а следствие В — ложно».

П2: «Импликация А à В истинна,

когда истинно следствие либо ложны и посылка и следствие».

Общий закон логического вывода был указан Аристотелем — основателем логики как научной дисциплины — и назван modus ponens:

Если из А следует В и посылка А истинна, то истинно и следствие В.

Примеры логического вывода:

«Если идет дождь, то на улице мокро».

Аристотелем данная формулировка закона логического вывода была дана на языке исчисления высказываний. В таком виде она содержится во всех учебниках по логике и учебниках по математической логике.

В исчислении предикатов этот закон сохраняет свою силу. Однако в предикатной форме закон логического вывода превращается в конструктивную процедуру вывода новых сведений из имеющихся конкретных фактов и правил вывода.

Первый принцип логического вывода:

Данная процедура вывода позволяет вывести суждение В(с) из конкретного факта А(с) и правила А(х) à В(х). Пример логического вывода:

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

Этим свойством и этими законами логического вывода могут пользоваться не только люди — они применяются в механизмах автоматического доказательства теорем, заложенных в современных системах искусственного интеллекта.

Принцип вывода отрицаний — второй общий принцип логического вывода:

Данная процедура из отрицания следствия не В(с) на основании правила вывода А(х) à В(х) позволяет сделать заключение о невыполнении предпосылки не А(с).

Примеры логического вывода из отрицаний:

Данный принцип также представляет конструктивную процедуру вывода новых сведений — отрицаний предпосылок не А(с) при нарушении следствий не В(с) для заданного правила А(х) à В(х).

Приведенные принципы и законы логического вывода и заложены в современные модели систем искусственного интеллекта. В частности, они заложены в механизмы системы логического программирования Пролог, которая в 90-х годах была принята японским правительством в основу проекта нового поколения ЭВМ.