705:
43:. A clause is true either whenever at least one of the literals that form it is true (a disjunctive clause, the most common use of the term), or when all of the literals that form it are true (a conjunctive clause, a less common use of the term). That is, it is a finite
564:
125:
325:
480:
434:
153:
257:
225:
193:
173:
76:
357:
488:
390:, where clauses are usually written as an implication in this form. More generally, the head may be a disjunction of literals. If
746:
135:
A clause can be empty (defined from an empty set of literals). The empty clause is denoted by various symbols such as
674:
383:
causes a clause to be true, and all of the literals of the body satisfy the clause, then the head must also be true.
770:
84:
265:
36:
439:
393:
780:
775:
739:
51:
of literals, depending on the context. Clauses are usually written as follows, where the symbols
630:
625:
17:
375:
of a head from a body, where the head is an arbitrary literal of the clause and the body is the
138:
666:
660:
32:
765:
693:
230:
198:
178:
158:
54:
333:
8:
732:
376:
372:
48:
44:
720:
40:
670:
387:
380:
716:
759:
360:
656:
635:
612:
559:{\displaystyle h_{1},\ldots ,h_{n}\leftarrow b_{1},\ldots ,b_{m}.}
371:
Every nonempty (disjunctive) clause is logically equivalent to an
482:
are those of its head, the clause is usually written as follows:
195:. The truth evaluation of an empty disjunctive clause is always
704:
579:
260:
330:
The truth evaluation of an empty conjunctive clause is always
712:
24:
654:
379:
of the complements of the other literals. That is, if a
491:
442:
396:
336:
268:
233:
201:
181:
161:
141:
87:
57:
558:
474:
428:
351:
319:
251:
219:
187:
167:
147:
119:
70:
757:
604:> 0, the clause is called a (Prolog) query.
740:
662:Symbolic Logic and Mechanical Theorem Proving
593:> 0, the clause is called a (Prolog) rule.
436:are the literals in the body of a clause and
305:
272:
120:{\displaystyle l_{1}\vee \cdots \vee l_{n}}
747:
733:
227:. This is justified by considering that
758:
359:. This is related to the concept of a
320:{\displaystyle (\{false,true\},\vee )}
386:This equivalence is commonly used in
699:
475:{\displaystyle h_{1},\ldots ,h_{n}}
429:{\displaystyle b_{1},\ldots ,b_{m}}
366:
35:formed from a finite collection of
13:
162:
142:
14:
792:
687:
703:
694:Clause logic related terminology
611:> 1, the clause is no longer
130:
39:(atoms or their negations) and
648:
521:
314:
269:
259:is the neutral element of the
1:
641:
578:= 0, the clause is called a (
719:. You can help Knowledge by
7:
619:
10:
797:
698:
665:. Academic Press. p.
148:{\displaystyle \emptyset }
15:
631:Disjunctive normal form
626:Conjunctive normal form
18:Clause (disambiguation)
771:Propositional calculus
715:-related article is a
560:
476:
430:
353:
321:
253:
221:
189:
169:
149:
121:
72:
657:Richard Char-Tung Lee
561:
477:
431:
354:
322:
254:
252:{\displaystyle false}
222:
220:{\displaystyle false}
190:
188:{\displaystyle \Box }
170:
168:{\displaystyle \bot }
150:
122:
73:
71:{\displaystyle l_{i}}
33:propositional formula
489:
440:
394:
352:{\displaystyle true}
334:
266:
231:
199:
179:
159:
139:
85:
55:
16:For other uses, see
655:Chang, Chin-Liang;
41:logical connectives
556:
472:
426:
349:
317:
249:
217:
185:
165:
145:
117:
68:
781:Logic programming
728:
727:
388:logic programming
788:
749:
742:
735:
707:
700:
681:
680:
652:
565:
563:
562:
557:
552:
551:
533:
532:
520:
519:
501:
500:
481:
479:
478:
473:
471:
470:
452:
451:
435:
433:
432:
427:
425:
424:
406:
405:
381:truth assignment
367:Implicative form
358:
356:
355:
350:
326:
324:
323:
318:
258:
256:
255:
250:
226:
224:
223:
218:
194:
192:
191:
186:
174:
172:
171:
166:
154:
152:
151:
146:
126:
124:
123:
118:
116:
115:
97:
96:
77:
75:
74:
69:
67:
66:
796:
795:
791:
790:
789:
787:
786:
785:
776:Predicate logic
756:
755:
754:
753:
690:
685:
684:
677:
653:
649:
644:
622:
547:
543:
528:
524:
515:
511:
496:
492:
490:
487:
486:
466:
462:
447:
443:
441:
438:
437:
420:
416:
401:
397:
395:
392:
391:
369:
335:
332:
331:
267:
264:
263:
232:
229:
228:
200:
197:
196:
180:
177:
176:
160:
157:
156:
140:
137:
136:
133:
111:
107:
92:
88:
86:
83:
82:
62:
58:
56:
53:
52:
21:
12:
11:
5:
794:
784:
783:
778:
773:
768:
752:
751:
744:
737:
729:
726:
725:
708:
697:
696:
689:
688:External links
686:
683:
682:
675:
646:
645:
643:
640:
639:
638:
633:
628:
621:
618:
617:
616:
605:
594:
583:
567:
566:
555:
550:
546:
542:
539:
536:
531:
527:
523:
518:
514:
510:
507:
504:
499:
495:
469:
465:
461:
458:
455:
450:
446:
423:
419:
415:
412:
409:
404:
400:
368:
365:
348:
345:
342:
339:
316:
313:
310:
307:
304:
301:
298:
295:
292:
289:
286:
283:
280:
277:
274:
271:
248:
245:
242:
239:
236:
216:
213:
210:
207:
204:
184:
164:
144:
132:
129:
128:
127:
114:
110:
106:
103:
100:
95:
91:
78:are literals:
65:
61:
9:
6:
4:
3:
2:
793:
782:
779:
777:
774:
772:
769:
767:
764:
763:
761:
750:
745:
743:
738:
736:
731:
730:
724:
722:
718:
714:
709:
706:
702:
701:
695:
692:
691:
678:
676:0-12-170350-9
672:
668:
664:
663:
658:
651:
647:
637:
634:
632:
629:
627:
624:
623:
614:
610:
606:
603:
599:
595:
592:
588:
584:
581:
577:
573:
569:
568:
553:
548:
544:
540:
537:
534:
529:
525:
516:
512:
508:
505:
502:
497:
493:
485:
484:
483:
467:
463:
459:
456:
453:
448:
444:
421:
417:
413:
410:
407:
402:
398:
389:
384:
382:
378:
374:
364:
362:
361:vacuous truth
346:
343:
340:
337:
328:
311:
308:
302:
299:
296:
293:
290:
287:
284:
281:
278:
275:
262:
246:
243:
240:
237:
234:
214:
211:
208:
205:
202:
182:
131:Empty clauses
112:
108:
104:
101:
98:
93:
89:
81:
80:
79:
63:
59:
50:
46:
42:
38:
34:
30:
26:
19:
721:expanding it
710:
661:
650:
608:
601:
597:
590:
586:
575:
571:
385:
370:
329:
134:
28:
22:
766:Logic stubs
636:Horn clause
377:conjunction
373:implication
49:conjunction
45:disjunction
760:Categories
642:References
538:…
522:←
506:…
457:…
411:…
312:∨
183:◻
163:⊥
143:∅
105:∨
102:⋯
99:∨
659:(1973).
620:See also
600:= 0 and
589:= 1 and
574:= 1 and
37:literals
582:) fact.
673:
580:Prolog
261:monoid
29:clause
713:logic
711:This
175:, or
31:is a
25:logic
717:stub
671:ISBN
613:Horn
27:, a
607:If
596:If
585:If
570:If
47:or
23:In
762::
669:.
667:48
363:.
327:.
155:,
748:e
741:t
734:v
723:.
679:.
615:.
609:n
602:m
598:n
591:m
587:n
576:m
572:n
554:.
549:m
545:b
541:,
535:,
530:1
526:b
517:n
513:h
509:,
503:,
498:1
494:h
468:n
464:h
460:,
454:,
449:1
445:h
422:m
418:b
414:,
408:,
403:1
399:b
347:e
344:u
341:r
338:t
315:)
309:,
306:}
303:e
300:u
297:r
294:t
291:,
288:e
285:s
282:l
279:a
276:f
273:{
270:(
247:e
244:s
241:l
238:a
235:f
215:e
212:s
209:l
206:a
203:f
113:n
109:l
94:1
90:l
64:i
60:l
20:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
