-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathao_bfo_dolce_mappings_v0.4.tex
2435 lines (1966 loc) · 215 KB
/
ao_bfo_dolce_mappings_v0.4.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
% PLEASE USE THIS FILE AS A TEMPLATE
% Check file iosart2x.tex for more examples
%
%%%% Journal title (\documentclass optional parameter)
%% Applied Ontology (ao)
%%%% IOS Press
%%%% Latex 2e
% add. options: [seceqn,secthm,crcready,onecolumn]
\documentclass[ao]{iosart2x}
\usepackage[T1]{fontenc}
\usepackage{times}%
\usepackage{array}
\usepackage{natbib}
\usepackage{rawfonts}
\usepackage{stmaryrd}
\usepackage{amsmath,txfonts,bbm}
%dsserif}
%mathbbol}
%\usepackage[mathscr]{eucal}
%\usepackage{phonetic} % added to get an upside-down iota (Russell's definite description) \riota.
% incompatibile con \usepackage{mathptmx}
\usepackage{graphicx}
\usepackage{calc}
\usepackage{mathptmx}
\usepackage{graphicx,amssymb,verbatim,color,hyperref}
\usepackage[all]{xy}
\usepackage{multicol}
\usepackage{enumerate}
\usepackage{pdflscape}
\usepackage{float}%exact placement of floats (things inside a begin{})
\usepackage{listings}
\usepackage{nameref}
\usepackage{hyperref}
\lstset{% general command to set parameter(s)
basicstyle=\tiny}%, % print whole listing small
% keywordstyle=\color{black}\bfseries\underbar,
% % underlined bold black keywords
% identifierstyle=, % nothing happens
% commentstyle=\color{white}, % white comments
% stringstyle=\ttfamily, % typewriter type for strings
% showstringspaces=false} % no special string spaces
%\usepackage{textcomp}
%\newlength{\mylength}
% \newcommand{\proofdbth}[2]{#1 - Proof of Theorem \refdbth{#2}}:}
% \newcommand{\proofdolceth}[2]{#1 - Proof of Theorem \refdolceth{#2}}:}
\newcommand{\proofdbth}[2]{\textbf{Proof of Theorem \refdbth{#2}}}
\newcommand{\proofbdth}[1]{\textbf{Proof of Theorem \refbdth{#1}}}
\newcommand{\proofdolceth}[2]{\textbf{Proof of Theorem \refdolceth{#2}}}
%\newcommand{\proofdolceth}[2]{\subsubsection{Proof of Theorem \refdolceth{#2}}}
\newcommand{\counterExampleDB}[1]{\noindent Counter model to \refdbth{#1}}
\newcommand{\counterExampleBD}[1]{\noindent Counter model to \refbdth{#1}}
%\renewcommand{\familydefault}{cmss}
%\fontencoding{TS1}
%\renewcommand{\sfdefault}{pcr}
\newcommand{\nb}[1]{\textcolor{red}{$|$}\marginpar{\hspace*{-0cm}\parbox{20mm}{\scriptsize\raggedright\textcolor{red}{#1}}}}
%\newcommand{\nb}[1]{}
% COUNTERS
% newcommand for list ox formula environment
\newcommand{\bflist}{\begin{list}{}{\setlength{\topsep}{2mm}\setlength{\parsep}{0mm}\setlength{\leftmargin}{9.2mm}\setlength{\labelwidth}{8mm}}}
\newcommand{\eflist}{\end{list}}
\newcommand{\bflistnoind}{\begin{list}{}{\setlength{\topsep}{2mm}\setlength{\parsep}{0mm}\setlength{\leftmargin}{0mm}\setlength{\labelwidth}{8mm}}}
\newcommand{\eflistnoind}{\end{list}}
% newcommand for labels of axioms, definitions and formulae
\newcommand{\bfoAxLabel}{\textrm{a$_\texttt{b}$}}
\newcommand{\bfoDefLabel}{\textrm{d$_\texttt{b}$}}
\newcommand{\bfoFmLabel}{\textrm{f$_\texttt{b}$}}
\newcommand{\bfoThrLabel}{\textrm{t$_\texttt{b}$}}
% newcommand for labels of axioms, definitions and formulae
\newcommand{\dolceAxLabel}{\textrm{a$_\texttt{d}$}}
\newcommand{\dolceAxLabelscript}{\scriptsize \textrm{a$_\texttt{d}$}}
\newcommand{\dolceDefLabel}{\textrm{d$_\texttt{d}$}}
\newcommand{\dolceFmLabel}{\textrm{f$_\texttt{d}$}}
\newcommand{\dolceThrLabel}{\textrm{t$_\texttt{d}$}}
\newcommand{\dbDefLabel}{\textrm{d$_\texttt{db}$}}
\newcommand{\dbThrLabel}{\textrm{t$_\texttt{db}$}}
\newcommand{\dbAxLabel}{\textrm{a}$_\texttt{db}$}
\newcommand{\dbLemLabel}{\textrm{l$_\texttt{db}$}}
\newcommand{\bdDefLabel}{\textrm{d$_\texttt{bd}$}}
\newcommand{\bdThrLabel}{\textrm{t$_\texttt{bd}$}}
\newcommand{\bdAxLabel}{\textrm{a}$_\texttt{bd}$}
%\newcommand{\dbDefLabel}{\textrm{d\raisebox{-2.5pt}{$\hspace{0.8pt}^\triangleright\hspace{-0.3pt}$}bd}}
%\newcommand{\dbThrLabel}{\textrm{d\raisebox{-2.5pt}{$\hspace{0.8pt}^\triangleright\hspace{-0.3pt}$}bt}}
%\newcommand{\dbAxLabel}{\textrm{d\raisebox{-2.5pt}{$\hspace{0.8pt}^\triangleright\hspace{-0.3pt}$}ba}}
% counter and newcommand for numbering formulas of BFO
\newcounter{cntaxb}
\newcommand{\bfoax}[1]{\refstepcounter{cntaxb}\begin{small}{\bf \bfoAxLabel\thecntaxb\label{#1}}\end{small}}
\newcounter{cntdefb}
\newcommand{\bfodf}[1]{\refstepcounter{cntdefb}\begin{small}{\bf \bfoDefLabel\thecntdefb\label{#1}}\end{small}}
\newcounter{cntfmb}
\newcommand{\bfofm}[1]{\refstepcounter{cntfmb}\begin{small}{\bf \bfoFmLabel\thecntfmb\label{#1}}\end{small}}
\newcounter{cntthrb}
\newcommand{\bfoth}[1]{\refstepcounter{cntthrb}\begin{small}{\bf \bfoThrLabel\thecntthrb\label{#1}}\end{small}}
% counter and newcommand for numbering formulas of DOLCE
\newcounter{cntax}
\newcommand{\dolceax}[1]{\refstepcounter{cntax}\begin{small}{\bf \dolceAxLabelscript\thecntax\label{#1}}\end{small}}
\newcounter{cntdef}
\newcommand{\dolcedf}[1]{\refstepcounter{cntdef}\begin{small}{\bf \dolceDefLabel\thecntdef\label{#1}}\end{small}}
\newcounter{cntfm}
\newcommand{\dolcefm}[1]{\refstepcounter{cntfm}\begin{small}{\bf \dolceFmLabel\thecntfm\label{#1}}\end{small}}
\newcounter{cntthr}
\newcommand{\dolceth}[1]{\refstepcounter{cntthr}\begin{small}{\bf \dolceThrLabel\thecntthr\label{#1}}\end{small}}
% counter and newcommand for numbering mappings DOLCE => BFO
\newcounter{cntdbdf}
\newcommand{\dbdf}[1]{\refstepcounter{cntdbdf}\begin{small}{\bf \dbDefLabel\thecntdbdf\label{#1}}\end{small}}
\newcounter{cntdbax}
\newcommand{\dbax}[1]{\refstepcounter{cntdbax}\begin{small}{\bf \dbAxLabel\thecntdbax\label{#1}}\end{small}}
\newcounter{cntdbth}
\newcommand{\dbth}[1]{\refstepcounter{cntdbth}\begin{small}{\bf \dbThrLabel\thecntdbth\label{#1}}\end{small}}
\newcounter{cntdblm}
\newcommand{\dblm}[1]{\refstepcounter{cntdblm}\begin{small}{\bf \dbLemLabel\thecntdblm\label{#1}}\end{small}}
% counter and newcommand for numbering mappings BFO => DOLCE
\newcounter{cntbddf}
\newcommand{\bddf}[1]{\refstepcounter{cntbddf}\begin{small}{\bf \bdDefLabel\thecntbddf\label{#1}}\end{small}}
\newcounter{cntbdax}
\newcommand{\bdax}[1]{\refstepcounter{cntbdax}\begin{small}{\bf \bdAxLabel\thecntbdax\label{#1}}\end{small}}
\newcounter{cntbdth}
\newcommand{\bdth}[1]{\refstepcounter{cntbdth}\begin{small}{\bf \bdThrLabel\thecntbdth\label{#1}}\end{small}}
\newcommand{\refdolceax}[1]{({\dolceAxLabel}\ref{#1})}
\newcommand{\refdolcedf}[1]{({\dolceDefLabel}\ref{#1})}
\newcommand{\refdolcefm}[1]{({\dolceFmLabel}\ref{#1})}
\newcommand{\refdolceth}[1]{({\dolceThrLabel}\ref{#1})}
\newcommand{\refbfoax}[1]{({\bfoAxLabel}\ref{#1})}
\newcommand{\refbfodf}[1]{({\bfoDefLabel}\ref{#1})}
\newcommand{\refbfofm}[1]{({\bfoFmLabel}\ref{#1})}
\newcommand{\refbfoth}[1]{({\bfoThrLabel}\ref{#1})}
\newcommand{\refdbax}[1]{({\dbAxLabel}\ref{#1})}
\newcommand{\refdbdf}[1]{({\dbDefLabel}\ref{#1})}
\newcommand{\refdbth}[1]{({\dbThrLabel}\ref{#1})}
\newcommand{\refdblm}[1]{({\dbLemLabel}\ref{#1})}
\newcommand{\refbdax}[1]{({\bdAxLabel}\ref{#1})}
\newcommand{\refbddf}[1]{({\bdDefLabel}\ref{#1})}
\newcommand{\refbdth}[1]{({\bdThrLabel}\ref{#1})}
\newcommand{\ty}[1]{\textsc{#1}}
\newcommand{\pr}[1]{\mathtt{#1}}
\newcommand{\prbfo}[1]{{\textit{{#1}}}}
%\newcommand{\prbfo}[1]{\mathbb{#1}}
\newcommand{\cn}[1]{\mathtt{#1}}
\newcommand{\ifif}{\leftrightarrow}
\newcommand\textequal{%
\rule[.08ex]{5pt}{0.35pt}\llap{\rule[.78ex]{5pt}{0.35pt}}}
\newcommand{\sdef}{{\hspace{1.5pt}:\hspace{-2.5pt}\textequal\hspace{3pt}}}
\newcommand{\dolce}{{\textsc{dolce}}}
\newcommand{\dolceorig}{{\textsc{dolce-d{\footnotesize 18}}}}
\newcommand{\bfo}{{\textsc{bfo}}}
\newcommand{\bfocl}{{\textsc{bfo-cl}}}
\newcommand{\emmo}{{\textsc{emmo}}}
% THEORIES AND MAPPINGS
\newcommand {\thdolce} {\ensuremath{\mathfrak{D}}}
\newcommand {\thbfo} {\ensuremath{\mathfrak{B}}}
\newcommand {\dbmap} {\ensuremath{\mathfrak{M}_\texttt{db}}}
\newcommand {\bdmap} {\ensuremath{\mathfrak{M}_\texttt{bd}}}
\newcommand {\thbfobdmap} {\ensuremath{\mathfrak{B}_\texttt{d}}}
\newcommand {\thdolcedbmap} {\ensuremath{\mathfrak{D}_\texttt{b}}}
% CATEGORIES OF DOLCE
% Abstract
\newcommand {\ABdcat} {\textsc{ab}}
% Abstract Quality
\newcommand {\AQdcat} {\textsc{aq}}
% Abstract Region
\newcommand {\ARdcat} {\textsc{ar}}
% Achievement
\newcommand {\ACHdcat} {\textsc{ach}}
% Accomplishment
\newcommand {\ACCdcat} {\textsc{acc}}
% Agentive Physical Object
\newcommand {\APOdcat} {\textsc{apo}}
% Agentive Social Object
\newcommand {\ASOdcat} {\textsc{aso}}
% Amount of Matter
\newcommand {\Mdcat} {\textsc{m}}
% Arbitrary Sum
\newcommand {\ASdcat} {\textsc{as}}
% Endurant
\newcommand {\EDdcat} {\textsc{ed}}
% Event
\newcommand {\EVdcat} {\textsc{ev}}
% Feature
\newcommand {\Fdcat} {\textsc{f}}
% Mental Object
\newcommand {\MOBdcat} {\textsc{mob}}
% Non-agentive Physical Object
\newcommand {\NAPOdcat} {\textsc{napo}}
% Non-agentive Social Object
\newcommand {\NASOdcat} {\textsc{naso}}
% Non-physical Endurant
\newcommand {\NPEDdcat} {\textsc{nped}}
% Non-physical Object
\newcommand {\NPOBdcat} {\textsc{npob}}
% Particular
\newcommand {\PTdcat} {\textsc{pt}}
% Perdurant
\newcommand {\PDdcat} {\textsc{pd}}
% Physical Endurant
\newcommand {\PEDdcat} {\textsc{ped}}
% Physical Object
\newcommand {\POBdcat} {\textsc{pob}}
% Physical Quality
\newcommand {\PQdcat} {\textsc{pq}}
% Physical Region
\newcommand {\PRdcat} {\textsc{pr}}
% Process
\newcommand {\PROdcat} {\textsc{pro}}
% Quality
\newcommand {\Qdcat} {\textsc{q}}
% Region
\newcommand {\Rdcat} {\textsc{r}}
% Social Agent
\newcommand {\SAGdcat} {\textsc{sag}}
% Social Object
\newcommand {\SOBdcat} {\textsc{sob}}
% Society
\newcommand {\SCdcat} {\textsc{sc}}
% Space Region
\newcommand {\Sdcat} {\textsc{s}}
% Spatial Location
\newcommand {\SLdcat} {\textsc{sl}}
% State
\newcommand {\STdcat} {\textsc{st}}
% Stative
\newcommand {\STVdcat} {\textsc{stv}}
% Temporal Location
\newcommand {\TLdcat} {\textsc{tl}}
% Temporal Quality
\newcommand {\TQdcat} {\textsc{tq}}
% Temporal Region
\newcommand {\TRdcat} {\textsc{tr}}
% Time Interval
\newcommand {\Tdcat} {\textsc{t}}
%Essential quality
\newcommand {\EQdcat} {\textrm{e}\textsc{q}}
% RELATIONS OF DOLCE
% Rigid
\newcommand {\RGd} {\ensuremath{\pr{RG}}}
% Non-empty
\newcommand {\NEPd} {\ensuremath{\pr{NEP}}}
% Disjoint
\newcommand {\DJd} {\ensuremath{\pr{DJ}}}
% Subsumes
\newcommand {\SBd} {\ensuremath{\pr{SB}}}
% Equal
\newcommand {\EQd} {\ensuremath{\pr{EQ}}}
% Properly Subsumes
\newcommand {\PSBd} {\ensuremath{\pr{PSB}}}
% Leaf
\newcommand {\Ld} {\ensuremath{\pr{L}}}
\newcommand {\SBLd} {\ensuremath{\pr{SBL}}}
\newcommand {\PSBLd} {\ensuremath{\pr{PSBL}}}
\newcommand {\LxXd} {\ensuremath{\pr{L}_X}}
\newcommand {\SBLxXd} {\ensuremath{\pr{SBL}_X}}
\newcommand {\PSBLxXd} {\ensuremath{\pr{PSBL}_X}}
\newcommand {\PTd} {\ensuremath{\pr{PT}}}
\newcommand {\TMPd} {\ensuremath{\pr{TMP}}}
\newcommand {\TPd} {\ensuremath{\pr{tP}}}
\newcommand {\TPPd} {\ensuremath{\pr{tPP}}}
\newcommand {\TOd} {\ensuremath{\pr{tO}}}
\newcommand {\TATd} {\ensuremath{\pr{tAT}}}
\newcommand {\TATPd} {\ensuremath{\pr{tATP}}}
\newcommand {\TSUMd} {\ensuremath{\pr{tSUM}}}
\newcommand {\TDIFd} {\ensuremath{\pr{tSUM}}}
\newcommand {\TPRDd} {\ensuremath{\pr{tPRD}}}
\newcommand {\SUMd} {\ensuremath{\pr{SUM}}}
\newcommand {\DIFd} {\ensuremath{\pr{DIF}}}
\newcommand {\PRDd} {\ensuremath{\pr{PRD}}}
\newcommand {\Pd} {\ensuremath{\pr{P}}}
\newcommand {\PPd} {\ensuremath{\pr{PP}}}
\newcommand {\Od} {\ensuremath{\pr{O}}}
\newcommand {\ATd} {\ensuremath{\pr{AT}}}
\newcommand {\ATPd} {\ensuremath{\pr{ATP}}}
\newcommand {\CPd} {\ensuremath{\pr{CP}}}
\newcommand {\PREd} {\ensuremath{\pr{PRE}}}
\newcommand {\SPREd} {\ensuremath{\pr{sPRE}}}
\newcommand {\DQTd} {\ensuremath{\pr{DQT}}}
\newcommand {\QTd} {\ensuremath{\pr{QT}}}
\newcommand {\QLd} {\ensuremath{\pr{QL}}}
\newcommand {\TQLd} {\ensuremath{\pr{tQL}}}
\newcommand {\QLxTxPDd} {\ensuremath{\pr{QL}_{T,PD}}}
\newcommand {\QLxTxEDd} {\ensuremath{\pr{QL}_{T,ED}}}
\newcommand {\QLxTxTQd} {\ensuremath{\pr{QL}_{T,TQ}}}
\newcommand {\QLxTxPQorAQd} {\ensuremath{\pr{QL}_{T,PQ \vee AQ}}}
\newcommand {\QLxTxQd} {\ensuremath{\pr{QL}_{T,Q}}}
\newcommand {\QLxTd} {\ensuremath{\pr{QL}_{T}}}
\newcommand {\QLxSxPEDd} {\ensuremath{\pr{QL}_{S,PED}}}
\newcommand {\QLxSxPQd} {\ensuremath{\pr{QL}_{S,PQ}}}
\newcommand {\QLxSxPDd} {\ensuremath{\pr{QL}_{S,PD}}}
\newcommand {\QLxSd} {\ensuremath{\pr{QL}_{S}}}
\newcommand {\INxTd} {\ensuremath{\subseteq_T}}
\newcommand {\INPxTd} {\ensuremath{\subset_T}}
\newcommand {\INxSd} {\ensuremath{\subseteq_{S}}}
\newcommand {\INPxSd} {\ensuremath{\subset_{S}}}
\newcommand {\INxSTd} {\ensuremath{\subseteq_{ST}}}
\newcommand {\INxSTxTd} {\ensuremath{\subseteq_{ST}}}
\newcommand {\CNxTd} {\ensuremath{\approx_T}}
\newcommand {\CNxSd} {\ensuremath{\approx_{S}}}
\newcommand {\CNxSTd} {\ensuremath{\approx_{ST}}}
\newcommand {\CNxSTxTd} {\ensuremath{\approx_{ST}}}
\newcommand {\OVxTd} {\ensuremath{\bigcirc_T}}
\newcommand {\OVxSd} {\ensuremath{\bigcirc_{S}}}
\newcommand {\PxTd} {\ensuremath{\pr{P}_T}}
\newcommand {\PxSd} {\ensuremath{\pr{P}_S}}
\newcommand {\NEPxSd} {\ensuremath{\pr{NEP}_S}}
\newcommand {\CMd} {\ensuremath{\pr{CM}}}
\newcommand {\CMNEGd} {\ensuremath{\pr{CM}^\sim}}
\newcommand {\HOMd} {\ensuremath{\pr{HOM}}}
\newcommand {\HOMNEGd} {\ensuremath{\pr{HOM}^\sim}}
\newcommand {\ATOMd} {\ensuremath{\pr{AT}}}
\newcommand {\ATOMNEGd} {\ensuremath{\pr{AT}^\sim}}
\newcommand {\PCd} {\ensuremath{\pr{PC}}}
\newcommand {\PCxCd} {\ensuremath{\pr{PC_C}}}
\newcommand {\PCxTd} {\ensuremath{\pr{PC_T}}}
\newcommand {\MPCd} {\ensuremath{\pr{{mPC}}}}
\newcommand {\MPPCd} {\ensuremath{\pr{mppc}}}
\newcommand {\LFd} {\ensuremath{\pr{lf}}}
\newcommand {\SDd} {\ensuremath{\pr{SD}}}
\newcommand {\GDd} {\ensuremath{\pr{GD}}}
\newcommand {\Dd} {\ensuremath{\pr{D}}}
\newcommand {\ODd} {\ensuremath{\pr{OD}}}
\newcommand {\OSDd} {\ensuremath{\pr{OSD}}}
\newcommand {\OGDd} {\ensuremath{\pr{OGD}}}
\newcommand {\MSDd} {\ensuremath{\pr{MSD}}}
\newcommand {\MGDd} {\ensuremath{\pr{MGD}}}
\newcommand {\SDxSd} {\ensuremath{\pr{SD_S}}}
\newcommand {\PSDxSd} {\ensuremath{\pr{PSD_S}}}
\newcommand {\PinvSDxSd} {\ensuremath{\pr{P^{-1}SD_S}}}
\newcommand {\GDxSd} {\ensuremath{\pr{GD_S}}}
\newcommand {\PGDxSd} {\ensuremath{\pr{PGD_S}}}
\newcommand {\PinvGDxSd} {\ensuremath{\pr{P^{-1}GD_S}}}
\newcommand {\DGDxSd} {\ensuremath{\pr{DGD_S}}}
\newcommand {\SDTxSd} {\ensuremath{\pr{SDt_S}}}
\newcommand {\GDTxSd} {\ensuremath{\pr{GDt_S}}}
\newcommand {\DGDTxSd} {\ensuremath{\pr{DGDt_S}}}
\newcommand {\OSDxSd} {\ensuremath{\pr{OSD_S}}}
\newcommand {\OGDxSd} {\ensuremath{\pr{OGD_S}}}
\newcommand {\MSDxSd} {\ensuremath{\pr{MSD_S}}}
\newcommand {\MGDxSd} {\ensuremath{\pr{MGD_S}}}
\newcommand {\Kd} {\ensuremath{\pr{K}}}
\newcommand {\DKd} {\ensuremath{\pr{DK}}}
\newcommand {\SKd} {\ensuremath{\pr{SK}}}
\newcommand {\GKd} {\ensuremath{\pr{GK}}}
\newcommand {\OSKd} {\ensuremath{\pr{OSK}}}
\newcommand {\OGKd} {\ensuremath{\pr{OGK}}}
\newcommand {\MSKd} {\ensuremath{\pr{MSK}}}
\newcommand {\MGKd} {\ensuremath{\pr{MGK}}}
\newcommand {\EXDd} {\ensuremath{\pr{EXD}}}
\newcommand {\MEXDd} {\ensuremath{\pr{mEXD}}}
\newcommand {\SLCd} {\ensuremath{\pr{SLC}}}
\newcommand {\TLCd} {\ensuremath{\pr{TLC}}}
%================================================================
% BFO categories and relations
%================================================================
\newcommand{\cntbcat}{\cn{cnt}}
\newcommand{\idcntbcat}{\cn{idcnt}}
\newcommand{\gdcntbcat}{\cn{gdcnt}}
\newcommand{\sdcntbcat}{\cn{sdcnt}}
\newcommand{\mtenbcat}{\cn{mten}}
\newcommand{\imenbcat}{\cn{imen}}
\newcommand{\objbcat}{\cn{obj}}
\newcommand{\fobjbcat}{\cn{fobjp}}
\newcommand{\objaggbcat}{\cn{objagg}}
\newcommand{\sitebcat}{\cn{site}}
\newcommand{\cfbndbcat}{\cn{cfbnd}}
\newcommand{\sregbcat}{\cn{sreg}}
\newcommand{\rlzenbcat}{\cn{rlzen}}
\newcommand{\occbcat}{\cn{occ}}
\newcommand{\procbcat}{\cn{proc}}
\newcommand{\pbndbcat}{\cn{pbnd}}
\newcommand{\tregbcat}{\cn{treg}}
\newcommand{\stregbcat}{\cn{streg}}
\newcommand{\qltbcat}{\cn{qlt}}
\newcommand{\rqltbcat}{\cn{rqlt}}
\newcommand{\tinstbcat}{\cn{tinst}}
\newcommand{\tintbcat}{\cn{tint}}
\newcommand{\histbcat}{\cn{hist}}
\newcommand{\onetregbcat}{\cn{treg1}}
\newcommand{\zerotregbcat}{\cn{treg0}}
\newcommand{\rolebcat}{\cn{role}}
\newcommand{\dispbcat}{\cn{disp}}
\newcommand{\fntbcat}{\cn{fnt}}
\newcommand{\fptbcat}{\cn{fpt}}
\newcommand{\flnbcat}{\cn{fln}}
\newcommand{\fsfbcat}{\cn{fsf}}
\newcommand{\onesregbcat}{\cn{sreg1}}
\newcommand{\zerosregbcat}{\cn{sreg0}}
\newcommand{\twosregbcat}{\cn{sreg2}}
\newcommand{\threesregbcat}{\cn{sreg3}}
\newcommand{\bfopartic}{\textsc{par}}
\newcommand{\bfouniv}{\textsc{uni}}
\newcommand{\bfoentity}{\textsc{ent}}
\newcommand{\bfotime}{\textsc{tm}}
\newcommand{\bforigid}{\prbfo{RG}}
\newcommand{\bfoisa}{\prbfo{ISA}}
\newcommand{\bfodisj}{\prbfo{DJ}}
\newcommand{\bfocpart}{\prbfo{cP}}
\newcommand{\bfocppart}{\prbfo{cPP}}
\newcommand{\bfocdisj}{\prbfo{cDJ}}
\newcommand{\bfocoverlap}{\prbfo{cO}}
\newcommand{\bfoopart}{\prbfo{oP}}
\newcommand{\bfooppart}{\prbfo{oPP}}
\newcommand{\bfoooverlap}{\prbfo{oO}}
\newcommand{\bfotpart}{\prbfo{tP}}
\newcommand{\bfotppart}{\prbfo{tPP}}
\newcommand{\bfotdisj}{\prbfo{tDJ}}
\newcommand{\bfotoverlap}{\prbfo{tO}}
\newcommand{\bfompart}{\prbfo{mP}}
\newcommand{\bfoexist}{\prbfo{EX}}
\newcommand{\bfoiof}[1]{{\,::_{#1\:\!}}}
\newcommand{\bfoinh}{\prbfo{INH}}
\newcommand{\bfosdep}{\prbfo{SDEP}}
\newcommand{\bfogdep}{\prbfo{GDEP}}
\newcommand{\bfooccurs}{\prbfo{OCCIN}}
\newcommand{\bfolocated}{\prbfo{LOC}}
\newcommand{\bfosregof}{\prbfo{sREG}}
\newcommand{\bfosregofocc}{\prbfo{sREG_O}}
\newcommand{\bfotregof}{\prbfo{tREG}}
\newcommand{\bfostregof}{\prbfo{stREG}}
\newcommand{\bfoparticin}{\prbfo{PTC}}
\newcommand{\bfoconcr}{\prbfo{CONCR}}
\newcommand{\bforealizes}{\prbfo{REAL}}
\newcommand{\bfotproj}{\prbfo{tPROJ}}
\newcommand{\bfosproj}{\prbfo{sPROJ}}
\newcommand{\bfohistory}{\prbfo{HIST}}
%==========================================
%==========================================
\pubyear{0000}
\volume{0}
\firstpage{1}
\lastpage{30}
\begin{document}
\begin{frontmatter}
\title{On the formal alignment of foundational ontologies: building mappings between {\bfo} and {\dolce}}
\runtitle{Formal alignment of {\bfo} and {\dolce}}
%\title{The formal alignment of foundational ontologies: a mapping of {\bfo} and {\dolce}}
\runtitle{Formal alignment of {\bfo} and {\dolce}}
%\title{{\bfo}-{\dolce} mappings: an experiment}
%\runtitle{{\bfo}-{\dolce} mappings: an experiment}
\author[A]{\inits{C.} \fnms{Claudio} \snm{Masolo}%\ead[label=e1]{[email protected]}
\thanks{Corresponding author. E-mail [email protected].}},
%\thanks{Corresponding author. \printead{e1}.}},
\author[B]{\inits{A.} \fnms{Francesco} \snm{Compagno}}, and %\ead[label=e2]{[email protected]}}
\author[A]
{\fnms{Stefano} \snm{Borgo}}
%\author[A]
%{\fnms{Luca} \snm{Biccheri}}, and
%\author[A]{\fnms{Emilio M.} \snm{Sanfilippo}}
\runauthor{Masolo et al.}
\address[A]{Laboratory for Applied Ontology, \institution{ISTC-CNR}, {Trento}, \cny{Italy}} %\printead[presep={\\}]{e1}}
\address[B]{Computer Science Department, \institution{University of Trento}, Trento, \cny{Italy}} %\printead[presep={\\}]{e2}}
%\address[C]{??, \institution{??},
%\cny{Italy}}
%\printead[presep={\\}]{e3}}
%==================================================
%==================================================
%==================================================
\begin{abstract}
\noindent
The development of an ontology-based ecosystem suitable for interoperability and for the reliable exchange of data is a longstanding goal of the applied ontology community. The construction of such a system relies on alignments across a variety of ontologies: foundational, reference and domain. While the techniques for the alignment of reference and domain ontologies have been continuously studied for more than 15 years; work on the techniques for the alignment of foundational ontologies and across foundational and reference ontologies have been scattered or hardly addressed. %Still today, the topic remains largely unexplored.
This paper aims to bring attention to the issue in three ways. It motivates the research, presents an approach to develop formal alignments of foundational ontologies, and implements its applicability to study the relationship among two of them, namely, {\bfo} and {\dolce}. The paper points also to variants of and alternatives to this approach by briefly comparing advantages and difficulties.
\end{abstract}
%==========================================
\begin{keyword}
\kwd{Ontology}
\kwd{{\bfo}}
\kwd{{\dolce}}
\kwd{Ontology Mappings}
\end{keyword}
\end{frontmatter}
%\noindent {\bf NOTA:}\\
% - QUALCHE VOLTA ``MAPPING'' SI RIFERISCE ALL'INSIEME DI TUTTE LE DEFINIZIONI\\
% - QUALCHE VOLTA ``MAPPING'' SI RIFERISCE A UNA SINGOLA DEFINIZIONE E POI SCRIVIAMO ``MAPPINGS'' PER PARLARE DI TUTTE\nb{CM: non ci vedo un problema forte, comunque mi sembra che siamo già abbastanza su questa linea}
% \medskip
% \noindent
% {\bf PROPOSTA:} (NON IMPLEMENTATA)\\
% USIAMO ``MAPPING'' PER L'INSIEME, ``DEFINIZIONE'' PER LA SINGOLA DEFINIZIONE\\
%===================================
\section{Introduction}\label{sect_intro}
%===================================
%{\color{red} **** direi che si tratta di un mapping fatto in OntoCommons con un'idea pluralistica e che qui riportiamo quali sono stati i challenges incontrati e come li abbiamo affrontati oltre poi a dire qualche cosa su alcune differenze trovate tra bfo e dolce / parlerei fin dall'inizio del fatto che abbiamo cercato di usare dei theorem provers / model generator (con successo parziale)}
In the 1980s the increasing development of storage and computational capacities made evident that interoperability across data and systems was becoming a fundamental problem of information science. In the early 1990s the research community started to focus on the hidden assumptions behind the generation and collection of data and the construction of information systems at large and, in a few years, this turned into a visionary research line, soon called {\em applied ontology}, that quickly became `the' approach to solve interoperability problems.
The roots of interoperability barriers were not yet clear but the growing availability and potentiality of large datasets, varying in both organisation and quality, drove attention to what one means by interoperability and how it could be achieved \citep{oukselSemanticInteroperability1999,gardner2005ontologies}. %\nb{CM: @Stefano, aggiungere entry}
A first source of problems, as it became clear later, was the lack of conceptual clarity and coherence in the internal organisation of datastores. Relational databases are powerful and successful tools but have important limitations (in particular when dealing with heterogeneous data) due to their rigidity and structural complexity. %\nb{CM: non capisco questa frase, in che senso hanno heterogeneous data?}
A second source of problems was the lack of a consistent methodology to merge databases and, more generally, to cope with the different structures of information systems. The fact that data were collected from different sources (each following its own purposes) and using different methodologies (each relying on often implicit assumptions) hampered any attempt to develop such a methodology, and information sharing across data storage remained a problem.
The applied ontology vision relies on two tenets: $(a)$ exploitation of formal semantics, and $(b)$ making explicit all the assumptions. It follows that the process of data integration should be analyzed at different levels: syntactic, semantic, conceptual and structural. %\nb{CM: mi suona strano questo interoperability, perché parlavamo di livelli, forse si può semplicemente togliere} \citep{guarinoOntologicalLevel1998}.
The focus on the semantics of data and on the conceptualisation of data organisation has brought a sharp change of perspective, and led to studying how to make explicit the viewpoint one takes on the external reality.
%, something that today we call the ontological viewpoint.
In the following ten years, the idea that one has to make explicit the assumptions behind data collection and data management became popular, even though how to do it remained unclear~\citep{oukselSemanticInteroperability1999}.
%\medskip
The focus of applied ontology on semantics and hidden assumptions made it possible to develop methodologies for data integration and systems' interoperability. The idea was to study an interoperability problem separating the interoperability levels and to use formal logic to uncover semantic inconsistencies, and philosophical analysis to uncover conceptual inconsistencies.
This step leads to clarifying the implicit choices on which the two systems or datasets rely, and to use logical and philosophical methods -- whenever useful -- to overcome possible mismatch. The next step is to harvest logical methodologies to develop an alignment methodology for those semantic frameworks, and similarly to harvest philosophical methodologies for the alignment of the conceptual frameworks.
This procedure gives, as one would expect, a general methodology whose product is a trustable semantic and conceptual mapping across the two systems, which can now be shown compatible at least to the extent of the mapping.
%\nb{CM: questo claim mi sembra forte, dipende dal significato di mapping}
%Yet, the two systems may rely on two distinct ontologies blocking the construction of the semantic mapping. This problem was easily dismissed by a simple iteration of the same process. After all, the ontologies themselves are nothing more than (perhaps special) information systems. This means that one could apply the same methodology to solve the semantic problem at the level of ontologies. That is, one can compare the two ontologies' conceptual systems from a more general viewpoint (e.g., from the so-called top-level~\citep{guarinoontologicalevels}) to find an alignment of the ontological systems. Once these are aligned, one can proceed with the alignment of the initial systems.
This approach was convincing enough to suggest that each dataset and information system should be shared together with its own semantic and conceptual frameworks, now known as their ontology. Each system, augmented with its explicit ontology, was then considered transparent and suitable for interoperability, if not for full integration.
Admittedly, systems may rely on incompatible semantic or conceptual choices, the alignments one can find in such cases may be only partial. This, one would have argued, is the cost of the pluralistic approach in modeling. The community, with only limited exceptions, accepted this cost as needed to practically verifying which modeling approaches were optimal and for which purposes.
%and, hopefully, over time there would be a convergence of modeling views at least in {\em real} applications.
% Furthermore, when an alignment was partial, one could at least minimise the data integration and system interoperability problem. Ontology alignment itself, it was quickly realised, was a complex topic well beyond the expertise of the standard knowledge engineer, and was happily left to the ontologist to face.
Today we have a set of general methodologies \citep{Euzenat2013, Jarrar2009, fernandezMethontology1997, gomezNeon2009} that help to develop and align datasets and information systems. While these approaches need time to be consolidated, they leave open the problem of aligning general ontologies, those that are now called foundational or top-level, as they are aimed to be applicable in full generality.
How ontology interoperability may work at this level has not been explored yet, mainly because of the complexity of these systems. Early works include a comparative study of {\bfo}, {\dolce} and \textsc{ochre}, with an alignment of \textsc{ochre} to {\dolce}~\citep{D18}.
%{\color{red}[ALTRO?]}\nb{CM: (1) nel d18 abbiamo mostrato come l'es. statua/creta è modellato dalle 3 ontologie, e abbiamo fatto solo il mapping ochre2dolce, nient'altro; (2) non conosco nessun altro che abbia fatto questi links, non so se GFO o Gruninger abbia fatto qualche cosa, ma non sarebbe un early work}.
Unfortunately, this study uses an \textit{ad hoc} approach and does not provide a systemic view. So far no general methodology has been investigated and no systematic study has been carried out.
\medskip
The present paper is part of a larger effort to build an ontology ecosystem as described by the visionary OntoCommons European project\footnote{\url{ontocommons.eu/}}. Motivated by this line of research, the paper proposes an approach to align top-level formal ontologies, and presents problems, advantages and limitations as elicited by studying the alignment of two well-known foundational ontologies, namely {\dolce} \citep{borgoDOLCEDescriptiveOntology2022} and {\bfo} \citep{barryBasicFormalOntology2015}. The main purpose is to investigate the kind of problems and possible solutions that emerge in this kind of analysis in the hope that the collection and study of these cases highlight the specificity of these issues and their relevance to understand cross-ontology interoperability. Furthermore, practical experiences like this can lead to developing a shared and general methodology for the alignment of top-level ontologies in general.
%\medskip
The view underlying the work in this paper is known as ``ontological pluralism'' which claims that science needs to remain open to different ontologies, i.e., to ontologies representing different points of view, and thus should allow the coexistence of possibly mutually inconsistent models. Inconsistence, we should add, can be conceptual as well as formal. Interoperability across inconsistent ontologies is obtained by (possibly partial) alignments via formal mappings. The OntoCommons ontology ecosystem is essentially a network of interconnected domain, reference and foundational ontologies, which is being built in these years starting from an initial set of ontologies and a number of guidelines (still under development). The alignment presented in this paper is one of the results of the project at this stage.
%OntoCommons investigates three top-level ontologies, namely, Basic Formal Ontology\footnote{??} ($\bfo$), Descriptive Ontology for Linguistic and Cognitive Engineering\footnote{??} ($\dolce$), and European Materials and Modelling Ontology\footnote{??} ($\emmo$).
The alignment (and underpinning conceptual and technical choices) is performed on the first-order logic (FOL) versions of the chosen ontologies.
%Today the $\emmo$ ontology is mostly available in OWL\footnote{??}. The FOL formalisation of $\emmo$ is under development and its alignment with the other ontologies will be investigated in the future.
The $\bfo$-$\dolce$ mapping applies to the most recent versions of these two ontologies in the CLIF language of Common Logic (CL), an ISO standard\footnote{\url{https://www.iso.org/standard/66249.html}}, as submitted by the groups that developed these ontologies, see Sect.~\ref{sect_bfo_and_dolce} for more details.
The choice to use CL is the result of several considerations including that the use of CL is fairly consolidated in the research literature and in applications, and that the visibility and stability of standards can help to increase users' trust in an ontology ecosystem fostering its adoption and extension.
\medskip
The aims of this paper are:
\begin{enumerate}[$(i)$]
\item to report the theoretical and practical challenges one faces in aligning foundational, large (more than 100 axioms) ontologies;
\item to highlight the most difficult and intertwined choices one might be confronted with during alignment processes;
\item to discuss possible alternatives and their consequences on the alignment; and
\item (as a byproduct of the alignment) to provide an analysis of the main differences/similarities between $\bfo$ and $\dolce$.
\end{enumerate}
The paper is structured as follows:
Section \ref{sect_bfo_and_dolce} introduces the ontologies and the notation. %The axiomatisation itself is given in the appendix.\nb{CM: non sono sicuro sia una buon idea perché quella di DOLCE ce l'abbiamo mentre per quella di BFO non abbiamo tutti gli assiomi. Inoltre poi in sez. 2.1 diciamo diversamente}
Section \ref{sect_methodology} describes the adopted methodology and the software used to support and check the alignment.
%The following material,
Section \ref{sect_prelim_considerations} presents the alignment strategy and discusses the main categories that form the core of the two ontologies.
The two following sections, Section \ref{sect_d2b} and Section \ref{sect_b2d}, form the technical core of the paper: they present the formal alignment as two distinct mappings: from $\dolce$ to $\bfo$ and from $\bfo$ to $\dolce$.
Since the motivation of this work is the construction of an ontology ecosystem that includes also reference and domain ontologies, Section \ref{sect_FOL_OWL} adds some considerations on the possible use (and consequences) of using the given alignments to support alignments in languages of the OWL family \citep{owlref}.
The last session, Section \ref{sect_conclusion}, summarises the results, discusses other open questions, and lists the next steps in this research line.
%===================================
\section{{\bfo} and {\dolce}}
\label{sect_bfo_and_dolce}
%===================================
%{\color{red} ****aggiungere qui due parole sulla storia di DOLCE e BFO magari ispirandoci dai siti web (per BFO https://basic-formal-ontology.org/, dal d2.2 di OntoCommons, ecc.\\
%SB: qui sotto ho ripreso il testo dall'intro allo sp. issue FOUST, se serve estendiamo.}
{\bfo} and {\dolce} are among the most well-known and used foundational ontologies. In the literature one can find several systems, all developed within the last 20 years and each investigating different ontological choices \citep{Borgo-GK2022FOinAction}. %\nb{CM: non ho capito che cosa si voleva citare qui, forse lo special issue di AO? SB: non ricordo neppure io, ok per lo sp. issue}
The decision to investigate the alignment between {\bfo} and {\dolce} is due to the choice made in the OntoCommons project which, in turn, has selected the two ontologies that have been developed earlier in this research area and that have influenced how applied ontologies are presented and discussed today. Note that, leaving aside terminological and other lightweight alignments, a formal comparison of {\bfo} and {\dolce} was partially investigated in 2003~\citep{D18} and, more recently, a conceptual analysis has been proposed~\citep{Guarino-2017BfoDolce}. %\nb{CM: (1) questo non è vero; (2) citare qui i lavori che esistono su questo inclusi quelli di Nicola?}\nb{SB: ho messo `comparison' e aggiunto Guarino. altro da correggere/aggiungere?}
A brief historical view of the {\bfo} and {\dolce} ontologies is given next, an introduction of their formal approaches follows. For more information on the ontologies see \citep{ISO21838, Borgo-GK2022FOinAction}.
`Basic Formal Ontology', $\bfo$ for short, is a ``realist'' top-level ontology intended to represent entities as described by science and designed to support information integration, retrieval, and analysis across all domains of scientific investigation, and has been under development since around 2002 \citep{grenonBiodynamic2004}. %\nb{per bib vedi file .tex}
It serves as the top-level ontology of the Open Biomedical and Bioinformatic Ontology (OBO) Foundry and the Industrial Ontology Foundry (IOF). $\bfo$ has changed considerably over the years and today there are several versions available.
The one considered in this paper is the $\bfo$ presented in 2020 as part of the standard ISO 21838 (part 2) \citep{ISO21838}. This version is axiomatised in Common Logic (CLIF) \citep{ISO24707} and in the Web Ontology Language (OWL).
`Descriptive Ontology for Linguistic and Cognitive Engineering', $\dolce$ for short, is a top-level ontology with a cognitive bias developed in early 2000 as part of the European project `WonderWeb'\footnote{\url{http://wonderweb.man.ac.uk/index.shtml}} and published as part of WonderWeb Deliverable 18 \citep{D18}. The axiomatisation is done in FOL extended with modalities, namely, the standard necessity and possibility operators. Following this work, $\dolce$ has been applied in a number of areas, in several national, European and other international projects, leading to build some application-oriented versions in OWL among which $\dolce$-lite, $\dolce$-ultralite, and $\dolce$-zero.
The group that developed $\dolce$ takes a conservative approach. The ontology has only minimally changed over the years making it the most stable top-level ontology worldwide. In this paper we consider the $\dolce$ version presented in 2022 as part of the standard ISO 21838 (part 3) which required a version in Common Logic (CLIF).
From the ISO 21838 we also take the $\dolce$ version in the Web Ontology Language (OWL).
%===================================
\subsection{CL version of {\bfo} 2020 (as of November 12, 2021)}\label{sect_bfo}
%===================================
%This section reports the axioms of {\bfo} that are relevant for the mappings from {\dolce} to {\bfo}.
%%mapping.
%In Sect.~\ref{sect_mappings_d2b} we discuss the fact that some notions of {\bfo} are not definable in {\dolce}. It is important to observe that for the {\bfo} to {\dolce} mapping we consider the full {\bfo}, see in particular the material in Sec.~\ref{sect_check_dolce_preservation}.
%
%\medskip
We start from the logical theory {\bfocl} consisting of all the axioms of BFO 2020 in CLIF, released on 12 November 2021 and accessible in GitHub\footnote{\url{https://github.com/BFO-ontology/BFO-2020/tree/master/21838-2/prover9}}. The version we use in the alignment is called $\thbfo$, is given in the syntax of Prover9 and presents four differences with respect to {\bfocl}: $(i)$ inverse relations in {\bfocl} (e.g., hasContinuantPart is the inverse of continuantPartOf) are given in $\thbfo$ by inverting the order of arguments (the temporal argument maintains its position); $(ii)$ the `AtSomeTime' and `AtAllTimes' relations present in {\bfocl} are never used in other axioms of {\bfocl} and, for this reason, are not considered in $\thbfo$\footnote{Note that `AtSomeTime' and `AtAllTimes' relations are used in the OWL version of {\bfo}.}; $(iii)$ relations introduced in {\bfocl} with `if and only if' clauses are present in $\thbfo$ as syntactic definitions;
% \refbfodf{cppart} for continuantProperPartOf, \refbfodf{oppart} for occurrentProperPartOf, \refbfodf{tppart} for temporalProperPartOf, and \refbfodf{bfoinh} for inheresIn.\nb{CM: si può togliere questo credo}
and $(iv)$ further syntactic definitions are added to improve the readability of some formulas.
To have more compact formulas, the {\bfo} predicates has been shorten as shown in Table~\ref{table_prim_bfo} (where the third column gives the original predicates in {\bfocl}) and in Table~\ref{table_cat_bfo}. To avoid confusion, we indicate the {\bfo}-predicates in $\mathit{italics}$ while the {\dolce}-predicates in $\mathtt{type writer}$.
The classes of \emph{particulars} and \emph{universals} are represented in {\bfo} by unary predicates (and not by individual constants as the other explicitly named universals): we use $\bfopartic$ for particulars and $\bfouniv$ for universals. %\nb{FC: PAR non è una costante. Assieme a "entity(.)" e a "UNI(.)" è un predicato. Inserire tutti e tre in tabella 1 oppure aggiungere UNI e entity nella 2?}.\nb{CM: togliere PAR, mettere una nota su PAR, UNI, e EN e dire che tabella 2 e fig. 1 sono relative solo ai particulars}
%\nb{CM: aggiungere nelle tabelle le primitive che si trovano nel file CL; FC: adesso, le uniche non menzionate sono entità e universale, mancavano inerenza [che è definita, quindi ok] e occorrenti}
The taxonomy of the $\thbfo$ particulars is depicted in Figure~\ref{figure_tax_bfo} (vertical lines represent ISA relationships, solid lines indicate a partition). All the universals in the taxonomy in Figure~\ref{figure_tax_bfo} are `rigid' (in the sense that their instances cannot migrate over time to another universal) except for $\objbcat$, $\fobjbcat$, and $\objaggbcat$. %In addition, all the universals directly subsumed by a given universal cover the whole root and are disjoint except $\objbcat$, $\fobjbcat$, and $\objaggbcat$ for which the disjointness is not explicitly stated.
%Third, for relevant relations introduced in {\bfo}-\textsc{cl} with `if and only if' clauses, we introduce corresponding syntactic definitions: \refbfodf{cppart} for continuantProperPartOf, \refbfodf{oppart} for occurrentProperPartOf, \refbfodf{tppart} for temporalProperPartOf, and \refbfodf{bfoinh} for inheresIn.\nb{CM: si può togliere questo credo}
%Fourth, to improve the readability of formulas, we introduce some syntactic definitions: \refbfodf{time}, \refbfodf{b_iof_notime}, \refbfodf{def_bfoisa}, \refbfodf{coverlap}, \refbfodf{ooverlap}, \refbfodf{toverlap}.
%Few other relevant axioms are still missing in the comparison.
%this theory
% the consisting of the axioms \refbfoax{particORuniv}-\refbfoax{tinst_to_treg} together with the syntactic definitions \refbfodf{time}-\refbfodf{bfoinh} introduced in the Sections \ref{bfo:partANDuniv}-\ref{bfo:taxonomy}.
%%==============================
%\subsection{{\bfo} primitive relations}
%%==============================
%
%Table~\ref{table_prim_bfo} lists the primitive relations of {\bfo}. We excluded from this table:
%\begin{itemize}
%\item the inverse relations (e.g., hasContinuantPart is the inverse of continuantPartOf) because in FOL it is enough to invert (some of) the arguments (e.g., $\bfocpart(x,y,t)$ vs. $\bfocpart(y,x,t)$);
%
%\item `AtSomeTime' and `AtAllTimes' relations that can be easily defined in FOL, e.g.,
%$\mathrm{continuantPartOfAtSomeTime}(x,y) \sdef \exists t(\bfocpart(x,y,t))$;
%
%\item some relations that can be syntactically defined: continuantProperPartOf \refbfodf{cppart}, occurrentProperPartOf \refbfodf{oppart}, temporalProperPartOf \refbfodf{tppart}, inheresIn \refbfodf{bfoinh}.
%\end{itemize}
\begin{table*}
\caption{Primitive relations of {\bfo}.}\label{table_prim_bfo}
\begin{tabular}{|l|l|l|}
\hline
$x \bfoiof{t} u$ & $x$ is an instance of $u$ at time $t$ & instanceOf\\
\hline
$\bfoexist(x,t)$ & $x$ exists at time $t$ & existsAt\\
\hline
$\bfocpart(x,y,t)$ & $x$ is a continuant part of $y$ at time $t$ & continuantPartOf\\
\hline
$\bfoopart(x,y)$ & $x$ is an occurrent part of $y$ & occurentPartOf\\
\hline
$\bfompart(x,y)$ & $x$ is a member part of $y$ & memberPartOf\\
\hline
$\bfotpart(x,y)$ & $x$ is a temporal part of $y$ & temporalPartOf\\
\hline
$\bfostregof(x,y)$ & $x$ occupies spatiotemporal region $y$ & occupiesSpatiotemporalRegion\\
\hline
$\bfosregof(x,y,t)$ & $x$ occupies spatial region $y$ at time $t$ & occupiesSpatialRegion\\
\hline
$\bfotregof(x,y)$ & $x$ occupies temporal region $y$ & occupiesTemporalRegion\\
\hline
$\bfotproj(x,y)$ & $x$ temporally projects onto $y$ & temporallyProjectsOnto\\
\hline
$\bfosproj(x,y,t)$ & $x$ spatially projects onto $y$ at time $t$ & spatiallyProjectsOnto\\
\hline
$\bfooccurs(x,y)$ & $x$ occurs in $y$ & occursIn\\
\hline
$\bfolocated(x,y,t)$ & $x$ is located in $y$ at time $t$ & locatedIn\\
\hline
$\bfosdep(x,y)$ & $x$ specifically depends on $y$ & specificallyDependsOn\\
\hline
$\bfoconcr(x,y)$ & $x$ concretizes $y$ & concretizes\\
\hline
$\bfogdep(x,y,t)$ & $x$ generically depends on $y$ at time $t$ & genericallyDependsOn \\
\hline
$\bfoparticin(x,y,t)$ & $x$ participates in $y$ at time $t$ & participatesIn \\
\hline
$\bforealizes(x,y)$ & $x$ realizes $y$ & realizes\\
\hline
$\bfohistory(x,y)$ & $x$ is the history of $y$ & historyOf \\
\hline
$\prbfo{PREC}(x,y)$ & $x$ precedes $y$ & precedes\\
\hline
$\prbfo{FINST}(x,y)$ & $x$ is the first instant of $y$ & firstInstantOf\\
\hline
$\prbfo{LINST}(x,y)$ & $x$ is the last instant of $y$ & lastInstantOf\\
\hline
$\prbfo{MBAS}(x,y,t)$ & $x$ is the material basis of $y$ at time $t$ & materialBasisOf\\
\hline
\end{tabular}
\end{table*}
%%==============================
%\subsection{{\bfo} categories}
%%==============================
\begin{table*}
\caption{Categories of {\bfo}.}\label{table_cat_bfo}
\begin{minipage}{0.43\textwidth}
\hspace{30pt}
\begin{tabular}{|p{.14\textwidth}|p{.60\textwidth}|}\hline
$\cfbndbcat$ & Continuant Fiat Boundary\\\hline
$\cntbcat$ & Continuant \\\hline
$\dispbcat$ & Disposition \\\hline
$\flnbcat$ & Fiat Line \\\hline
$\fobjbcat$ & Fiat Object Part\\\hline
$\fptbcat$ & Fiat Point \\\hline
$\fsfbcat$ & Fiat Surface \\\hline
$\fntbcat$ & Function \\\hline
$\gdcntbcat$ & Generically Dep. Continuant \\\hline
$\histbcat$ & History \\\hline
$\idcntbcat$ & Independent Continuant \\\hline
$\imenbcat$ & Immaterial Entity \\\hline
$\mtenbcat$ & Material Entity \\\hline
$\objbcat$ & Object \\\hline
$\objaggbcat$ & Object Aggregate \\\hline
$\occbcat$ & Occurrent \\\hline
%$\bfopartic$ & Particular \\\hline
$\pbndbcat$ & Process Boundary \\\hline
$\procbcat$ & Process \\\hline
\end{tabular}
\end{minipage}%
\mbox{}\hfill{}
\begin{minipage}{0.43\textwidth}
\hspace{-30pt}\begin{tabular}{|p{.14\textwidth}|p{.60\textwidth}|}
\hline
$\qltbcat$ & Quality \\\hline
$\rqltbcat$ & Relational Quality \\\hline
$\rlzenbcat$ & Realizable Entity \\\hline
$\rolebcat$ & Role \\\hline
$\sdcntbcat$ & Specifically Dep. Continuant \\\hline
$\sitebcat$ & Site \\\hline
$\sregbcat$ & Spatial Region \\\hline
$\zerosregbcat$ & 0d Spatial Region \\\hline
$\onesregbcat$ & 1d Spatial Region \\\hline
$\twosregbcat$ & 2d Spatial Region \\\hline
$\threesregbcat$ & 3d Spatial Region \\\hline
$\tregbcat$ & Temporal Region \\\hline
$\zerotregbcat$ & 0d Temporal Region \\\hline
$\onetregbcat$ & 1d Temporal Region \\\hline
$\stregbcat$ & Spatiotemporal Region \\\hline
$\tinstbcat$ & Temporal Instant \\\hline
$\tintbcat$ & Temporal Interval \\\hline
& \\\hline
\end{tabular}
\end{minipage}%
\end{table*}
\begin{figure}
\begin{small}
\hspace{-0pt}\xymatrix@R=10pt@C=0pt{
&&&&&&& \bfopartic \ar@{-}[drr] \ar@{-}[dll] \\
&&&&& \cntbcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr] &&&& \occbcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr] \ar@{-}[drr]\\
&&&& \idcntbcat \ar@{-}[d] \ar@{-}[dlll] & \gdcntbcat & \sdcntbcat \ar@{-}[d] \ar@{-}[dr] && \procbcat \ar@{--}[d] & \pbndbcat & \tregbcat \ar@{-}[d] \ar@{-}[dr]& \stregbcat \\
& \mtenbcat \ar@{--}[d] \ar@{--}[dl] \ar@{--}[dr]& & & \imenbcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr] & & \qltbcat \ar@{--}[d] & \rlzenbcat \ar@{-}[d] \ar@{-}[dr]& \histbcat & & \zerotregbcat \ar@{--}[d] & \onetregbcat \ar@{--}[d] \\
\objaggbcat & \fobjbcat & \objbcat& \cfbndbcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dll] & \sitebcat & \sregbcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr] \ar@{-}[drr] & \rqltbcat & \rolebcat & \dispbcat \ar@{--}[d] & &\tinstbcat & \tintbcat \\
& \fptbcat & \flnbcat & \fsfbcat & \zerosregbcat & \onesregbcat & \twosregbcat & \threesregbcat & \fntbcat \\
}
\end{small}
\caption{Taxonomy of {\bfo} (vertical lines stand for ISA relationships, solid lines indicate a partition).}\label{figure_tax_bfo}
\end{figure}
%The whole theory {$\thbfo$} is available in prover9 syntax at XXXX\nb{FC: loro GitHub o versione nostra?}.
As anticipated in the introduction, {\bfo} is a large theory, thus we do not report the whole axiomatisation. It can be found at the link given earlier. Nonetheless, whenever specific axioms are discussed, we report them explicitly in the text.
%\nb{CM: tagliate definizioni che non mi sembra servino, da controllare comunque} Furthermore, when the context is clear, we will use $\thbfo$ and ${\bfo}$ interchangeably.
%We start by reporting some definitions that introduce predicates commonly used in $\thbfo$, such as inheritance \refbfoax{bfoinh}, the predicates derived from mereological theories, such as overlapping and stric parts \refbfoax{coverlap}, \refbfoax{ooverlap}, \refbfoax{tppart}, subsumption between universals \refbfodf{def_bfoisa}, atemporalized instantiation \refbfoax{def_bfoisa}, and the class of {$\bfo$} times \refbfoax{time}.\nb{CM: spostare dopo e tenere solo quelle che servono}
%
%%hroughout the paper, $\thbfo$ axioms that are simple transpositions of axioms of {\bfocl} are accompanied by the identifier of the original axiom between square brackets.
%%If a $\thbfo$ axiom is not accompanied by square brackets\nb{FC: richiederebbe di riportare tutti gli identificativi degli assiomi originali}, it is a new axiom introduced by us with the role of `syntactical sugar'.
%%\nb{CM: forse conviene mettere qui gli assiomi che poi andiamo a considerare nei teoremi invece che scrivere i teoremi per cui basta scrivere $\thdolcedbmap \vDash (\bfoax{xx})$ or $\thdolcedbmap \nvDash (\bfoax{xx})$ o dirlo a parole}
%%
%\bflist
%\item[\bfodf{time}] $\bfotime(x) \sdef x \bfoiof{x} \tregbcat$
%
%\item[\bfodf{b_iof_notime}] $x \bfoiof{} u \sdef \exists t(x \bfoiof{t} u)$
%
%\item[\bfodf{def_bfoisa}] $\bfoisa(x,y) \sdef \forall zt(z \bfoiof{t} x \to z \bfoiof{t} y)$
%
%%\item[\bfodf{coverlap}] $\bfocoverlap(x,y,t) \sdef \exists z(\bfocpart(z,x,t) \land \bfocpart(z,y,t))$
%
%%\item[\bfodf{ooverlap}] $\bfoooverlap(x,y) \sdef \exists z(\bfoopart(z,x) \land \bfoopart(z,y))$
%
%\item[\bfodf{toverlap}] $\bfotoverlap(x,y) \sdef \exists z(\bfotpart(z,x) \land \bfotpart(z,y))$
%
%\item[\bfodf{tppart}] $\bfotppart(x,y) \sdef \bfotpart(x,y) \land x \neq y$
%
%\item[\bfodf{bfoinh}] $\bfoinh(x,y) \sdef \bfosdep(x,y) \land x \bfoiof{} \sdcntbcat \land y \bfoiof{} \idcntbcat \land \neg (y \bfoiof{} \sregbcat)$ \hfill {\scriptsize [tht-1]}
%
%
%\eflist
%===================================
\subsection{CL version of {\dolce} (as of August 13, 2021) }\label{sect_dolce}
%===================================
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%DOLCE SIMPLE plus CONCEPTS
%Version for MACE4 / PROVER9 by D. Porello, S. Borgo, L. Vieu.
%Proved consistent.
%
%
%Based on the axioms of DOLCE (D18) proved consistent in
%(v. DolceSimple) https://github.com/spechub/Hets\neglib/blob/master/Ontology/Dolce/DolceSimpl.dol
%NOTE: The names of the axioms and theorems of DOLCE SIMPLE are those from DOLCE D18 for direct comparison.
%(http://www.loa.istc.cnr.it/wp\negcontent/uploads/2020/03/D18inv.31\neg12\neg03.pdf)
%
We write $\thdolce$ for the logical theory consisting of all the axioms in the CL-version of {\dolce}\footnote{Available from \url{http://www.loa.istc.cnr.it/wp-content/uploads/2023/05/DOLCE_clean.tptp_.txt} (in tptp syntax) and \url{http://www.loa.istc.cnr.it/wp-content/uploads/2023/05/DOLCE_clean.prover9.txt} (in Prover9 syntax). For a more human-accessible version refer to \citep[ch.2]{D24} available from \url{https://cloud.cnr.it/owncloud/index.php/s/WzsBI7qw3Om0j0u}.} using the syntax of Prover9. With respect to the original version of {\dolce} introduced in \citep{D18}, from now on called {\dolceorig},
%\nb{CM: non so se vogliamo fare riferimento alla versione di Daniele (per capirci) depositata pe l'ISO}\nb{SB: direi di si, anche per coerenza con la scelta su BFO}
$\thdolce$ presents two main differences following the {\dolce-\textsc{iso}} version:
\bflist
\item[(1)] Modality operators are not used as they are not part of the language of Common Logic (since {\dolceorig} is a first order {\em modal} theory relying on the modal logic QS5 with constant domain, the lack of modal operators in $\thdolce$ changes the intended models of {\dolce});
\item[(2)] The mereological fusion operator (operator $\sigma$ in {\dolceorig}) is not available in the language of Common Logic (for each property expressible in the system, {\dolceorig} enforces the existence of the mereological sum of all the entities that satisfy that property; this cannot be ensured in $\thdolce$ due to the lack of the fusion operator.)
\eflist
The first simplification weakens several notions of dependence since these are strongly grounded on modality. To partially overcome this difference, $\thdolce$ has the additional primitive of temporary existential dependence ($\EXDd$) which, however, compensates only in part the lack of modal operators. %remain weaker than the existential dependence operator in {\dolceorig}. % as we will see in Section \ref{sect:dolce_dependence} .
% (specific dependence ($\SDd$) is introduced only considering time, see \refdolcedf{dfSDd});
Concerning the second simplification, %\nb{CM: ho tagliato qui perché non mi sembrava corretto} %to partially overcome the lack of the fusion operation, $\thdolce$ adopts the axiom of strong supplementation for $\Pd$ (parthood simpliciter) and $\TPd$ (temporary parthood). Therefore,
$\thdolce$ is based on extensional mereologies (EM), rather than general extensional mereologies (GEM) assumed in $\dolceorig$. % as in the case of {\dolceorig}.
Note that $\thdolce$ does not enforces the closure of the domain under (binary) sum and product. It is left to the user to add sum and product operators depending on modeling needs. Additionally, some notions that in {\dolceorig} are defined via the mereological fusion operator, are introduced in $\thdolce$ as primitives. In particular, in $\thdolce$ we have the temporal relation $\TLCd(x,t)$, read as ``$x$ is (exactly) located at time $t$'', and the temporary spatial relation $\SLCd(x,s,t)$, ``at time $t$, $x$ is (exactly) located at space $s$''.
Two additional simplifications, with respect to $\dolceorig$, are adopted in $\thdolce$ (again following {\dolce-\textsc{iso}}):
%
\bflist
%\item (Ad9) and (Ad15) in D18 are weakened assuming the existence of {binary} sums instead of fusions;
%\item the predicate $\PREd$ (being present) defined {\dolce} by means of the mereological fusion is here introduced as a primitive relation;
\item[--] only direct qualities are considered ($\DQTd$);
\item[--] the one-to-one link between quality types (e.g., temporal location, color location) and
%(Ad56), (Ad57), (Ad63), and (Ad64) in {\dolceorig} are instantiated only by
quality spaces (e.g., time interval, color region) assumed in {\dolceorig}\footnote{See (Ad56), (Ad57), (Ad63), and (Ad64) in {\dolceorig}.} is not enforced anymore. The same quality kind can be linked to several quality spaces, a given color location can be located in an RGB color-space, a color spindle space, etc.
%\nb{CM: se ricordo bene questo è il motivo per cui in $\thdolce$ non abbiamo ad es.$\QLd(x,y) \to (\Tdcat(x) \ifif \TLdcat(y))$ o $\TQLd(x,y,t) \to (\Sdcat(x) \ifif \SLdcat(y))$} \nb{SB: anch'io ricordo così}
%is explicitly introduced only
%$(i)$ between temporal location ($\TLdcat$) and time interval ($\Tdcat$); and $(ii)$ between spatial location ($\SLdcat$) and space region ($\Sdcat$), i.e., between the quality kinds and quality spaces explicitly considered in {$\thdolce$}.\footnote{See (Ad56), (Ad57), (Ad63), and (Ad64) in {\dolceorig}.}\nb{[FC: dopo aver letto la versione di DOLCE in AO 2022 e quella di D.Porello et al., non vedo come questo punto sia corretto, a meno che non faccia riferimento al mantenimento degli assiomi Ad53 e Ad61]}\nb{CM: Francesco prova a vedere se ti quadra adesso}\nb{CM: credo si debba rafforzare $\thdolce$, perché $\QLd(x,y) \to (\Tdcat(x) \ifif \TLdcat(y))$ e $\TQLd(x,y,t) \to (\Sdcat(x) \ifif \SLdcat(y))$ non mi sembra valgano adesso} % 2-Io voto per non citare assiomi di D18, magari qualcosa tipo "Axioms that quantified over taxonomy categories are not considered."]}
%\item {\color{red} the ``spatial inclusion'' relation is not defined here (originally it needs fusion) therefore axioms (Ad19),(Ad28), and (Ad68) are not expressed.}\nb{CM: per questi in effetti si potrebbe fare qualche cosa}
%\item To obtain more populated models, we omit the existence of sums and (Ad29)
\eflist
%DOLCE SIMPLE plus CONCEPTS with respect to DOLCE D18:
%1. Adjunction of the theory of concepts and roles as endurtants (non\negagentive social objects) and of the relation of classification from:
%Claudio Masolo, Laure Vieu, Emanuele Bottazzi, Carola Catenacci, Roberta Ferrario, Aldo Gangemi,and Nicola Guarino.
%Social roles and their descriptions.
%In Proceedings of the 9th International Conference on the Principles of KnowledgeRepresentation and Reasoning (KR\neg2004), pages 267–277, 2004
%In the following, with {\dolce} we indicate the logical theory $\thdolce$ consisting of the axioms \refdolceax{PdArg}-\refdolceax{disj_tr_ar} together with the syntactic definitions \refdolcedf{def_PPd}-\refdolcedf{dfSPREd} introduced in the Sections \ref{dolce_mereology}-\ref{dolce:taxonomy}.
Table~\ref{table_prim_dolce} lists the primitive relations of {$\thdolce$}, Table~\ref{table_cat_dolce} lists the categories of {$\thdolce$}, and Figure~\ref{fig_tax_dolce} shows the taxonomy of {$\thdolce$} (vertical lines stand for ISA relationships, solid lines indicate a partition).
\bflist
\item[\dolcedf{def_PPd}] $\PPd(x,y) \sdef \Pd(x,y) \land \neg\Pd(y,x)$
\mbox{} \hfill{} (\emph{Proper Part})
\item[\dolcedf{def_Od}] $\Od(x,y) \sdef \exists z (\Pd(z,x) \land \Pd(z,y))$
\mbox{} \hfill{} (\emph{Overlap})
\item[\dolcedf{def_ATd}] $\ATd(x) \sdef (\PDdcat(x) \lor \ABdcat(x)) \land \neg\exists y (\PPd(y,x))$
\mbox{} \hfill{} (\emph{Atom})
\item[\dolcedf{def_SUMd}] $\SUMd(s,x,y) \sdef \forall z (\Od(z,s) \ifif (\Od(z,x) \lor \Od(z,y)))$
\mbox{} \hfill{} (\emph{Mereological Sum})
\item[\dolcedf{def_TPPd}] $\TPPd(x,y,t) \sdef \TPd(x,y,t) \land \neg\TPd(y,x,t)$
\mbox{} \hfill{} (\emph{Temporary Proper Part})
\item[\dolcedf{def_TOd}] $\TOd(x,y,t) \sdef \exists z (\TPd(z,x,t) \land \TPd(z,y,t))$
\mbox{} \hfill{} (\emph{Temporary Overlap})
\item[\dolcedf{dfPREd}] $\PREd(x,t) \sdef \exists u(\TLCd(x,u) \land \Pd(t,u))$
\mbox{} \hfill{} (\emph{Being Present in Time})
\item[\dolcedf{dfSDd}] $\SDd(x,y) \sdef \exists t (\PREd(x,t)) \land \forall t (\PREd(x,t) \to \EXDd(x,y,t))$
\mbox{} \hfill{} (\emph{Specific Dependence})
\item[\dolcedf{dfSPREd}] $\SPREd(x,s,t) \sdef \exists r(\SLCd(x,r,t) \land \Pd(s,r))$
\mbox{} \hfill{} (\emph{Being Present in Space})
\eflist
In the paper we report only the axioms of $\thdolce$ actually needed for the discussion. When the context is clear, we will use $\thdolce$ and ${\dolce}$ interchangeably. %\nb{CM: forse ricordare qui dove è disponibile la lista di tutti gli assiomi}
%
%%==============================
%\subsection{{\dolce} primitive relations}
%%==============================
\begin{table*}
\caption{Primitive relations of {\dolce}.}\label{table_prim_dolce}
\begin{tabular}{|l|l|}
\hline
$\DQTd(x,y)$ & $x$ is a direct quality of $y$ \\
\hline
$\EXDd(x,y,t)$ & $x$ is existentially dependent on $y$ at time $t$\\
\hline
$\Kd(x,y,t)$ & $x$ constitutes $y$ at time $t$ \\
\hline
$\Pd(x,y)$ & $x$ is part of $y$ \\
\hline
$\PCd(x,y,t)$ & $x$ participates in $y$ at time $t$\\
\hline
$\QLd(x,y)$ & $x$ is the immediate quale of $y$ \\
\hline
$\SLCd(x,y,t)$ & $x$ is (exactly) located at space $y$ at time $t$\\
\hline
$\TLCd(x,t)$ & $x$ is (exactly) located at time $t$ \\
\hline
$\TPd(x,y,t)$ & $x$ is part of $y$ at time $t$ \\
\hline
$\TQLd(x,y,t)$ & $x$ is the temporary quale of $y$ at time $t$\\
\hline
\end{tabular}
\end{table*}
%%==============================
%\subsection{{\dolce} categories}
%%==============================
\begin{table*}
\caption{Categories of {\dolce}.}\label{table_cat_dolce}
\begin{minipage}{0.45\textwidth}
\hspace{40pt}
\begin{tabular}{|p{.10\textwidth}|p{.60\textwidth}|}
\hline
$\ABdcat$ & Abstract \\
\hline
$\ACCdcat$ & Accomplishment \\
\hline
$\ACHdcat$ & Achievement \\
\hline
$\APOdcat$ & Agentive Physical Object \\
\hline
$\AQdcat$ & Abstract Quality\\
\hline
$\ARdcat$ & Abstract Region\\
\hline
$\ASdcat$ & Arbitrary Sum \\
\hline
$\ASOdcat$ & Agentive Social Object \\
\hline
$\EDdcat$ & Endurant \\
\hline
$\EVdcat$ & Event \\
\hline
$\Fdcat$ & Feature \\
\hline
$\Mdcat$ & Amount Of Matter \\
\hline
$\MOBdcat$ & Mental Object \\
\hline
$\NAPOdcat$ & Non-agentive Physical Object \\