Введение

В логике, клауза — это пропозициональная формула, образованная из конечного набора литералов (атомов или их отрицаний) и логических связок. Клауза истинна, если хотя бы один из литералов, входящих в её состав, истинен (дизъюнктивная клауза, наиболее распространенное употребление термина), или если все литералы, входящие в её состав, истинны (конъюнктивная клауза, менее распространенное употребление термина). Иными словами, это конечная дизъюнкция или конъюнкция литералов, в зависимости от контекста. Клаузы обычно записываются следующим образом, где символы являются литералами:

Пустые пункты

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

Имплицитная форма

Каждая непустая (дизъюнктивная) клауза логически эквивалентна импликации, где голова – произвольный литерал клаузы, а тело – конъюнкция отрицаний остальных литералов. То есть, если при задании значений истинности клауза становится истинной, и все литералы тела удовлетворяют клаузе, то голова также должна быть истинной. Эта эквивалентность широко используется в логическом программировании, где клаузы обычно записываются в виде импликации. В более общем случае, голова может быть дизъюнкцией литералов. Если – литералы в теле клаузы, а – литералы в её голове, то клауза обычно записывается следующим образом:

Если n = 1 и m = 0, клауза называется (Prolog) фактом. Если n = 1 и m > 0, клауза называется (Prolog) правилом. Если n = 0 и m > 0, клауза называется (Prolog) запросом. Если n > 1, клауза перестаёт быть клаузой Хорна.