Кіріспе

Логикада клауза – бұл сөзбе-сөздердің (атомдар немесе олардың жоққа шығарылулары) және логикалық байланыстардың шекті жиынтығынан құрылған логикалық формула. Клауза, егер оны құрайтын сөзбе-сөздердің кем дегенде біреуі дұрыс болса (дизъюнктивті клауза, терминнің ең көп қолданылатын түрі) немесе оны құрайтын барлық сөзбе-сөздер дұрыс болса (конъюнктивті клауза, терминнің сирек қолданылатын түрі) дұрыс болады. Яғни, бұл сөзбе-сөздердің шекті ажырауы немесе бірігуі, контекстке байланысты. Клаузалар әдетте мына түрде жазылады, онда символдар сөзбе-сөздерді білдіреді:

Бос тармақтар

Клауза бос болуы мүмкін (бос литералдар жиынтығынан анықталады). Бос клауза әр түрлі символдармен белгіленеді, мысалы , , немесе . Бос дизъюнктивті клаузаның шындық мәні әрқашан болады. Бұл моноидтың бейтарап элементі екенін ескере отырып негізделген. Бос конъюнктивті клаузаның шындық мәні әрқашан болады. Бұл бос шындық концепциясымен байланысты.

Нысандылық форма

Кез келген бос емес (дизъюнктивті) клауза логикалық тұрғыдан денеден бастаудың салдарына тең, мұнда бастау клаузаның кез келген мәтіні болып табылады, ал дене – басқа мәтіндердің инверсияларының конъюнкциясы болып табылады. Яғни, егер шындыққа тағайындау клаузаны шын етсе және дененің барлық мәтіндері клаузаны қанағаттандырса, онда бастау да шын болуы керек. Бұл эквиваленттілік логикалық бағдарламалауда кеңінен қолданылады, онда клаузалар әдетте осы формада импликация ретінде жазылады. Жалпырақ айтқанда, бастау мәтіндердің дизъюнкциясы болуы мүмкін. Егер клауза денесіндегі мәтіндер және басындағы мәтіндер болса, онда клауза әдетте былай жазылады: Егер n = 1 және m = 0 болса, клауза (Prolog) фактісі деп аталады. Егер n = 1 және m > 0 болса, клауза (Prolog) ережесі деп аталады. Егер n = 0 және m > 0 болса, клауза (Prolog) сұранысы деп аталады. Егер n > 1 болса, клауза енді Horn клаузасы емес.