662:
133:
190:
25:
66:
389:
vocabulary V { age: () β β€ // function declaration prescriptive, vote: () β πΉ // predicate declarations } theory T:V { age() < 18 β Β¬vote(). // axiom: if you are less than 18, you may not vote. prescriptive() β (age() β₯ 18 β
343:
By itself, a FO(.) knowledge base cannot be run, as it is just a "bag of information", to be used as input to various generic reasoning algorithms. Reasoning engines that use FO(.) include IDP-Z3, IDP and FOLASP. As an example, the IDP system allows generating
384:
A voting law specifies that citizens must be at least 18 years old to vote. Furthermore, if the voting law is interpreted as being prescriptive, voting is mandatory when you are over 18. This can be represented in FO(.) as follows:
462:
436:
716:
1047:
725:
372:
Definitions that specify a unique interpretation of a defined symbol, given the interpretation of its parameters. Definitions can be inductive.
329:
214:
of the topic and provide significant coverage of it beyond a mere trivial mention. If notability cannot be shown, the article is likely to be
340:, aggregates (counting, summing, maximising ... over a set), arithmetic, inductive definitions, partial functions, and intensional objects.
993:
578:
303:
285:
171:
114:
52:
149:
88:
983:
142:
211:
973:
889:
803:
702:
266:
709:
869:
846:
798:
238:
207:
1016:
826:
245:
223:
930:
96:
92:
76:
960:
252:
1011:
968:
945:
925:
831:
405:
38:
894:
775:
760:
750:
234:
1026:
1006:
836:
745:
519:
481:
200:
808:
729:
445:
419:
915:
584:
509:
219:
1021:
978:
950:
861:
841:
740:
574:
333:
215:
818:
765:
755:
566:
557:
De Cat, Broes; Bogaerts, Bart; Bruynooghe, Maurice; Janssens, Gerda; Denecker, Marc (2018).
317:
1001:
770:
694:
523:
353:
259:
487:
Such knowledge base can be turned automatically into an
Interactive Lawyer (see here)
1041:
785:
558:
642:
588:
345:
602:
622:
148:
It may require cleanup to comply with
Knowledge's content policies, particularly
851:
337:
504:
Denecker, Marc (2000). "Extending classical logic with inductive definitions".
687:
349:
153:
44:
570:
390:
vote()). // axiom: if prescriptive: if you are at least 18, you must vote }
473:
935:
879:
465:
439:
910:
514:
484:. Predicates < and β₯ are built-in and have their usual meaning.
95:
external links, and converting useful links where appropriate into
940:
920:
793:
366:
206:
Please help to demonstrate the notability of the topic by citing
874:
563:
Declarative Logic
Programming: Theory, Systems, and Applications
698:
356:, among other types of inference over a FO(.) knowledge base.
183:
126:
59:
18:
375:
Enumerations, i.e., definitions of symbols by enumeration.
559:"Predicate logic as a modeling language: The IDP system"
537:
84:
141:
A major contributor to this article appears to have a
16:
Knowledge representation computer programming language
448:
422:
992:
959:
903:
860:
817:
784:
456:
430:
79:may not follow Knowledge's policies or guidelines
506:International Conference on Computational Logic
369:, i.e., logic sentences about possible worlds,
710:
8:
53:Learn how and when to remove these messages
717:
703:
695:
363:Type, function and predicate declarations,
513:
450:
449:
447:
424:
423:
421:
304:Learn how and when to remove this message
286:Learn how and when to remove this message
172:Learn how and when to remove this message
115:Learn how and when to remove this message
496:
7:
359:FO(.) has four types of statements:
1048:Knowledge representation languages
352:between two theories and checking
348:, answering set queries, checking
14:
34:This article has multiple issues.
188:
152:. Please discuss further on the
131:
64:
23:
42:or discuss these issues on the
1:
974:Constraint logic programming
890:Knowledge Interchange Format
847:Procedural reasoning systems
804:Expert systems for mortgages
799:Connectionist expert systems
457:{\displaystyle \mathbb {B} }
431:{\displaystyle \mathbb {Z} }
201:general notability guideline
870:Attempto Controlled English
1064:
208:reliable secondary sources
197:The topic of this article
1017:Preference-based planning
736:
336:(FO). It extends FO with
199:may not meet Knowledge's
726:Knowledge representation
643:"Interactive Consultant"
387:
330:knowledge representation
961:Constraint satisfaction
571:10.1145/3191315.3191321
1012:Partial-order planning
969:Constraint programming
458:
432:
895:Web Ontology Language
837:Deductive classifiers
776:Knowledge engineering
761:Model-based reasoning
751:Commonsense reasoning
459:
433:
150:neutral point of view
1027:State space planning
1007:Multi-agent planning
809:Legal expert systems
746:Case-based reasoning
663:"Interactive Lawyer"
565:. pp. 279β323.
482:material conditional
446:
420:
85:improve this article
524:2000cs........3019D
97:footnote references
994:Automated planning
862:Ontology languages
832:Constraint solvers
454:
428:
332:language based on
203:
1035:
1034:
1022:Reactive planning
979:Local consistency
819:Reasoning systems
766:Inference engines
741:Backward chaining
334:first-order logic
314:
313:
306:
296:
295:
288:
270:
198:
182:
181:
174:
145:with its subject.
125:
124:
117:
57:
1055:
771:Proof assistants
756:Forward chaining
719:
712:
705:
696:
691:
690:
688:Official website
673:
672:
670:
669:
659:
653:
652:
650:
649:
639:
633:
632:
630:
629:
619:
613:
612:
610:
609:
599:
593:
592:
554:
548:
547:
545:
544:
534:
528:
527:
517:
501:
479:
471:
463:
461:
460:
455:
453:
437:
435:
434:
429:
427:
400:
318:computer science
309:
302:
291:
284:
280:
277:
271:
269:
228:
192:
191:
184:
177:
170:
166:
163:
157:
143:close connection
135:
134:
127:
120:
113:
109:
106:
100:
68:
67:
60:
49:
27:
26:
19:
1063:
1062:
1058:
1057:
1056:
1054:
1053:
1052:
1038:
1037:
1036:
1031:
1002:Motion planning
988:
955:
904:Theorem provers
899:
856:
827:Theorem provers
813:
780:
732:
723:
686:
685:
682:
677:
676:
667:
665:
661:
660:
656:
647:
645:
641:
640:
636:
627:
625:
621:
620:
616:
607:
605:
601:
600:
596:
581:
556:
555:
551:
542:
540:
536:
535:
531:
503:
502:
498:
493:
477:
469:
444:
443:
418:
417:
398:
392:
391:
382:
310:
299:
298:
297:
292:
281:
275:
272:
229:
227:
205:
193:
189:
178:
167:
161:
158:
147:
136:
132:
121:
110:
104:
101:
82:
73:This article's
69:
65:
28:
24:
17:
12:
11:
5:
1061:
1059:
1051:
1050:
1040:
1039:
1033:
1032:
1030:
1029:
1024:
1019:
1014:
1009:
1004:
998:
996:
990:
989:
987:
986:
981:
976:
971:
965:
963:
957:
956:
954:
953:
948:
943:
938:
933:
928:
923:
918:
913:
907:
905:
901:
900:
898:
897:
892:
887:
882:
877:
872:
866:
864:
858:
857:
855:
854:
849:
844:
842:Logic programs
839:
834:
829:
823:
821:
815:
814:
812:
811:
806:
801:
796:
790:
788:
786:Expert systems
782:
781:
779:
778:
773:
768:
763:
758:
753:
748:
743:
737:
734:
733:
724:
722:
721:
714:
707:
699:
693:
692:
681:
680:External links
678:
675:
674:
654:
634:
614:
594:
579:
549:
529:
495:
494:
492:
489:
452:
426:
394:In this code,
388:
381:
378:
377:
376:
373:
370:
364:
354:satisfiability
312:
311:
294:
293:
196:
194:
187:
180:
179:
139:
137:
130:
123:
122:
77:external links
72:
70:
63:
58:
32:
31:
29:
22:
15:
13:
10:
9:
6:
4:
3:
2:
1060:
1049:
1046:
1045:
1043:
1028:
1025:
1023:
1020:
1018:
1015:
1013:
1010:
1008:
1005:
1003:
1000:
999:
997:
995:
991:
985:
982:
980:
977:
975:
972:
970:
967:
966:
964:
962:
958:
952:
949:
947:
944:
942:
939:
937:
934:
932:
929:
927:
924:
922:
919:
917:
914:
912:
909:
908:
906:
902:
896:
893:
891:
888:
886:
883:
881:
878:
876:
873:
871:
868:
867:
865:
863:
859:
853:
850:
848:
845:
843:
840:
838:
835:
833:
830:
828:
825:
824:
822:
820:
816:
810:
807:
805:
802:
800:
797:
795:
792:
791:
789:
787:
783:
777:
774:
772:
769:
767:
764:
762:
759:
757:
754:
752:
749:
747:
744:
742:
739:
738:
735:
731:
727:
720:
715:
713:
708:
706:
701:
700:
697:
689:
684:
683:
679:
664:
658:
655:
644:
638:
635:
624:
618:
615:
604:
598:
595:
590:
586:
582:
580:9781970001990
576:
572:
568:
564:
560:
553:
550:
539:
533:
530:
525:
521:
516:
511:
507:
500:
497:
490:
488:
485:
483:
475:
467:
441:
415:
411:
407:
403:
397:
386:
379:
374:
371:
368:
365:
362:
361:
360:
357:
355:
351:
347:
341:
339:
335:
331:
327:
323:
319:
308:
305:
290:
287:
279:
276:February 2022
268:
265:
261:
258:
254:
251:
247:
244:
240:
237: β
236:
232:
231:Find sources:
225:
221:
217:
213:
209:
202:
195:
186:
185:
176:
173:
165:
162:February 2022
155:
151:
146:
144:
138:
129:
128:
119:
116:
108:
98:
94:
93:inappropriate
90:
86:
80:
78:
71:
62:
61:
56:
54:
47:
46:
41:
40:
35:
30:
21:
20:
884:
852:Rule engines
666:. Retrieved
657:
646:. Retrieved
637:
626:. Retrieved
617:
606:. Retrieved
597:
562:
552:
541:. Retrieved
532:
505:
499:
486:
464:denotes the
413:
409:
404:indicates a
401:
395:
393:
383:
358:
342:
325:
321:
315:
300:
282:
273:
263:
256:
249:
242:
230:
168:
159:
140:
111:
105:January 2022
102:
87:by removing
74:
50:
43:
37:
36:Please help
33:
984:SMT solvers
508:: 703β717.
212:independent
668:2022-02-01
648:2022-02-01
628:2022-02-01
608:2022-02-01
543:2022-02-01
515:cs/0003019
491:References
350:entailment
246:newspapers
220:redirected
39:improve it
730:reasoning
210:that are
154:talk page
89:excessive
45:talk page
1042:Category
623:"FOLASP"
538:"IDP-Z3"
480:denotes
474:negation
472:denotes
466:booleans
440:integers
438:denotes
406:function
324:(a.k.a.
936:Prover9
931:Paradox
880:F-logic
589:3866665
520:Bibcode
380:Example
328:) is a
260:scholar
235:"FO(.)"
224:deleted
83:Please
75:use of
911:CARINE
587:
577:
476:, and
367:Axioms
346:models
326:FO-dot
262:
255:
248:
241:
233:
216:merged
941:SPASS
926:Otter
921:Nqthm
885:FO(.)
794:CLIPS
603:"IDP"
585:S2CID
510:arXiv
408:from
338:types
322:FO(.)
267:JSTOR
253:books
222:, or
875:CycL
728:and
575:ISBN
239:news
946:TPS
567:doi
412:to
316:In
91:or
1044::
951:Z3
583:.
573:.
561:.
518:.
468:,
442:,
416:,
320:,
218:,
48:.
916:E
718:e
711:t
704:v
671:.
651:.
631:.
611:.
591:.
569::
546:.
526:.
522::
512::
478:β
470:Β¬
451:B
425:Z
414:B
410:A
402:B
399:β
396:A
307:)
301:(
289:)
283:(
278:)
274:(
264:Β·
257:Β·
250:Β·
243:Β·
226:.
204:.
175:)
169:(
164:)
160:(
156:.
118:)
112:(
107:)
103:(
99:.
81:.
55:)
51:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.