Пункт (логика) - Clause (logic)

В логике , А пункт является выражение формируется из конечного набора литералов (атомов или их отрицаний). Предложение истинно либо тогда, когда хотя бы один из образующих его литералов истинен (дизъюнктивное предложение, наиболее распространенное использование термина), либо когда все литералы, образующие его, истинны (конъюнктивное предложение, менее распространенное использование термина). То есть это конечная дизъюнкция или соединение литералов, в зависимости от контекста. Пункты обычно записываются следующим образом, где символы являются литералами: ${\ displaystyle l_ {i}}$

{\ Displaystyle l_ {1} \ vee \ cdots \ vee l_ {п}}

Пустые предложения

Предложение может быть пустым (определенным из пустого набора литералов). Пустой пункт обозначается различными символами , такими как , , или . Оценка истинности пустого дизъюнктивного предложения всегда . Это оправдано тем, что это нейтральный элемент моноида . ${\ displaystyle \ emptyset}$ ${\ displaystyle \ bot}$ ${\ displaystyle \ Box}$ ${\ displaystyle false}$ ${\ displaystyle false}$ ${\ displaystyle (\ {ложь, истина \}, \ vee)}$

Оценка истинности пустого конъюнктивного предложения всегда . Это связано с концепцией пустой истины . ${\ displaystyle true}$

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

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

Эта эквивалентность обычно используется в логическом программировании , где предложения обычно записываются как импликация в этой форме. В более общем смысле, голова может быть дизъюнкцией литералов. Если это литералы в теле предложения и литералы в его голове, предложение обычно записывается следующим образом: ${\ displaystyle b_ {1}, \ ldots, b_ {m}}$ ${\ displaystyle h_ {1}, \ ldots, h_ {n}}$