ao_bfo_dolce_mappings_v0.1.tex

% 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{natbib}
\usepackage{rawfonts}
\usepackage{stmaryrd}
\usepackage{amsmath,txfonts,bbm}
%\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{\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 \dolceAxLabel\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{\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{fobj}}
\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{\bforigid}{\pr{RG}}
\newcommand{\bfoisa}{\pr{ISA}}
\newcommand{\bfodisj}{\pr{DJ}}

\newcommand{\bfotime}{\textsc{tm}}

\newcommand{\bfocpart}{\pr{cP}}
\newcommand{\bfocppart}{\pr{cPP}}
\newcommand{\bfocdisj}{\pr{cDJ}}
\newcommand{\bfocoverlap}{\pr{cO}}
\newcommand{\bfoopart}{\pr{oP}}
\newcommand{\bfooppart}{\pr{oPP}}
\newcommand{\bfoooverlap}{\pr{oO}}
\newcommand{\bfotpart}{\pr{tmP}}
\newcommand{\bfotppart}{\pr{tmPP}}
\newcommand{\bfotdisj}{\pr{tmDJ}}
\newcommand{\bfotoverlap}{\pr{tmO}}
\newcommand{\bfompart}{\pr{mP}}
\newcommand{\bfoexist}{\pr{EX}}
\newcommand{\bfoiof}[1]{{\,::_{#1\:\!}}}
\newcommand{\bfoinh}{\pr{INH}}
\newcommand{\bfosdep}{\pr{SDEP}}
\newcommand{\bfogdep}{\pr{GDEP}}
\newcommand{\bfooccurs}{\pr{OCCIN}}
\newcommand{\bfolocated}{\pr{LOC}}
\newcommand{\bfosregof}{\pr{SREG}}
\newcommand{\bfosregofocc}{\pr{SREG_O}}
\newcommand{\bfotregof}{\pr{TREG}}
\newcommand{\bfostregof}{\pr{STREG}}
\newcommand{\bfoparticin}{\pr{PTC}}
\newcommand{\bfoconcr}{\pr{CONCR}}
\newcommand{\bforealizes}{\pr{REAL}}
\newcommand{\bfotproj}{\pr{TPROJ}}
\newcommand{\bfosproj}{\pr{SPROJ}}
\newcommand{\bfohistory}{\pr{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]{masolo@loa.istc.cnr.it}
\thanks{Corresponding author. E-mail masolo@loa.istc.cnr.it.}},
%\thanks{Corresponding author. \printead{e1}.}},
\author[B]{\inits{A.} \fnms{Francesco} \snm{Compagno}}, %\ead[label=e2]{francesco.compagno@unitn.it}}
\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 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 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 study 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 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 clarify the implicit choices on which the two systems or datasets rely, and to use logical and philosophical strategies to overcome possible mismatch whenever possible. 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 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 develop 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{OWL}. 
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 investigated in 2002~\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 top-level ontology 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 developed in early 2000 as part of the European project `WonderWeb'\footnote{\url{http://wonderweb.man.ac.uk/index.shtml}} and published in 2002 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.

The {\bfo} terms tend to be long strings. This makes hard for humans to parse the logical formulas. For this reason, we shorten the terms 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}. 
The classes of \emph{particulars} and \emph{universals} are represented in {\bfo} by unary predicates and not by individual constants: to distinguish them we introduce $\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
$\pr{PREC}(x,y)$ & $x$ precedes $y$ & precedes\\
\hline
$\pr{FINST}(x,y)$ & $x$ is the first instant of $y$ & firstInstantOf\\
\hline
$\pr{LINST}(x,y)$ & $x$ is the last instant of $y$ & lastInstantOf\\
\hline
$\pr{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 \\\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 {\color{red} XXXX}. For a more human-accessible version refer to \citep[ch.2]{D24}.}\nb{add sito web in footnote} 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). 

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 \\
\hline
$\NASOdcat$ & Non-agentive Social Object \\
\hline
$\NPEDdcat$ & Non-physical Endurant \\
\hline
$\NPOBdcat$ & Non-physical Object \\
\hline
$\PDdcat$ & Perdurant \\
\hline
\end{tabular}
\end{minipage}%
\mbox{}\hfill{}
\begin{minipage}{0.45\textwidth}
\hspace{-12pt}\begin{tabular}{|p{.10\textwidth}|p{.60\textwidth}|}
\hline
$\PEDdcat$ & Physical Endurant \\
\hline
$\POBdcat$ & Physical Object \\
\hline
$\PQdcat$ & Physical Quality\\
\hline
$\PRdcat$ & Physical Region\\
\hline
$\PROdcat$ & Process\\
\hline
$\Qdcat$ & Quality \\
\hline
$\Rdcat$ & Region \\
\hline
$\Sdcat$ & Space Region \\
\hline
$\SAGdcat$ & Social Agent \\
\hline
$\SCdcat$ & Society \\
\hline
$\SOBdcat$ & Social Object \\
\hline
$\SLdcat$ & Spatial Location \\
\hline
$\STdcat$ & State \\
\hline
$\STVdcat$ & Stative \\
\hline
$\Tdcat$ & Time Interval \\
\hline
$\TQdcat$ & Temporal Quality \\
\hline
$\TLdcat$ & Temporal Location \\
\hline
$\TRdcat$ & Temporal Region \\
\hline
\end{tabular}
\end{minipage}%
\end{table*}
%Mereology%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}
\begin{small}
\hspace{-4pt}\xymatrix@R=10pt@C=0pt{
&&&&&&& \circ \ar@{-}[dllll] \ar@{-}[dl] \ar@{-}[drrr] \ar@{-}[drrrrrr]\\
&&&  \EDdcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr] & & &  \PDdcat \ar@{--}[dl] \ar@{--}[dr] &&&&  \Qdcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr] &&&  \ABdcat \ar@{--}[d]\\
  & &  \PEDdcat \ar@{--}[d] \ar@{--}[dl] \ar@{--}[dll] & \NPEDdcat \ar@{--}[d] & \ASdcat &  \EVdcat \ar@{--}[d] \ar@{--}[dr] & &  \STVdcat \ar@{--}[d] \ar@{--}[dr] & & \TQdcat \ar@{--}[d] & \PQdcat \ar@{--}[d] & \AQdcat & & \Rdcat \ar@{-}[d] \ar@{-}[dl] \ar@{-}[dr]\\
\Mdcat & \Fdcat & \POBdcat \ar@{-}[d] \ar@{-}[dl]  &  \NPOBdcat \ar@{--}[d] \ar@{--}[dr]  & & \ACHdcat & \ACCdcat & \STdcat & \PROdcat & \TLdcat & \SLdcat & & \TRdcat \ar@{--}[d] & \PRdcat \ar@{--}[d] & \ARdcat \\
& \APOdcat & \NAPOdcat & \MOBdcat & \SOBdcat \ar@{-}[d] \ar@{-}[dl]&&&&&&&&  \Tdcat & \Sdcat\\
&&& \ASOdcat \ar@{--}[d] \ar@{--}[dr] & \NASOdcat \\
&&& \SAGdcat & \SCdcat \\
}
\end{small}
\caption{Taxonomy of {\dolce} (vertical lines stand for ISA relationships, solid lines indicate a partition).}\label{fig_tax_dolce}
\end{figure}

\subsection{Notation}
In the paper we adopt the following notation to referencing formulas: ({\rm a}$x$), ({\rm t}$x$) and ({\rm d}$x$), followed by an integer, identify axioms, theorems, and syntactic definitions, respectively, in the order in which they are listed in the theories. More specifically,
\begin{itemize}
\item (\bfoAxLabel $x$), (\bfoThrLabel $x$), (\bfoDefLabel $x$) are used for axioms, theorems, and definitions of $\thbfo$ (index $b$ stands for $\bfo$); 
\item (\dolceAxLabel $x$), (\dolceThrLabel $x$), (\dolceDefLabel $x$) are used for axioms, theorems, and definitions of {$\thdolce$} (index $d$ stands for $\dolce$); 
\item %(\dbAxLabel $x$), (\dbThrLabel $x$), 
(\dbDefLabel $x$) define %are used for axioms, theorems, and definitions used in 
the mapping  from ${\thdolce}$ to ${\thbfo}$; and
\item %(\bdAxLabel $x$), (\bdThrLabel $x$), 
(\bdDefLabel $x$) define %are used for axioms, theorems, and definitions used in 
the mapping  from ${\thbfo}$ to ${\thdolce}$.  
\end{itemize}
where by mapping we mean the formal counterpart of the alignment of (a part of) one ontology to (a part of) the other such that {\bf XXXXX}\nb{SB: qui serve una spiegazione di qualche riga su cosa intendiamo con il termine alignment (che usiamo in modo informale) e mapping (che usiamo in modo formale), bisogna almeno dare l'intuizione}. Thus, we say that one ontology is aligned to another when there is an explicit mapping from (part of) the first to the second.\nb{controllare!!}

%===================================
\section{The general strategy and the role of methodological assumptions for the alignment of TLOs}\label{sect_methodology}
%===================================

%The purpose of the report is to present the consolidated formal systems of the two covered TLOs and the alignment across these systems. Indirectly, it also serves as a guideline for the alignment of other TLOs that might be interested in joining the ontology network.

%In the previous sections we have introduced the Common Logic versions of {\bfo} and {\dolce}. 
Before introducing the alignment (that is, providing the mapping) and presenting the difficulties we encountered to develop it, we provide the assumptions, strategy, and further considerations that are behind this work.\nb{SB: changed} These observations motivate the choices made in building the mappings and determine in which sense the result is correct.

The approach is centred on the CL-versions of the two ontologies. These, with their explanatory documentation, are taken as the primary sources of information on the ontologies and are considered in our strategy from the start. 
Here are the steps that characterize an alignment strategy\footnote{The steps are ideally performed in order but, due to the complexity of the work, in many cases one has to cycle among the steps}:
% a first step consists in the following steps% report was developed following these steps:
\begin{enumerate}[({\bf S}1)]
%\item The versions in Common Logic of the {\bfo} and {\dolce} ontologies were collected from the groups that developed them. The choice to use Common Logic is the result of several considerations including 
%%the fact 
%that Common Logic is a consolidated standard (\url{https://www.iso.org/standard/66249.html}) and that the visibility and stability of standards increases users' trust in the OCES system.
%\item Ontologies with a stable reference version were compared to the version in Common Logic to highlight relevant changes. This case applies to {\dolce} whose reference version was released in 2003 in first-oder modal logic. The version in Common Logic is an adaptation due to the reduced expressivity of Common Logic.
%\item Formal primitive relations were listed.
\item analyze the CL-axioms together with the available documentation\footnote{In our case, \citep{barryBasicFormalOntology2015} and \citep{D18} for {\bfo} and {\dolce}, respectively.}\nb{CM: non sono riuscito a trovare dove è disponibila la versione aggiornata che spiega BFO 2020 che abbiamo usato noi [FC:  esiste tale versione? Io ho solo trovato questo sito https://basic-formal-ontology.org/bfo-2020.html che contiene anche ISO scaricabile.]}\nb{SB: non è quella fornita Alan su github?} to ensure proper understanding of the intended interpretations of the primitives of the two ontologies; % (in case of incongruences across documents, the statements of the formal theory have priority);
 \item establish and document the methodological choices;
%where 
\item introduce formal mappings from one ontology to the other (and vice versa) with a description of what is aligned;
\item test (manual or with theorem provers) that the set of mappings is coherent and aligns what is intended;
\item re-evaluate if the set of mappings can be further generalized.
\end{enumerate}

The strategy ({\bf S}1)-({\bf S}5) is clearly underspecified. To become operative, one has to give the methodological choices which determine the kind of alignment is sought (and how it can be verified). For instance, one may want to align the terminology, the primitives, the concepts, the inferences, the (intended) domains or even the whole models of the ontologies. This kind of choice leads to pay attention to some features of these systems leaving aside others. Generally speaking, the strategy ({\bf S}1)-({\bf S}5) may generate two incompatible mappings when applied to preserve distinct features.
In particular, one has to state what happens in case of inconsistencies across the available documentation. One may decide that the description in natural language is the most reliable of the authors' intentions. Others may insist that the formal theory has priority since it is the only one that can be tested for consistency. Furthermore, the documentation might not be precise or detailed on aspects relevant for the alignment since the latter depends also on how the other ontology is developed. For instance, during the construction of the {\bfo} and {\dolce} alignment that we present in the next sections, the intended interpretation of some concepts was unclear to the alignment developers and clarifying questions were sent to the ontology authors to collect further information. This approach might not always be possible and, even so, it might not solve all cases (sometimes the authors of an ontology might not have a ready answer especially if the question raises foundational problems). %Generally speaking, an alignment methodology should explicitly state how to manage this situation.}


Here are the assumptions %\nb{SB: il termine "methodological assumptions" non mi piace molto}\nb{CM: si può togliere methodological} 
adopted in this paper to align {\bfo} and {\dolce}. Note that the assumptions ({\bf M}1)-({\bf M}3) are not mutually independent since they contribute to define a coherent characterization of the alignment goal which, in this case, is {\em domain focused}. 
%
\begin{enumerate}[({\bf M}1)]
\item \label{Ass1} %In this alignment\nb{CM: cosa vuol dire? quale sarebbe questo alignment?}, 
Given an analysis of the documentation and the examples in the ontologies, any elicited informal correspondence across the notions of the two ontologies 
is assumed to provide a basis for a mapping of categories and relations of one ontology into the other. 
For instance, \emph{occurrents} 
%(\emph{continuants}) 
are described and used, in the {\bfo} formal system and accompanying documentation, in a way that is conceptually similar to that of \emph{perdurants} in the {\dolce} formal system and documentation.
%(\emph{endurants}) 
This similarity is taken as an informal correspondence and leads to consider the alignment of the {\bfo} occurrent category to the {\dolce} perdurant category. (Note that such a correspondence might be suggested by common examples in the two ontologies, or even be based on the comparison of relevant relations which are, perhaps for different reasons, considered similar like the {\bfo} relation \emph{continuantPartOf} and the {\dolce} relation \emph{temporary parthood}). 

\item \label{Ass2} A mapping aims to %must\nb{CM: mi sembra forte, c'è solo un tendere a massimizzare l'overlap tra domini} 
embed all (or most of) the members of a category of the \emph{source} ontology (e.g., {$\thdolce$} in the case of Sect.~\ref{sect_d2b}) in the domain of quantification of the \emph{target} ontology ({$\thbfo$} in Sect.~\ref{sect_d2b}). In other terms, the purpose is to maximize the coverage of the entities of one ontology by the domain of the other ontology. 
Given this scenario, the study of which axioms of the target ontology hold or fail after the mappings from point (M\ref{Ass1}) are formalized, highlights genuine differences between the ontological commitments of the two ontologies (at least relatively to the CL language), and which entities of the source ontology are problematic in, or even incompatible with, the target ontology.   

\item \label{Ass3} Only mappings that can be formalized in FOL as syntactic definitions are considered. %This means that we explore the connection between the entities of the source ontology that can be mapped into the domain of the target ontology. 
Meta-modeling techniques, like the application of abstraction processes or set-theoretical (second-order) constructions to enrich the domain of the source %(or target\nb{SB: ho aggiunto, ci sta?}\nb{CM: non lo so, se ci sono entità in meno nella target, semplicemente non mappo alcune della source, poi è nel link inverso che le introduco, ma non ci ho pensato; inoltre, non sono sicuro che le second-orders definitions estendano sempre il dominio})\nb{SB: ho tolto, non è rilevante} 
ontology with additional entities, are not considered. %These techniques usually require . This change raises concerns about the actual correspondence between the ontological commitments of the source ontology and that of the theory with the enriched domain. 
Since mappings are sets of syntactic definitions, theorem provers can be used to verify which axioms of the target ontology are preserved by the mappings.%\nb{CM: questo ultimo commento non mi convince, abbiamo cercato di restare a FOL perché: (1) possiamo sperare di farci aiutare dai TPs; (2) sfruttiamo l'idea classica di definitional extension (invece che passare a teoremi di rappresentazione che comunque avrebbero senso) [FC: non so seguirti sul punto (2) (teoremi di rappresentazione = ?, in questo contesto), né su M\ref{Ass3} originale. PEr punto (1) ho messo frase sui TP]} 
\end{enumerate}

Note that the assumptions (M\ref{Ass2}) and (M\ref{Ass3}) are interrelated and are seen from the perspective of an interactive development of mappings that starts with the analytical step (M\ref{Ass1}). 

\subsection{General observations learned from the alignment of {\bfo} and {\dolce}}
The alignment between large ontologies present a formal and a conceptual challenge: the formal challenge consists of the identification and the verification of the mappings; the conceptual challenge refers to the choice among alternative mapping options.
For instance, in Sect.~\ref{sect_analysis_d2b} and Sect.~\ref{sect_analysis_b2d}, where the alignment of {\bfo} and {\dolce} are presented, we discuss some mappings which have not been adopted in our alignment. These mappings modify (by restricting or expanding the mappings proposed in, respectively, Sect.~\ref{sect_mappings_d2b} and Sect.~\ref{sect_mappings_b2d}) the way some notions of the target ontology are modeled in terms of the ones of the source ontology. 
In particular, these alternative mappings presents possible solutions (or improvements) to the partiality of the alignments developed in Sect.~\ref{sect_d2b} and Sect.~\ref{sect_b2d}. Furthermore, formal constructions (definitely more complex) can be implemented to extend the domain of the source ontology to resemble more closely the domain of the target ontology, facilitating a richer mapping across these systems. This result can be achieved also by allowing to define in the source ontology the primitives of the target ontology via reference to newly introduced entities. This situation is not specific to the alignment of {\bfo} and {\dolce}. Instead, it is a strategic choice that one has to consider when specialising the strategy to follow.
%\nb{CM: qui cosa volevamo dire? [FC: non ne ho idea, forse fa riferimento a quando nel testo parli di introdurre e.g. coppie di cose. Io taglierei frase]} 
%In the context of the OCES framework, the alignment strategy to be exploited is exemplified by the mapping from {\bfo} to {\dolce} and by the mappings from {\dolce} to {\bfo} carried out in Sect.~\ref{sect_d2b} and in Sect.~\ref{sect_b2d}.
 
%Discuss here the general strategy followed in this first draft: (-1) illustrate what we will do technically; (0) `maintain' as much entities as possible from {\dolce}; (1) critical choice of mappings and idea of trying to match has much as possible intuitive correspondence between categories and primitive relations (e.g., $\cntbcat$/$\EDdcat$, $\occbcat$/$\PDdcat$, $\bfoopart$/$\Pd$, $\bfocpart$/$\TPd$); (2) look at which ones of the original {\bfo}-axioms are not valid in the {\dolce}+mappings and try to understand the motivation; (3) individuate alternative mappings (modifying the `imported' entities or the relations) that try to fix some of these dis-alignments.

Assumption (M\ref{Ass3}) may be better understood if we compare two approaches to extend a theory via definitions. 
Recall that the goal is to have formulas in the source ontology that capture (or best approximate) the concepts in the target ontology. In this example, we take {$\thdolce$} as the source ontology and {$\thbfo$} as the target ontology. (Analogous considerations hold for the other direction.)

The first approach, which we adopt in this paper, is to extend theory $\thdolce$ with a set of syntactic definitions---the mappings in Sect.~\ref{sect_mappings_d2b}---, which inject {$\thbfo$} primitives into {$\thdolce$}, i.e., these definitions are introduced as a way to `understand' the {$\thbfo$} primitives in the {\dolce} language. 
We use the symbol {$\sdef$} \,for these syntactic definitions and treat them as `parametric macros'. That is, one can simply substitute at the syntactic level the \emph{definiens} for the \emph{definendum}. Note that these syntactic definitions have parameters which must be suitably matched. For instance, suppose we aim to define the primitive of parthood on occurrents in {$\thbfo$} via formula $\bfoopart(x,y) \sdef \phi(x,y)$. As we know, the lefthand side (namely, $\bfoopart(x,y)$) a primitive in {$\thbfo$}. Let us assume that $\phi$ is an expression in the language of {$\thdolce$} with $x$ and $y$ as the only free variables. %\footnote{We assume the usual constraints for syntactic substitution in FOL, e.g., see \cite{?}.}\nb{CM: Serve questa nota? In caso aggiungere riferimento} 
In this case, $x$ and $y$ are treated as parameters and the formula $\forall zw(\bfoopart(z,w) \land \bfoopart(w,z) \to z=w)$ in the language of {$\thbfo$} becomes formula $\forall zw(\phi(z,w) \land \phi(w,z) \to z=w)$ in the language of {$\thdolce$}. Similarly, {$\thbfo$}-formula $\bfoopart(\cn{proc\#1},\cn{proc\#2})$ becomes {$\thdolce$}-formula $\phi(\cn{proc\#1},\cn{proc\#2})$. 

The second approach consists in adding these syntactic definitions as new formulas in the source ontology, obtaining a definitional extension of the source theory. %that is an `extension by definitions'. 
It suffices to turn our syntactic definitions in biconditionals rather than syntactic definitions as described above. Syntactically, this means to use the $\ifif$ symbol (if and only if) instead of the $\sdef$ symbol, and to close the expression by adding universal quantifiers for all the free variables. For example, in the previous example one would add the entire formula $\forall xy(\bfoopart(x,y) \ifif \phi(x,y))$ directly into the source theory. The two approaches are quite similar. The advantage of using syntactic definitions instead of extensions by definitions is that the vocabulary of the theory in which we introduce the syntactic definition does not change. Using the `if and only if' clause automatically adds the defined predicates to the ontology language (e.g., we would add the {$\bfo$}-predicate $\bfoopart$ into the {$\dolce$} vocabulary when using the biconditional in the previous example). In Sect.~\ref{sect_problem_univ} we will see that this latter approach may add new ontological commitments with important consequences, in particular on the view of universals.

Once {$\thdolce$} has been extended with these syntactic definitions (and possibly further syntactic definitions already present in {$\thbfo$})---we dub $\thdolcedbmap$ such extension---it is possible to check how much of the theory $\thbfo$ is preserved: each axiom in $\thbfo$ expressible\footnote{We will see in Sect.~\ref{sect_mappings_d2b} that this mapping is only partial.} in $\thdolcedbmap$ is proved or disproved in $\thdolcedbmap$. The analysis in Sect.~\ref{sect_analysis_d2b} of the preserved/non-preserved axioms allows, modulo the introduced mapping, to highlight and understand similarities and divergences between the two ontologies. The mapping in the other direction, i.e., the extension $\thbfobdmap$ with the syntactic definitions of {$\dolce$}-primitives in terms of {$\bfo$}-primitives, is formalized in Sect.~\ref{sect_b2d}. The combined analysis of the mappings {\dolce}-into-{\bfo} and {\bfo}-into-{\dolce} points out genuine ontological differences as well as problematic aspects of the adopted technique. 

These observations hold beyond the {\bfo} and {\dolce} case. Also, the general strategy can be iterated to further refine the mappings and to solve, as far as possible, false cases of agreement or disagreement.

%======================================
\subsection{Use of theorems provers and model builders}
%======================================

The material presented in the next sections is tested using two theorem provers for FOL, namely, Prover9\footnote{\url{https://www.cs.unm.edu/~mccune/prover9/}} and Vampire\footnote{\url{https://vprover.github.io/}}. For the generation of models and countermodels, the software Mace4\footnote{\url{https://www.cs.unm.edu/~mccune/prover9/}} was used.
According to the literature \citep{Sut16} and in our experience, Vampire is generally faster than Prover9. However, we experienced that, for some of the proofs we asked the provers to demonstrate, Prover9 performed better then Vampire.\nb{CM: @Francesco, forse spiegare meglio in che senso è meglio FC:riscritto} Furthermore, Prover9 proofs are generally shorter and easy to read. To this contributes the (optional) syntactic choice of assuming that the non-quantified variables of formulas are universally-quantified).\nb{CM: non sono sicuro di capire, nel senso che non si riportano i quantificatore per le variabili univ. quantificate? FC: riscritto}\nb{SB: ho indebolito, da ricontrollare} Therefore we kept using both provers. 

%The provers are used in order to infer a logical consequence from a set of axioms. %Since first-order logic is semi-decidable the provers are not guaranteed to prove or disprove the inference of an axiom from a set of premises so the automated provers cannot be expected to prove or disprove all theorems.

Our methodology to use these software packages (provers) is as follows. We rewrite all axioms and definitions of {$\thdolce$} and $\thbfo$ in the syntax accepted by the software (Vampire accepts tptp \citep{Sut16}\nb{CM: saltato riferimento, @Francesco, puoi aggiungre? FC:cambiato}, Prover9 uses its own syntax).
%and we submit this translation together with the translation of the theorem to\nb{CM: qui c'era un problema?}  %used them as antecedents as inputs for 
%the theorem prover. We repeated this procedure for all theorems and the provers returned the proofs listed in Section \ref{sec:dolce_theorems}. 
To prove a theorem regarding the mappings from {\dolce} to {\bfo}, we add to the tptp or Prover9-syntax version of {\dolce} \nb{CM: non ho capito di che rewriting si tratta} the translations, in the appropriate syntax, of both the mappings in Sect.\ref{sect_mappings_d2b} and the theorem (i.e., we rewrite the whole $\thdolcedbmap$ plus the theorem). 
%then add the rewriting of the statement (that we already proved by hand)
\nb{FC: non mi ricordo di aver scritto la vecchia frase. Comunque non è corretta: solo alcuni teoremi soon stati dimostrati a mano prima di sottoporli al prover. Ho riscritto e commentato la vecchia versione} 
Then we submit this large theory to the software and ask it if the theorem follows from the other axioms. 
We proceed similarly in the case of the mappings from {\bfo} to {\dolce}. The documentation we provided in the appendix of \cite{D24}\nb{CM: che cosa sarebbe? FC: tipo l'appendice del deliverable di ontocommons, oppure citare quello: ho citato D24, in caso aggiungere link a appendice} refers to these automatically generated proofs.
%the same, but we also added the definitions of {\bfo} and the definitions of the ({\dolce} to {\bfo}) mapping in the input of the provers. In this case, the proofs were more difficult, and t
When the provers do not find a proof of a statement, and this happens in several cases, we provide a manual proof. Some of the manually generated proofs are verified by at least one prover by adding intermediate lemmas (which are also automatically verified). %All verified proofs are reported in Section \ref{db_mappings}.\nb{FC: At this moment not all manual proofs have been verified in this way.} 

To formally verify counterexamples of relevant sentences, we produce a counterexample by hand and then proceed in the following way: we write axioms (in the prover syntax) enforcing the existence of the exact number of individual constants required by the counterexample, as well as each and every relation holding among them. 
For sake of brevity, some of the relations are skipped by exploiting taxonomical axioms. That is, we add the axioms of the {$\thdolce$} (or  {$\thbfo$}) taxonomy, %to simplify our work, 
then, it is sufficient to specify to which leaf-level class of the taxonomy each constant belongs: the constant will automatically belong to each superclass and not belong to disjoint classes, thanks to the ISA relationship axioms holding between the classes of the taxonomy. Additionally, the disjunction axioms between the taxonomical classes spare us from stating that individuals belonging to disjoint classes are different (non-identity among different individual constants belonging to the same class must be still forced through appropriate axioms).\nb{CM: non ho capito questo, non è possibile avere due costanti dello stesso tipo foglia? FC: riscritto} In this way, we obtain a theory that syntactically describes the domain and the relationships at the core of the counterexample, which is complete by construction. 
At this point, we run Mace4 using all these axioms as input.\nb{CM: è vero questo? mi ricordavo che facevamo andare solo il prover FC: lo facevo girare senza i teoremi, prima divfar girare i prover} This software verifies that this (small) set of axioms is consistent and generates an explicit model.
Such a model is the only model (up to isomorphism) of the theory, because we take care that the theory is complete and the model is finite by construction.
Then, for each axiom of {$\thdolce$} (or $\thbfo$), we verify that such an axiom holds in that model, by asking the provers if the axiom follows from those axioms that specify the model, thus proving that the model is a model of {$\thdolce$} ($\thbfo$).\nb{SB: il testo era ambiguo e ho cambiato, controllate FC: ricambiato} 
Lastly, we check that in this model the sentence that we want to disprove is actually false (one may think that this step is not needed, essentially it guarantees that everything was done correctly)\nb{FC: in che senso non serve? O si verica a mano che è un contromodello o si verifica in automatic. A me non verrebbe da pensare che questo passo non serve.}.

Note that the standard way to generate counterexamples with Mace4, that is, by asking Mace4 to find a model of all the axioms of {$\thdolce$} ($\thbfo$) with the addition of the negation of the sentence to be disproved, does not work in most of our cases. In our experience, perhaps due to the complexity of these ontologies, the generation of a model requires an excessive computational effort.

%In Section \ref{db_counter_examples} we report the syntactic description of the models and not the semantic one, as it is too long and can be generated from the syntactic description using Mace4. Some models are counterexamples of more than one theorem, in those cases we list all the theorems they are counterexamples of. 
%
%In order to verify the mappings and the counterexamples corresponding to the opposite direction, that is, from {\bfo} to {\dolce}, we proceeded in the same way, and the results are shown in sections \ref{bd_mapping} and \ref{bd_counter_examples}. The only difference is that we used the formal axiomatisation of {\bfo} developed by its authors\footnote{\url{https://github.com/BFO-ontology/BFO-2020}}.

%Notice that the proofs use prefixed notation for the ternary (or binary, when the time argument is absent) predicate of instantiation, in place of the infixed syntax ($\bfoiof{}(x,y,t)$ in place of $x\bfoiof{t}y$).


All the proofs and models relative to our alignments are collected in \citep{??}.\nb{CM: mettiamo il del d2.4 in cui manca qualcosa o un rapporto?}\nb{a che punto è il d2.4?}

%===================================
\section{Preliminary considerations}\label{sect_prelim_considerations}
%===================================
This section presents a few points specific to the alignment of {\bfo} and {\dolce}. This allows us to introduce two problems related to the technical choices made in these systems, and to discuss the different levels at which these theories investigate some ontological classes. 
%Problem of the universals and problem of the different resolution of the ontologies in some subdomains.


%%===================================
%\subsection{Preliminary remarks}
%%===================================

%===================================
\subsection{Representation of categories}\label{sect_problem_univ}
%===================================

In  {$\dolce$} the categories in  Table~\ref{table_cat_dolce} are represented by means of FOL unary predicates. These categories are disjoint and assumed to correspond to rigid properties, that is, an entity cannot change its taxonomic classification. In other terms, if an entity belongs to a category, it must belong to that category from the time it starts to exist to the time it ceases to exist (if any). To state that an entity $x$ is an endurant, one formally writes $\EDdcat(x)$. Similarly for the other categories.
%TOLTO
%\nb{CM: check if the CL version imposes categories to be non-empty} 

In {$\bfo$}, all the universals in Table~\ref{table_cat_bfo} are in the domain of quantification and a temporary \emph{instance-of} primitive relation (written $\bfoiof{}$) is introduced to represent when %a particular 
an individual is an instance of a universal at a given time. For instance, the fact that ``at time $t$, $x$ is a continuant'' is formally written $x \bfoiof{t} \cntbcat$, where $\cntbcat$ corresponds to the universal \emph{being a continuant}.
{\bfo} universals are non-empty and rigid through time %(see Sect.~\ref{bfo_rigidity_univ}) 
with the exception of $\objbcat$, $\objaggbcat$, and $\fobjbcat$. For instance, a material entity could belong to $\objbcat$ at some time, and later to $\objaggbcat$ (or $\fobjbcat$) and, perhaps, change again later, provided at each point in time it is classified by one and only one of these three universals.

These different representational choices raise an initial problem because, according to (M\ref{Ass3}), one should individuate to which kind of {\dolce} entities the {\bfo} universals correspond (Sect.~\ref{sect_analysis_d2b} adds further considerations on this point). 
We consider only 
%on 
the {$\bfo$}-universals present in the taxonomy, and start from the subset that can be defined in {$\dolce$}. 
For each universal $\cn{u}$, a syntactic definition of form $x \bfoiof{t} \cn{u} \sdef \phi(x,t)$ is introduced. Note that here the `parameters' are $x$ and $t$, while $\cn{u}$ is a constant. This means that, first, we do not define the notion of instance-of but 
define only the instantiation of a given $\cn{u}$. That is, in general, the definitions of $x \bfoiof{t} \cn{u_1}$ and  $x \bfoiof{t} \cn{u_2}$ could be different. 
Second, as discussed earlier, $\cn{u}$ will not appear in $\phi(x,t)$ and thus will not become an individual in the domain of {$\dolce$}. If we were to use the biconditional conditions, writing $x \bfoiof{t} \cn{u} \ifif \phi(x,t)$ in the theory, both the predicate $\bfoiof{}$ and the individual constant $\cn{u}$ would be added to the vocabulary of {$\dolce$}, and this would imply to have some universal in the domain of {$\dolce$}. 

A way to avoid this problem is to substitute $\pr{U}(x,t) \sdef \phi(x,t)$ for $x \bfoiof{t} \cn{u} \ifif \phi(x,t)$, i.e., to map the needed {\bfo} categories to {\dolce} predicates, and the instance-of relation to (logical) predication. %\footnote{This could generate some problems if {\bfo} universals are intensional (vs.~extensional) properties. However this aspect does not emerge from the {\bfo} axioms.}
We adopt the first strategy because it is closer to the formalization in $\thbfo$, and it avoids
%in Sect.~\ref{sect_bfo}, we write $x \bfoiof{t} \cn{u}$ instead of $\pr{U}(x,t)$ (see, for instance, \refdbdf{d2b_pbnd} and \refdbdf{d2b_proc} in Sect.~\ref{sect_mappings_d2b}). However, it must be clear that this is just a notational convention that requires neither 
to include universals in the domain of {$\dolce$} as well as the relation instance-of among the primitives of {$\dolce$}.
% (as said, we represent instance-of by means of predication).  

In this perspective, {$\bfo$} axioms quantifying over universals %(see, especially, Sect.~\ref{bfo:instance+exists}) 
are disregarded by the mappings. Weaker versions of some of these axioms are introduced by considering the (finite) set $\{\cn{u_1}, \dots, \cn{u_n}\}$ of those universals explicitly used to generate the mappings. For instance, $\exists xt(x \bfoiof{t} \cn{u_1}) \land \ldots \land \exists xt(x \bfoiof{t} \cn{u_n})$ can replace  the following axiom:\footnote{[mbf-1] is the label originally adopted in $\bfo$ to refer to this axiom. In the following we always indicate these labels.}
%\refbfoax{univ_are_insta}:
%\nb{CM: still some of these axioms are not present in sect. \ref{sect_check_bfo_preservation}}
%
\bflist
\item[\bfoax{univ_are_insta}] $\bfouniv(u) \to \exists xt(x \bfoiof{t} u)$ \hfill {\scriptsize [mbf-1]}
\eflist

%$x \bfoiof{t} \cn{u} \sdef \phi(x,t)$  (see, for instance, \refdbdf{d2b_pbnd} and \refdbdf{d2b_proc} in Sect.~\ref{sect_mappings_d2b}). Note that $\cn{u}$ is not in $\phi(x,t)$ and universals are not in the {\dolce} domain as maybe the form of the definition could suggest. A different way to look at these definitions is to consider the form $\cn{u}(x,t) \sdef \phi(x,t)$, i.e., they introduce a new predicate for each considered universal. We opted for the first form to be closer to the formalization of {\bfo} in Sect.~\ref{sect_bfo}.
%
% and where $\cn{u}$ is one  (see the relative mappings s of instantiation of these universals like, for instance, the following  \refdbdf{d2b_pbnd} or \refdbdf{d2b_proc}. The universals in the {\bfo}-taxonomy are then represented in {\dolce} by means of corresponding predicates. For instance,  $x \bfoiof{t} \procbcat$ can be intuitively seen in {\dolce} as $\procbcat(x,t)$.   


%===================================
\subsection{Different ontological focus and resolution}\label{sect_diff_resolution}
%===================================

The informal categorical distinctions in {\dolce} and {\bfo} are quite similar. The presentations of {\bfo} occurrents and {\dolce} perdurants are very close. This observation is further supported by the fact that both the ontologies introduce a primitive of parthood simpliciter for these entities (relation $\Pd$ in {$\dolce$} and $\bfoopart$ in {$\bfo$}). 
Analogously, we notice a similarity between {\bfo} continuants and {\dolce} endurants, given that both ontologies conceive the temporary parthood relation as a primitive ($\TPd$ in {$\dolce$} and $\bfocpart$ in {$\bfo$}).
Things are different for temporal/spatial  regions and qualities. At first sight, these categories appear to be similar. Formally, they are classified in different ways in the two ontologies. 
{$\bfo$} classifies qualities (and, more generally, specific dependent continuants) and spatial regions under continuants while temporal regions are classified under occurrents. In {$\dolce$}, temporal regions, spatial regions, and qualities are neither endurants nor perdurants.\footnote{We will resume this issue in more detail below when we discuss spatiotemporal regions.} In particular, temporal regions and spatial regions are abstract entities in {$\dolce$}. This difference---mainly grounded on the way the distinction between endurants/continuants  and perdurants/occurents is characterized---complicates the comparison and needs to be taken into account in defining the mappings (this can be seen, for instance, at p.\pageref{d2b_exist} the definition \refdbdf{d2b_exist} in $\thdolcedbmap$ relative to primitive $\bfoexist$ of {$\thbfo$}).      

How the most general categories (endurants/continuants on the one hand, perdurants/occurrents on the other hand) are specialized diverges considerably in the two ontologies:

\paragraph{On perdurants vs.~occurrents} In {\dolce} perdurants are specialized mainly on the basis of two notions, both extensively discussed in the linguistic and philosophical literature: \emph{homeomericity} (roughly, any temporal part of a perdurant of a certain kind is a perdurant of the same kind) and \emph{cumulativity} (roughly, the mereological sum of perdurants of a certain kind is a perdurant also of the same kind); in {\bfo} processes are distinguished from process boundaries mainly based on the dimensionality of their temporal locations and on the fact that they are temporal proper parts of other occurrents.

\paragraph{On endurants vs.~continuants} The spatial and material dimensions of this kind of entities play a central role in both {\dolce} and {\bfo} (see Sect.~\ref{sect_analysis_d2b} for their differences). {\dolce} presents a finer taxonomy mainly aimed to cover the notions of agentivity and sociality. {\bfo}, which is driven by the distinction between fiat vs.~bona fide entities, explicitly introduces the notion of aggregate, and relies on the dimensionality of the spatial (rather than temporal) location to distinguish sites vs.~continuant fiat boundaries.

\paragraph{On qualities} The branch of the taxonomy for qualities in {\dolce} is detached from that of endurants and continuants, differently from {\bfo}, and is motivated by the \emph{comparability} principle: it makes sense to compare the color of a rose and the color of a vase, it does not make sense to compare the color of a rose and the weight of a vase. Qualities are clustered in terms of maximal comparability, e.g., colors, weights, lengths, shapes, etc. form different quality types. Spaces of regions have a structure and are associated accordingly, e.g., for colors, the space has regions for red, blue, green, etc. Instead, {\bfo} distinguishes classes of specifically dependent continuants according to the existence, the nature of, and the participants in their realization processes.

\smallskip
These different ways of classifying entities are not incompatible \textit{per se}. For instance, one could consider cumulativity, agentivity, comparability in {\bfo}, and dimensionality of temporal/spatial regions and realization processes in {\dolce}. But, clearly, this approach requires extending {\bfo} and {\dolce}, a choice that should be pondered carefully. The approach based on ontology extension is not exploited in the alignment we present here. The consequence is that some primitive notions and categories of the target ontology cannot be defined in terms of those in the source ontology. This leads to developing a mapping that focuses on the general notions and categories of the two ontologies.
   





% Formally, both {\bfo} and {\dolce} consider, respectively, temporary parthood for continuants and endurants and parthood simpliciter for occurrents and perdurants.
%


%Second, some of the axioms above can be problematic for the mappings because {\dolce} does not consider universals in the domain of quantification. However, the {\bfo}-taxonomy considers only a small number of universals (and the mappings concern only subset of these). We can then consider the following simplifications.
%%
%\bflist
%\item[--] Instead of \refbfoax{iof_args} and \refbfoax{exist_ifif_iof}, we consider: 
%%
%
%\item[--]  \refbfoax{partic2exist} follows from \refbfoax{cnt_to_exist}, \refbfoax{occ_to_exist}, and \refbfoax{cont+occ_iff_pt}.
%
%
%\item[--] The left to right direction of \refbfoax{exist_ifif_iof} would then follow from \refbfoax{exist_args} and \refbfoax{cont+occ_iff_pt}. 
%
%\item[--] Given \refbfoax{exist_ifif_iof}, \refbfoax{iof_time_dissective} can be substituted by \refbfoth{exist_time_dissective}.


%The following mappings will then consider a modified version of $\thbfo$, namely $(\thbfo \setminus \{$\refbfoax{time}-\refbfoax{iof_time_dissective}$\})\cup \{$\refdbax{cont+occ_iff_pt}-\refdbax{maten2exist_db}$\}$.


%{\color{red} ****add a note to make explicit that we do not consider universals in the domain of quantification and that then we define only $x \bfoiof{t} u$ only for the finite set of universals explicitly considered in the taxonomy of {\bfo}} 

%===================================
\section{The mapping from {\dolce} to {\bfo}}\label{sect_d2b}
%===================================

%In this Section we will analyze how and what categories and primitive relations of {\bfo} can be mapped to the ones of {\dolce}. 

%{\color{red} ****add something to explain the structure of the section}
This section presents the technical results of the establishment of a mapping from {\dolce} to {\bfo}, that is, it shows how to define in {$\dolce$} the categories and primitive relations of {$\bfo$}. As anticipated, the mapping does not cover all categories and relations. 
In other terms, the starting point is the domain of {\dolce}, and the goal is to classify and relate the entities of this domain in terms of the categories and relations of {\bfo}.%\nb{check!!}\nb{CM: mi sembra ok}

The first part of the section, Sect. \ref{sect_mappings_d2b}, reports the elements covered by the mapping and the conceptual and motivations for its limitations. This part makes technically clear the theoretical and formal barriers to complete the coverage of the ontology in the kind of mapping that our general strategy and related assumptions can generate. 
At the end, we list the primitive relations and the categories of {$\bfo$} which are covered by the mappings with the corresponding syntactic definitions in {$\dolce$}. 
Next, we verify whether the axioms of {$\bfo$} hold in {$\dolce$} when extended with the given syntactic definitions. 
%The axioms are clustered according to the relations or categories they characterize. This part is essentially a list of theorems and their proofs. The proofs have been tested using state of the art theorem provers.

The second part, Sect. \ref{sect_analysis_d2b}, provides an analysis of the achieved results, the limitations and possible alternative strategies.


%===================================
\subsection{The definitions of {\bfo} primitives in the language of {\dolce}}\label{sect_mappings_d2b}
%===================================
%In this section we establish how the {\bfo} notions can be mapped to {\dolce}: 
According to our previous discussion and point (M\ref{Ass3}) of Sect. \ref{sect_methodology}, our goal is to introduce syntactic definitions of {$\bfo$} primitives in terms of {$\dolce$} primitives.
%Unfortunately, not all the {$\bfo$} primitives can be defined in {$\dolce$} in this way. We clarify the main reasons for this limitation when it happens.
%\nb{CM: da qui in poi controllare l'uso di $\thdolce$ vs. {\dolce} e lo stesso per bfo [FC: ho cominciato a controllare, ma dopo alcuni controlli mi sono reso conto che 1-l'ordine di grandezza è circa 300/400 controlli da effettuare 2-risulta un po' pesante 3-la corrente lettura non viene ostacolata, anzi, forse è meglio così.]} 

%Let us start by analyzing the {\bfo} categories. 
First of all, {$\thdolce$} lacks the language to refer to the dimensionality of the instances of a given category. This implies that these distinctions cannot be modeled in this theory, thus: 
\begin{enumerate}[$(i)$]
\item the subcategories of $\sregbcat$ and of $\cfbndbcat$ cannot be distinguished; %are ruled out; 
\item the distinction between $\sitebcat$ and $\cfbndbcat$ cannot be introduced (sites are three-dimensional while continuant fiat boundaries are two-, one-, or zero-dimensional); 
\item the distinction between $\tintbcat$ and $\tinstbcat$ cannot be fully characterized.
\end{enumerate} 

Concerning $(ii)$ we introduce a definition only for the disjunction of $\sitebcat$ and $\cfbndbcat$ (written $\sitebcat{\cup}\cfbndbcat$), see \refdbdf{d2b_siteUcfbnd}. $\sitebcat{\cup}\cfbndbcat$ is clearly not among the categories in the {\bfo} taxonomy and it might not be acceptable as a {\bfo} universal. It is used in the mapping with a technical role: $x \bfoiof{t} \sitebcat{\cup}\cfbndbcat$ is a shortcut for $x \bfoiof{t} \sitebcat \lor x \bfoiof{t}\cfbndbcat$. %It can be removed if needed.\nb{SB: check} 
Concerning $(iii)$ we identify temporal instants (intervals) with $\thdolce$ atomic (non-atomic) time intervals, see \refdbdf{d2b_tinst} and \refdbdf{d2b_tint}. Admittedly, this is a very rough characterization. First, temporal atoms can have the same dimensionality of the times they are part of. Second, in {\bfo} the finite sum of (distinct) zero-dimensional temporal regions is still zero-dimensional while the sum of (distinct) atomic times is always not atomic, i.e., according to \refdbdf{d2b_tinst} and \refdbdf{d2b_tint}, {it is} an interval. Third, {\bfo} time intervals are convex while {\dolce} non-atomic time intervals are not necessarily convex. Thus, \refdbdf{d2b_tint} seems to approximate the category $\onetregbcat$ better than $\tintbcat$. At the same time, if all the non-atomic entities are instances of  $\onetregbcat$, then $\zerotregbcat$ and $\tinstbcat$ collapse. For these reasons, we omit $\onetregbcat$ and $\zerotregbcat$ and 
%we 
consider only the rough definitions of $\tinstbcat$ and $\tintbcat$. Note that, in {\bfo}, the convexity of intervals is characterized by means of the primitive of precedence ($\pr{PREC}$). To define $\pr{PREC}$ in {\dolce} one should extend the theory with an order relation defined on time intervals. Similarly for $\pr{FINST}$ (firstInstantOf) and $\pr{LINST}$ (lastInstantOf). It follows that the mapping does not cover the relations $\pr{PREC}$, $\pr{FINST}$, and $\pr{LINST}$.

As anticipated earlier, see also assumption (M\ref{Ass1}) in Sect. \ref{sect_methodology}, the category of specifically dependent continuants ($\sdcntbcat$) seem to correspond to the {\dolce} category of qualities. However, as observed in Sect.~\ref{sect_diff_resolution}, {\bfo} and {\dolce} distinguish the subclasses of these categories based on different criteria. In {\bfo}, the subcategories of $\sdcntbcat$ are mainly characterized by means of the primitives $\bforealizes$ (realizes) and $\pr{MBAS}$ (materialBasisOf) for which, however, the characterization is missing.\footnote{Necessary conditions are given for $\bforealizes$. These are not enough to characterize the relation.} As a consequence, $\bforealizes$, $\pr{MBAS}$, and the subcategories of $\sdcntbcat$ are not covered by the mapping.

A similar situation holds for the subcategories of material entities ($\mtenbcat$). In particular, objects aggregates are intimately connected to the $\bfompart$ (memberPartOf) primitive. None of these notions can be defined without an extension of {\dolce}. It follows that also $\bfompart$ and the subcategories of $\mtenbcat$ are not covered by the mapping.

Other cases are more subtle. The primitive $\bfohistory$ (historyOf) seems to be naturally defined in $\thdolce$ by:
%
\bflist
\item[] $\bfohistory(x,y) \sdef \forall z(\Pd(z,x) \ifif \forall t(\PREd(z,t) \to \PCd(y,z,t))$
\eflist
%
However the effectiveness of this definition depends on the existential assumptions on perdurants. 
For instance, assume that $y$ participates only at the beginning of a perdurant $p$ and that this beginning is not a temporal part of $p$ in {\bfo}, since {\dolce} does not commit to the existence of all the temporal slices of a perdurant, then $y$ would not have a history. %\nb{SB: questo non era semplice da spiegare, ho cambiato molto}\nb{CM: mi sembra ok}
%For instance, if $y$ just participates in a perdurant $p$ but only during a part $t$ of the temporal  extension of $p$ and the temporal part of $p$ during $t$ does not exist---and {\dolce} does not commit to the existence of all the temporal slices of a perdurant---then $y$ would not have a history. 
These technical difficulties, and the fact that histories seem to have a marginal role in the {\bfo} ontology, suggest to leave out also the classes $\bfohistory$ and $\histbcat$.

Spatiotemporal regions are compatible but not enforced in {\dolce}. One could introduce them among the %spatial and the temporal 
regions together with the correspondent qualities. The projections regulating the relationships with spatial and temporal regions (corresponding to the {\bfo} $\bfotproj$ and $\bfosproj$) would also be necessary.
Alternatively, violating (M\ref{Ass3}), spatiotemporal regions could be constructed (at the semantic level, for instance) as pairs $\langle$time interval, space region$\rangle$. 
%
%These options could be investigated but, since they are 
As we do not exploit constructive extensions, %\nb{CM: cosa vuol dire?}, 
we do not consider them here even though, from the expressive power viewpoint, spatiotemporal regions seem not to change the language. This suggests that their introduction might be, at least technically, less controversial. %everything that can be expressed via spatiotemporal regions can also be expressed taking into account $\TLCd$ together with $\SLCd$. 
Here we do not consider them, more details on spatiotemporal regions can be found in \citep{D24}.\nb{CM: ho tagliao il discorso su $\bfosregofocc$ che non mi sembra usiamo nel seguito}
%In our case, we prefer to introduce the relation $\bfosregofocc$ which is the analogous on occurrents of the relation $\bfosregof$ defined on continuants:\footnote{$\bfosregofocc$ is not considered in {\bfo} even though it can be easily defined on the basis of spatiotemporal regions and their projection on space.}
%%
%\bflist
%\item[] $\bfosregofocc(x,s,t) \sdef (x \bfoiof{t} \procbcat \lor x \bfoiof{t} \pbndbcat) \land \SLCd(x,s,t)$,
%\eflist
%%
%and then use the temporal locations of $x$ and $y$ to understand what is their spatiotemporal relation. More details on spatiotemporal regions can be found in \cite{OntoCdel2.4}.\nb{CM: rif. deliverable}

Finally, following the discussion in Sect.~\ref{sect_problem_univ}, instance-of ($\bfoiof{}$) is not directly defined. Instead, we define in $\thdolce$ the instantiation of the needed universals. We also define the primitive predicate $\bfopartic$ and $\bfouniv$ of $\bfo$, introduced to distinguish particulars from universals, even though $\bfouniv$ results empty in $\thdolce$ (when at least a temporal interval exists, see \refdbth{all_particulars} in Sect.~\ref{sect_analysis_d2b}).\nb{CM: aggiunta questa ultima frase} 


%\smallskip
Summing up, among the {\bfo} notions, in the following we introduce: 
\begin{enumerate}[$(i)$]
\item syntactic definitions for the primitive predicates: $\bfoexist$, $\bfocpart$, $\bfoopart$, $\bfotpart$, $\bfosregof$, $\bfotregof$, $\bfooccurs$, $\bfolocated$, $\bfosdep$, $\bfoconcr$, $\bfogdep$, $\bfoparticin$, $\bfopartic$, $\bfouniv$; and 
\item syntactic definitions with form $x \bfoiof{t} \cn{u}$ for each category $\cn{u} \in \{\cntbcat$, $\occbcat$, $\idcntbcat$, $\gdcntbcat$, $\sdcntbcat$, $\mtenbcat$, $\imenbcat$, $\sitebcat{\cup}\cfbndbcat$, $\sregbcat$, $\procbcat$, $\pbndbcat$, $\tregbcat$, $\tinstbcat$, $\tintbcat\}$.
\end{enumerate}

%Let us start by analyzing the {\bfo} primitive relations, see Table~\ref{table_prim_bfo}. The primitive relations precedes, firstInstantOf, and lastInstantOf would require to extend {\dolce} with a structuring relation on time intervals. The relations realizes and materialBasisOf would require {\dolce} to be able at least to individuate among its qualities the ones that are realizable entities. We don't see how this is possible without any extension. 

These syntactic definitions are given below---where, in {\dolce}, $\ATd(x) \sdef \forall y(\Pd(y,x) \to x=y)$---together with a short informal description. (Once a definition has been introduced, it may be used only in definitions given later to avoid circularity.) A deeper analysis about these definitions and their impact on the preservation of the axioms of {\bfo} is in Sect.~\ref{sect_analysis_d2b}. 
%
\bflist
\item[\dbdf{d2b_exist}] $\bfoexist(x,t)\sdef \PREd(x,t) \lor (\Tdcat(x) \land \Pd(t,x)) \lor (\ABdcat(x) \land \neg \Tdcat(x) \land \Tdcat(t))$.

%{\color{red} ****check if in {\bfo} a time $t$ exist only during $t$, see \refbfoax{timeiof2tpart}}
\vspace{1pt}
$\bfoexist$ coincides with $\PREd$ on $\EDdcat$s, $\PDdcat$s, and $\Qdcat$s; it also applies to $\ABdcat$.  Time intervals $\bfoexist$-exist at every subinterval of themselves while the other abstracts entities $\bfoexist$-exist at every time. This extension matches the fact that, in {\bfo}, both temporal regions and spatial regions (which seem very close to {\dolce} time intervals and space regions, respectively, see \refdbdf{d2b_treg} and \refdbdf{d2b_sreg}) are in time.

\item[\dbdf{d2b_opart}] $\bfoopart(x,y) \sdef \Pd(x,y) \land ((\PDdcat(x) \land \PDdcat(y)) \lor (\Tdcat(x) \land \Tdcat(y)))$

\vspace{1pt}
$\bfoopart$ is a restriction of $\Pd$ (the latter applies also to $\ABdcat$s). The definition preserves the fact that in {\bfo} $\bfoopart$ is defined only on occurrents (that include temporal regions but not spatial regions). 

\item[\dbdf{d2b_tpart}] $\bfotpart(x,y) \sdef \bfoopart(x,y) \land 
\forall z (\bfoopart(z,y) \land \forall t (\bfoexist(z,t) \to \bfoexist(x,t)) \to \bfoopart(z,x))$

\vspace{1pt}
This is the classical definition of temporal part or slice, i.e., $x$ is the maximal part of $y$ during the temporal extension of $x$.

\item[\dbdf{d2b_tregof}] $\bfotregof(x,t) \sdef \PDdcat(x) \land \TLCd(x,t)$

\vspace{1pt}
$\bfotregof$ is the restriction of $\TLCd$ to $\PDdcat$s (in {\dolce} $\TLCd$ is defined for all the entities present in time, i.e., also for $\EDdcat$s and $\Qdcat$s).  

%{\color{red} ****old definition
%
%$\bfotregof(x,t) \sdef \PDdcat(x) \land \PREd(x,t) \land \neg \exists t'(\PREd(x,t') \land \PPd(t,t'))$}
 
\item[\dbdf{d2b_pbnd}] $x \bfoiof{t} \pbndbcat \sdef \PDdcat(x) \land \exists y(\bfotpart(x,y) \land x \neq y) \land \TLCd(x,t) \land \ATd(t)$

\vspace{1pt}
A process boundary is a temporally atomic perdurant, that is a temporal proper part of at least another perdurant. As said, the atomicity of the temporal location of a perdurant is an approximation of its instantaneity. 

%{\color{blue} ****$\pbndbcat$ is rigid: $x \bfoiof{} \pbndbcat \land \bfoexist(x,t) \to x \bfoiof{t} \pbndbcat$
%
%\emph{Proof.} By \refdolceax{TLCd_unicity} the temporal location is unique, therefore $x$ exists at only one time.
%}
%
%{\color{red} ****old definition:
%
%$x \bfoiof{t} \pbndbcat \sdef \PDdcat(x) \land \PREd(x,t) \land \exists y(\bfotppart(x,y)) \land \neg\exists y(\bfotppart(y,x))$}

\item[\dbdf{d2b_proc}] $x \bfoiof{t} \procbcat \sdef \PDdcat(x) \land \PREd(x,t) \land \neg(x \bfoiof{t} \pbndbcat)$

\vspace{1pt}
Processes are perdurants that are not process boundaries (all the perdurants are present at some time \refdolceth{-AB_to_PRE}).

%{\color{blue} ****$\procbcat$ is rigid: $\exists u(x \bfoiof{u} \procbcat) \land \bfoexist(x,t) \to x \bfoiof{t} \procbcat$
%
%\emph{Proof.} From $\exists u(x \bfoiof{u} \procbcat)$ we have $\PDdcat(x)$ and by \refdolceax{d_partictime} and \refdolceax{TLCd_unicity}, $x$ has a temporal location and this temporal location is unique. From the definition of $\bfoexist$ and the disjointness between $\PDdcat$ and $\ABdcat$, $\bfoexist(x,t) \land \PDdcat(x)$ implies $\PREd(x,t)$. $x \bfoiof{u} \procbcat \land \PDdcat(x) \land \TLCd(x,v)$ implies $\neg \ATd(v)$ or $\neg \exists y(\bfotppart(x,y))$. Then $\PDdcat(x) \land \PREd(x,t) \land \TLCd(x,v) \land (\neg \ATd(v) \lor \neg \exists y(\bfotppart(x,y)))$, i.e., $\PDdcat(x) \land \PREd(x,t) \land \neg(x \bfoiof{t} \pbndbcat)$.}

\item[\dbdf{d2b_treg}] $x \bfoiof{t} \tregbcat \sdef \Tdcat(x) \land \bfoexist(x,t)$

\vspace{1pt}
Temporal regions coincide with {\dolce} time intervals.

%{\color{blue} ****$\tregbcat$ is rigid: $\exists u(x \bfoiof{u} \tregbcat) \land \bfoexist(x,t) \to x \bfoiof{t} \tregbcat$
%
%\emph{Proof.} From the definition of $\bfoexist$, $\Tdcat(x)$ implies that $\forall t(\bfoexist(x,t))$, therefore we have $\Tdcat(x) \to \forall t(x \bfoiof{t} \tregbcat)$.
%}
%
%{\color{red} ****in {\bfo} temporal intervals are self-connected but this constraint does not apply in general to one-dimensional temporal regions
%
%****in {\bfo} materials entities are assumed to exist at least at one `one-dimensional temporal region', i.e., there are no `instantaneous' material entities, see \refbfoax{maten2exist}; in {\dolce} we do not have the distinction between zero and one dimensional temporal regions therefore we cannot prove this ({\color{blue} but maybe we can say that they need to exist at one non-atomic interval})}

\item[\dbdf{d2b_occ}] $x \bfoiof{t} \occbcat \sdef x \bfoiof{t} \pbndbcat \lor x \bfoiof{t} \procbcat \lor x \bfoiof{t} \tregbcat$

\vspace{1pt}
As said, spatiotemporal regions are ruled out. An occurrent is any entity among process boundaries, processes and temporal regions (whose definitions are given above).
% (but see Sect.~\ref{occupies_streg}\nb{FC: sezione vecchia?}).

%{\color{blue} ****$\tregbcat$ is rigid because $\pbndbcat$, $\procbcat$, and $\tregbcat$ are all rigid. It follows that an occurrent can not migrate from a process to a process boundary, etc.}
%
%{\color{red} ****we are ruling out spatiotemporal regions (or $\stregbcat$ is empty, against \refbfoax{univ_are_insta})}

\item[\dbdf{d2b_tinst}]  $x \bfoiof{t} \tinstbcat \sdef x \bfoiof{t} \tregbcat \land \ATd(x)$

\vspace{1pt}
Temporal instants are atomic time intervals.

%{\color{blue} ****$\tinstbcat$ is rigid because $\tregbcat$ is rigid and $\ATd$ does not depends on time.}
% 
%{\color{red} **(1) temporal instants are elucidated in BFO as `without extent', here we cannot guarantee that; (2) zero-dimensional temporal regions are in general sums of `separated' temporal instants but we do not have a connection relation} 

\item[\dbdf{d2b_tint}] $x \bfoiof{t} \tintbcat \sdef x \bfoiof{t} \tregbcat \land \neg\ATd(x)$

\vspace{1pt}
Temporal intervals are non-atomic time intervals (in {\bfo} they are self-connected but this property cannot be defined in {\dolce}).

%{\color{blue} ****$\tintbcat$ is rigid because $\tregbcat$ is rigid and $\ATd$ does not depends on time.}
%
%{\color{red} **(1) temporal intervals are elucidated in BFO as `self-connected', here we cannot guarantee that; (2) one-dimensional temporal regions are temporal regions that have at least a temporal interval as part but possibly can also have temporal instants as parts, THEREFORE, our definition of $\tintbcat$ seems to capture more one-dimensional temporal regions than temporal intervals} 

\item[\dbdf{d2b_mten}] $x \bfoiof{t} \mtenbcat \sdef \ $\parbox[t]{\textwidth}{$\EDdcat(x) \land 
%\neg \ASdcat(x) \land 
\PREd(x,t) \land \exists u(\PREd(x,u) \land \neg \ATd(u)) \land \\
%\neg\exists y(\SDd(x,y)) \land 
\forall u(\PREd(x,u) \to \exists ysr($\parbox[t]{\textwidth}{$\Mdcat(y) \land \SLCd(x,s,u) \land \SLCd(y,r,u) \land \Pd(r,s)))$}}

\vspace{1pt}
Material entities are non instantaneous (to match $x \bfoiof{} \mtenbcat \to \exists t(t \bfoiof{t} \onetregbcat \land \bfoexist(x,t))$, {\bfo} axiom [zuw-1]) endurants that during their whole life are (at least partially) spatially co-localized with an amount of matter.

%{\color{blue} ****MODIFIED to obtain the rigidity of $\mtenbcat$: all the conditions in the definition hold at every time at which $x$ is present (in addition deleted the condition $\neg \ASdcat(x)$). 
%
%****old definition:
%
%$x \bfoiof{t} \mtenbcat \sdef \ $\parbox[t]{\textwidth}{$\EDdcat(x) \land \neg \ASdcat(x) \land \PREd(x,t) \land \exists u(\PREd(x,u) \land \neg \ATd(u)) \land \\
%%\neg\exists y(\SDd(x,y)) \land 
%\exists ysr($\parbox[t]{\textwidth}{$\Mdcat(y) \land \SLCd(x,s,t) \land \SLCd(y,r,t) \land \Pd(r,s))$}}
%}
%
%%(old def) $\ $ $x \bfoiof{t} \mtenbcat \sdef $\parbox[t]{\textwidth}{$(\PEDdcat(x) \lor \NPOBdcat(x)) \land \PREd(x,t) \land \neg\exists y(\SDd(x,y)) \land \\ \forall u(\PREd(x,u) \to 
%%\exists yzsr($\parbox[t]{\textwidth}{$\Mdcat(z) \land \SLCd(x,s,u) \land \SLCd(y,r,u) \land \Pd(r,s) \land \\ (\EXDd(x,y,u) \lor \TPd(y,x,u)) \land \Kd(z,y,u)))$}}
%
%{\color{red} ****added the presence in a non atomic interval to match  \refbfoax{maten2exist}}
%
%{\color{red} ****remember that not all the $\EDdcat$s necessarily have a spatial location}
%
%%{\color{red} ****$\MOBdcat$s are instances neither of $\idcntbcat$ nor of $\sdcntbcat$ because they are specifically dependent $\APOdcat$s}
%
%%****do we need to add $\TPd(x,y,t) \to \EXDd(y,x,t)$ ?? (in this case we can delete $\TPd(y,x,u)$ in the disjunct in \refdbdf{d2b_mten})\\
%%this move can be problematic because all the wholes become specifically dependent on their constant parts, in this case they would not be under independent continuant of {\bfo}}

\item[\dbdf{d2b_siteUcfbnd}] $x \bfoiof{t} (\sitebcat{\cup}\cfbndbcat) \sdef $\parbox[t]{\textwidth}{$\Fdcat(x) \land \PREd(x,t) \land \exists s(\SLCd(x,s,t)) \land \\ 
\forall u(\PREd(x,u) \to \neg\exists ysr(\Mdcat(y) \land \SLCd(x,s,u) \land \SLCd(y,r,u) \land \Pd(r,s)))$}

\vspace{1pt}
Both sites and continuant fiat boundaries are {\dolce} features localized in space that during their whole life are never (partially) spatially co-localized with an amount of matter.

%{\color{blue} ****MODIFIED to obtain the rigidity of $\sitebcat{\cup}\cfbndbcat$: all the conditions in the definition hold at every time at which $x$ is present. 
%
%****old definition:
%
%$x \bfoiof{t} (\sitebcat{\cup}\cfbndbcat) \sdef \ $\parbox[t]{\textwidth} {$\Fdcat(x) \land \PREd(x,t) \land 
%%\neg\exists y(\SDd(x,y)) \land 
%\exists s(\SLCd(x,s,t)) \land \\ \neg\exists ysr($\parbox[t]{\textwidth}{$\Mdcat(y) \land \SLCd(x,s,t) \land \SLCd(y,r,t) \land \Pd(r,s))$}}
%}
%
%%(old def) $\ $  $x \bfoiof{t} (\sitebcat{\cup}\cfbndbcat) \sdef \ $\parbox[t]{\textwidth}{$\Fdcat(x) \land \PREd(x,t) \land \\ \forall yu(\TPd(y,x,u) \to \neg\exists z(\Mdcat(z) \land \Kd(z,y,u)))$}
%{\color{red} ****in {\bfo} the distinction between instances of $\sitebcat$ and $\cfbndbcat$ is grounded on the dimensionality of the space they occupy}
%%, the distinction between 0- 1- 2- and 3-dimensional regions of space requires {\dolce} to be extended}

\item[\dbdf{d2b_sreg}] $x \bfoiof{t} \sregbcat \sdef \Sdcat(x) \land \bfoexist(x,t)$

\vspace{1pt}
Spatial regions coincide with {\dolce} space regions.

%{\color{blue} ****$\sregbcat$ is rigid, see the proof for $\tregbcat$}

\item[\dbdf{d2b_imen}] $x \bfoiof{t} \imenbcat \sdef x \bfoiof{t} (\sitebcat{\cup}\cfbndbcat) \lor x \bfoiof{t} \sregbcat$

\item[\dbdf{d2b_idcnt}] $x \bfoiof{t} \idcntbcat \sdef x \bfoiof{t} \mtenbcat \lor x \bfoiof{t} \imenbcat$

\item[\dbdf{d2b_sdcnt}] $x \bfoiof{t} \sdcntbcat \sdef \Qdcat(x) \land \PREd(x,t) \land \exists y(y \bfoiof{t} \idcntbcat \land \neg\Sdcat(y) \land \DQTd(x,y))$

\vspace{1pt}
Specifically dependent continuants are {\dolce} qualities inhering (in the sense of $\DQTd$) in an independent continuant (as defined in \refdbdf{d2b_idcnt}) that is not a spatial region.

%{\color{blue} ****$\sdcntbcat$ is rigid
%
%\emph{Proof}. From the ridigity of $\idcntbcat$, $y \bfoiof{t} \idcntbcat$ implies $y$ is and independent continuant at every time it is present/exists. By \refdolceth{PREd_Q}, when $x$ is present also $y$ is present.
%}
%
%{\color{red} ****{\bfo} does not have qualities of occurrents}
%% (?? and of NPEDs that are not NPOB)}
%
%{\color{red} ****{\dolce} does not investigate the difference btw $\qltbcat$ and $\rlzenbcat$ and do not have relational qualities}
%
%%{\color{red} **** instead of a definition here one could consider an axiom of inclusion}

\item[\dbdf{d2b_concr}] $\bfoconcr(x,y,t) \sdef x \bfoiof{t} \sdcntbcat \land \NPEDdcat(y) \land \neg\exists s(\SLCd(y,s,t))  \land \EXDd(y,x,t)$

\vspace{1pt}
Concretization is a form of {\dolce} existential dependence ($\EXDd$) between a non-physical endurant $y$ that does not have a spatial localization and a specifically dependent continuant (as defined in \refdbdf{d2b_sdcnt}) $x$.

%%\\ \exists z(z \bfoiof{t} \idcntbcat \land \neg \Sdcat(z) \land \DQTd(x,z))$}
%
%{\color{red} ****I think that $\forall t(\PREd(y,t) \to \neg\exists s(\SLCd(y,s,t)))$ follows from $\neg\exists s(\SLCd(y,s,t))$ if we consider the new version of DOLCE}

\item[\dbdf{d2b_gdcnt}] $x \bfoiof{t} \gdcntbcat \sdef \PREd(x,t) \land \forall u(\PREd(x,u) \to \exists y(\bfoconcr(y,x,u)))$

\vspace{1pt}
Generic dependent continuants are non-physical endurants (from \refdbdf{d2b_concr}) that are concretized during their whole life.

%{\color{blue} ****MODIFIED to obtain the rigidity of $\gdcntbcat$: all the conditions in the definition hold at every time at which $x$ is present. 
%
%****old definition:
%
%$x \bfoiof{t} \gdcntbcat \sdef \exists y(\bfoconcr(y,x,t))$
%}
%
%
%{\color{red} old old definition:
%
%$x \bfoiof{t} \gdcntbcat \sdef \NPEDdcat(x) \land \neg \exists s(\SLCd(x,s,t)) \land \\\mbox{} \hfill{} \forall t'(\PREd(x,t') \to \exists y(y \bfoiof{t'} \idcntbcat \land \neg\Sdcat(y) \land \EXDd(x,y,t') \land \EXDd(y,x,t')))$}

\item[\dbdf{d2b_cnt}] $x \bfoiof{t} \cntbcat \sdef x \bfoiof{t} \idcntbcat \lor x \bfoiof{t} \sdcntbcat \lor x \bfoiof{t} \gdcntbcat$

%{\color{red} ****{\dolce} does not directly analyze the nature of $\gdcntbcat$ that however could be considered as a subclass of (non spatially localized) $\NPEDdcat$; according to the BFO-2020 doc the generically dependent continuants are patterns that can be realized in multiple copies specifically dependent on the pattern; \emph{as first tentative approximation} one could define $\gdcntbcat$ as the subclass of $\NPEDdcat$s whose instances are generically dependent on $\idcntbcat \land \neg\sregbcat$ entities that are specific dependent on them:\\\vspace{-10pt}
%
%$x \bfoiof{t} \gdcntbcat \sdef \ $\parbox[t]{\textwidth} {$\NPEDdcat(x) \land \forall t'(\PREd(x,t') \to \\ \exists y(y \bfoiof{t'} \idcntbcat \land \neg(y \bfoiof{t'} \sregbcat) \land \EXDd(x,y,t') \land \EXDd(y,x,t')))$}
%}

\item[\dbdf{d2b_cpart}] $\bfocpart(x,y,t) \sdef x \bfoiof{t} \cntbcat \land y \bfoiof{t} \cntbcat \land (\TPd(x,y,t) \lor \Pd(x,y) \lor \exists zu(\DQTd(x,z) \land \DQTd(y,u) \land \TPd(z,u,t)))$

\vspace{1pt}
According to \refdbdf{d2b_idcnt}, \refdbdf{d2b_sdcnt}, \refdbdf{d2b_gdcnt}, and \refdbdf{d2b_cnt}, continuants include $\EDdcat$s, $\Sdcat$s, and $\Qdcat$s. For $\EDdcat$s, $\bfocpart$ coincides with $\TPd$. For $\Sdcat$s, $\bfocpart$ coincides with $\Pd$. {\dolce} does not define a parthood relation on $\Qdcat$s but it is defined on endurants. One can use the latter to infer a parthood relation on qualities (according to {\dolce} each quality inheres in a single entity,  $\DQTd(x,y) \land \DQTd(x,z) \to y=z$).\footnote{Note that this definition allows qualities of different kind to be one part of the other (e.g., the color of an object being part of the temperature of a larger object). To avoid these cases one could assume that every specialization of {\dolce} has a (finite) set of leaf-types of qualities and requires, in the last disjunct in \refdbdf{d2b_cpart}, $x$ and $y$ to be instances of the same leaf-type. We leave the  implementation and the study of this new definition for future work.}
%; one must check if this move introduces problems with some $\bfocpart$-properties (e.g., extensionality): for instance, some parts of an object with mass could be massless}

%{\color{red} ****{\bfo} continuants include spatial regions (for which $\Pd$ instead of $\TPd$ is considered) and some qualities (for which a parthood relation defined in terms of the one between the continuants they inhere in is considered)}

\item[\dbdf{d2b_sregof}] $\bfosregof(x,s,t) \sdef x \bfoiof{t} \idcntbcat \land \neg\Sdcat(x) \land \SLCd(x,s,t)$

\vspace{1pt}
$\bfosregof$ is the resctriction of $\SLCd$ to independent continuants (as defined in \refdbdf{d2b_idcnt}) that are not spatial regions.  

\item[\dbdf{d2b_partic}] $\bfoparticin(x,y,t) \sdef x \bfoiof{t} \cntbcat \land \neg\Sdcat(x) \land y \bfoiof{t} \procbcat \land \PCd(x,y,t)$

\vspace{1pt}
$\bfoparticin$ is the resctriction of $\PCd$ to continuants that are not spatial regions and to processes (as defined above).  

\item[\dbdf{d2b_occurs}] $\bfooccurs(x,y) \sdef $\parbox[t]{\textwidth}{$\PDdcat(x) \land \exists t(y \bfoiof{t} \mtenbcat \lor y \bfoiof{t} \sitebcat{\cup}\cfbndbcat) \land \\ 
\forall t(\PREd(x,t) \to \exists sr(\SLCd(x,s,t) \land \SLCd(y,r,t) \land \Pd(s,r)))$}
%\item[\dbdf{d2b_occurs}] $\bfooccurs(x,y) \sdef $\parbox[t]{\textwidth} {$\PDdcat(x) \land \exists t(y \bfoiof{t} \mtenbcat \lor y \bfoiof{t} \sitebcat{\cup}\cfbndbcat) \land \\ 
%\forall t(\PREd(x,t) \to \exists sr(\SLCd(x,s,t) \land \SLCd(y,r,t) \land \Pd(s,r)))$}

\vspace{1pt}
$\bfooccurs(x,y)$ holds when the spatial location of the perdurant $x$ is always included in the one of the material entity/site/continuant fiat boundary $y$ (this definition closely corresponds to the formal one provided in the documentation of BFO).

%{\color{red} ****this definition closely corresponds to \refbfodf{df_occurs} (doc. BFO 2020 p.101) but it requires  $\exists t(y \bfoiof{t} \mtenbcat \lor y \bfoiof{t} \sitebcat{\cup}\cfbndbcat)$ rather than $ \exists t(y \bfoiof{t} \mtenbcat \lor y \bfoiof{t} \sitebcat)$}

\item[\dbdf{d2b_located}] $\bfolocated(x,y,t) \sdef x \bfoiof{t} \idcntbcat \land \neg\Sdcat(x) \land y \bfoiof{t} \idcntbcat \land \neg\Sdcat(y) \land
\exists sr(\SLCd(x,s,t) \land \SLCd(y,r,t) \land \Pd(s,r))$

\vspace{1pt}
At time $t$, and independent continuant (that is not a space region) is located in another independent continuant (that is not a space region) when the spatial location (at $t$) of the first continuant is included in the spatial location (at $t$) of the second continuant (this definition closely corresponds to the formal one provided in the documentation of BFO).%\nb{SB: sopra diciamo che la parte formale ha priorità sull'altra documentazione, verificare che questo caso non contraddica quella affermazione}\nb{CM: ho aggiustato mettendo formal, infatti nella doc. fi BFO queste ultime due nozioni sono definite formalmente come sopra}

%{\color{red} ****this definition closely corresponds to the one in doc of BFO-2020 p.66}
%%{\color{red} ****it is not clear what the spatial location of a continuant during an extended interval is; in {\dolce} one could strengthen the last conjunct with \\ $\forall t'(\Pd(t',t) \to \exists sr(\SLCd(x,s,t') \land \SLCd(y,r,t') \land \Pd(s,r)))$}
%
%%$\bfolocated(x,y,t) \sdef  \ $\parbox[t]{\textwidth} {$x \bfoiof{t} \idcntbcat \land \neg\Sdcat(x) \land y \bfoiof{t} \idcntbcat \land \neg \Sdcat(y) \land
%%\\ \forall t'(\Pd(t',t) \to \exists sr(\SLCd(x,s,t') \land \SLCd(y,r,t') \land \Pd(s,r)))$}}

\item[\dbdf{d2b_sdep}] $\bfosdep(x,y) \sdef x \bfoiof{} \sdcntbcat \land \DQTd(x,y)$

\vspace{1pt}
$\bfosdep$ is the restriction of $\DQTd$ to specifically dependent continuants (as defined in \refdbdf{d2b_sdcnt}).

%{\color{red}
%
%****old definition:
%
%$\bfosdep(x,y) \sdef \ $\parbox[t]{\textwidth} {$\exists t(x \bfoiof{t} \sdcntbcat) \land \exists t(y \bfoiof{t} \sdcntbcat \lor (y \bfoiof{t} \idcntbcat \land \neg\Sdcat(y))) \land \\ \SDd(x,y) \land \neg \exists t(\bfocoverlap(x,y,t))$}
%}
%
%%{\color{red} ****differently from {dolce}, in {\bfo} specific dependence excludes temporary overlaps, see \refbfoax{sdep2disj}} 
%
%%{\color{red} ****this is a restriction of $\SDd$ defined in \refdolcedf{dfSDd}}

\item[\dbdf{d2b_gdep}] $\bfogdep(x,y,t) \sdef x \bfoiof{t} \gdcntbcat \land y \bfoiof{t} \idcntbcat \land \neg\Sdcat(y) \land \exists zs(\Pd(s,t) \land \DQTd(z,y) \land \bfoconcr(z,x,s))$

\vspace{1pt}
At time $t$, the generic dependent continuant $x$ generically depends on the independent continuant (that is not a spatial region) $y$, when it is concretized (during a part $s$ of $t$) by a specifically dependent continuant $z$ inhering in $y$. 

%{\color{red} ****stronger possibility: $\bfogdep(x,y,t) \sdef \exists z(\DQTd(z,y) \land \bfoconcr(z,x,t))$}
%
%%\item[\dbdf{d2b_gdep}] $\bfogdep(x,y,t) \sdef x \bfoiof{t} \gdcntbcat \land y \bfoiof{t} \idcntbcat \land \neg\Sdcat(y) \land \EXDd(x,y,t) \land \EXDd(y,x,t)$
%%
%%%{\color{red} ****this definition makes sense only if we assume the definition of $\gdcntbcat$ introduced in the discussion of \refdbdf{d2b_cnt}}
%%%****different from the one of dolce, quite peculiar relation, given the poor axiomatization one could try to define in terms of $\EXDd$ (together with realization and concretization, but this would not be very interesting
%%
%%
%%\item[\color{red} (??)] $\bfoconcr(x,y,t) \sdef (x \bfoiof{t} \sdcntbcat \lor  x \bfoiof{t} \procbcat) \land (\exists z(\DQTd(x,z) \land \bfogdep(y,z,t)) \lor \ ????$
%%
%%{\color{red} ****even by considering the definition of $\gdcntbcat$ introduced in the discussion of \refdbdf{d2b_cnt}, the concretization relation probably cannot be defined in the case $x$ is a process}
%%% (in the case $x$ is a specifically dependent continuant one can use what sketched in \refdbdf{d2b_concr})}
%%

\item[\dbdf{d2b_particular}] $\bfopartic(x) \sdef \exists t(\bfoexist(x,t))$

\vspace{1pt}
Particulars are entities that $\bfoexist$-exist in time (to match $\bfoexist(x,t) \to \bfopartic(x) \land \bfotime(t)$, see {\bfo}-[oap-1], and $\bfopartic(x) \to \exists t(\bfoexist(x,t))$, see {\bfo}-[nmq-1]).

 \item[\dbdf{d2b_univ}] $\bfouniv(x) \sdef \neg\bfopartic(x)$

\vspace{1pt}
Universals are non-particulars (to match $\bfopartic(x) \lor \bfouniv(x)$, see {\bfo}-[eto-1], and $\bfopartic(x) \to \neg \bfouniv(x)$, see [qkp-1]).%\nb{CM: visto quanto detto all'inizio della sezione, noi non aggiungiamo gli universali al dominio di DOLCE, facciamo semplicemente delle macro per l'istanziazione degli universali di BFO presi in conto esplicitamente. Quindi questa $\bfouniv$ saranno sempre vuoti.}


%Note that, according to (M\ref{Ass3}) all these mappings are syntactic definitions.\nb{CM: added, maybe to move before the introduction of mappings\\ SB: lo abbiamo già detto in più punti, io toglierei questa osservazione}

%\item[\color{red} (??)] $\bfompart(x,y,t) \sdef \ ??$
%
%{\color{red} ****the distinction between objects and object aggregates is not analyzed in {\dolce} and seems to require additional expressivity to be captured}
%
%\item[\color{red} (??)] $\bforealizes(x,y) \sdef \ ??$ \hfill{}(but see Sect.~\ref{sect_d2b_realizes} for a partial mapping)
%
%{\color{red} ****the distinction between qualities and realizable entities is not analyzed in {\dolce} and seems to require an extension to be captured, in addition realizability is not clear to us}
\eflist

%%=================================
%\subsection{Preservation of the original {\bfo} axioms}\label{sect_check_bfo_preservation}
%%=================================

In the rest of this section, $\thdolcedbmap$ indicates the theory $\thdolce$ with the definitions listed above, 
%in Sect.~\ref{sect_mappings_d2b} together with the syntactic definitions introduced in Sect.~\ref{sect_bfo}, 
that is,\\ 
$\thdolcedbmap = \thdolce \cup \{$\refdbdf{d2b_exist},\ldots,\refdbdf{d2b_univ}$\}$.%\nb{CM: ho tolto le definizioni di bfo che comunque non sono usate nel seguito}\nb{CM: tagliato anche tutta la discussione successiva sulle def. che qui non mi sembra molto pertinente} %\cup \{$\refbfodf{time}, \refbfodf{coverlap}-\refbfodf{bfoinh}$\}$\nb{FC. check references}.

%Note that \refbfodf{b_iof_notime} and \refbfodf{def_bfoisa} are not included in $\thdolcedbmap$ because they require universals in the domain of quantification. Moreover, \refbfodf{b_iof_notime} could be avoided by including the existential quantifier on time. Alternatively, for each predicate $\cn{u}$ representing a {\bfo}-category, one could introduce the syntactic definition $x \bfoiof{} \cn{u} \sdef \exists t(x \bfoiof{t} \cn{u})$. Definition \refbfodf{def_bfoisa} is also not needed since it does not occur in the {\bfo} axioms. This definition will be used in the mapping from {\bfo} to $\thdolce$, see Sect.~\ref{sect_mappings_b2d}. 

As said, %discussed in Sect.~\ref{sect_diff_resolution} (and made explicit in Sect.~\ref{sect_mappings_d2b}) 
some {\bfo}-axioms involve relations or categories that have not been defined in the mappings. When possible and relevant we considered approximations of these axioms as expressible in the {\dolce} language, otherwise we set them aside. Additional details as well as the proofs of all the theorems can be found in \citep{D24}. In the following analysis we mainly focus on the results that point out some ontological differences between $\dolce$ and $\bfo$. 


%We succeeded in proving or disproving all the axioms (expressible by the limited vocabulary taken into account in the mappings) reported in Sect.~\ref{sect_bfo} with the exception of \refdbth{d2b_cpart_ment}.

%{\color{red}Several proofs have been verified by using theorems provers...}\nb{CM: forse aggiungere qualche dettaglio su quanti assiomi sono stati preservati e quanti no, ecc. / poi rimandare al deliverable per i dettagli}\nb{SB: basterebbe dare qualche esempio e poi rimandare al deliverable}

%===================================
\subsection{Analysis}\label{sect_analysis_d2b}
%===================================

We begin this analysis by considering how the entities in the domain of $\thdolce$ are classified  by the categories of {\bfo} as encoded by our definitions. %\nb{SB: non mi tornava la frase che c'era e l'ho riscritta, va bene così?}\nb{CM: (1) qui stiamo assumendo una partizione, credo valga ma si vede solo alla fine; (2) invece di primitives parlerei di categorie } 
%We begin this analysis by considering how the entities in the domain of $\thdolce$ are classified from the point of view of {\bfo}.
Theorem \refdbth{-AB_particulars} shows that endurants, perdurants, and qualities are all {\bfo} particulars (in the sense of the {\bfo} notion of particular, $\bfopartic$ defined in \refdbdf{d2b_particular}). The case of abstracts is slightly more complex. \refdbth{all_particulars} shows that if there exists at least a time interval then all the abstracts are {\bfo} particulars too. This is due to the definition of $\bfoexist$ \refdbdf{d2b_exist} that assures that abstracts exist at every time. However, while in {\dolce} the existence of endurants, perdurants, and qualities requires them to have a temporal location (and then to be present in time), see \refdolceax{d_partictime} and \refdolceth{-AB_to_PRE}, this does not hold for abstracts, i.e., it is possible to have models of {\dolce} that contain only abstracts and no time intervals. In this case we would not have {\bfo} particulars, only universals \refdbth{no_particular}.

\bflist
\item[\dolceax{d_partictime}] $(\EDdcat(x) \lor \PDdcat(x) \lor \Qdcat(x)) \to \exists t(\TLCd(x,t))$ 

\item[\dolceth{-AB_to_PRE}] $\thdolce \vdash (\EDdcat(x) \lor \PDdcat(x) \lor \Qdcat(x)) \to \exists t(\PREd(x,t))$

\item[\dbth{-AB_particulars}] $\thdolcedbmap \vdash (\EDdcat(x) \lor \PDdcat(x) \lor \Qdcat(x)) \to \bfopartic(x)$

\item[\dbth{all_particulars}] $\thdolcedbmap \vdash \exists u(\Tdcat(u)) \to \forall x(\bfopartic(x))$

\item[\dbth{no_particular}] $\thdolcedbmap \vdash \neg\exists u(\Tdcat(u)) \to \forall x(\bfouniv(x))$

\eflist

\refdolceth{-AB_particulars} seems to conform to both (M\ref{Ass1}) and (M\ref{Ass2}), by corroborating the idea that {\dolce} particulars roughly correspond to {\bfo} particulars and that all the particulars of {\dolce} are `imported' into the ones of {\bfo}. However, \refdbth{no_particular} introduces some doubts about the nature of abstracts. The definition of $\bfoexist$ \refdbdf{d2b_exist}, starting from the fact that temporal and spatial regions are particulars in {\bfo}, extended this idea to all regions (and to all abstracts), i.e., there is a presupposition that all the regions have a uniform nature, they are all particulars in this case (even though, in {\bfo}, temporal and spatiotemporal regions are occurrents while spatial regions are continuants). However, other options are possible. One could consider, for instance, the following two variants of \refdbdf{d2b_exist}:
\bflist
\item[] $\bfoexist(x,t)\sdef \PREd(x,t) \lor (\Tdcat(x) \land \Pd(t,x)) \lor (\Sdcat(x) \land \Tdcat(t))$
\item[] $\bfoexist(x,t)\sdef \PREd(x,t)$
\eflist
%
In the first case time intervals and space regions become {\bfo} particulars as before (matching the fact that temporal and spatial regions are particulars in {\bfo}) but, according to \refdbdf{d2b_particular} and \refdbdf{d2b_univ}, the rest of abstracts would be included as universals. This possibility is interesting because the examples for {\dolce} (spaces of) regions are colors, weights, shapes, etc., while, in {\bfo}, \emph{being red}, \emph{being blue}, \emph{being round}, etc., are universals. In this perspective, one can also presuppose that the {\dolce} $\Pd$ relation holding between regions (in a given space) represents a sort of (intensional) ISA relation, while $\TQLd$---or, maybe better, the composition of $\DQTd$ and  $\TQLd$---represents instantiation (at a time). An option that deserves a detailed analysis even though it introduces differentiation between time intervals and space regions on the one side, and the remaining regions on the other side.%\nb{CM: estendere questo punto?}\nb{SB: a me sembra abbastanza chiaro} 

The second option excludes all abstracts, including time intervals and space regions, from particulars. Even in this case one could see the {\dolce} $\Pd$ as a sort of ISA relation and $\TLCd$ and $\SLCd$ as sorts of instantiation relations (here note that the \refdolceax{TLCd_PD} and  \refdolceax{SLCd_PEDs} go in the direction of considering $\TLCd$ and $\SLCd$ as compositions of $\DQTd$ and  $\TQLd$ as suggested in the previous case also).

In both these cases, the fact that (some) regions become universals is grounded on  \refdbdf{d2b_particular} and \refdbdf{d2b_univ}. The latter is motivated by \refbfoax{particORuniv} and \refbfoax{particNOuniv}, i.e., by the fact that the entities in the domain of {\bfo} are partitioned into universals and particulars. However, one could decide to reject  \refbfoax{particORuniv} and assume that some regions are neither {\bfo} particulars nor {\bfo} universals. They would form a kind of entity that {\bfo} does not consider. Also this option deserves a deeper analysis.
%
\bflist
\item[\dolceax{TLCd_PD}] $\PDdcat(x) \to (\TLCd(x,t) \ifif \exists y(\DQTd(y,x) \land \QLd(t,y) \land \Tdcat(t)))$ 
\item[\dolceax{SLCd_PEDs}] $\PEDdcat(x) \to (\SLCd(x,s,t) \ifif \exists y(\DQTd(y,x) \land \SLdcat(y) \land \TQLd(s,y,t)))$ 

\item[\bfoax{particORuniv}] $\bfopartic(x) \lor \bfouniv(x)$
\hfill {\scriptsize [eto-1]}

\item[\bfoax{particNOuniv}] $\bfopartic(x) \to \neg \bfouniv(x)$
\hfill {\scriptsize [qkp-1]}
\eflist

There are also more subtle correspondences to consider. Theorem \refdbth{pd_to_proc_or_pbnd} shows that perdurants are the union of processes and process boundaries. However, in $\thdolcedbmap$, the {\bfo} axioms \refbfoax{opart_proc1}, \refbfoax{opart_proc3}, \refbfoax{opart_pbnd2}, \refbfoax{pbndifif}, and \refbfoax{proctreg2tint} cannot be proved making evident that the distinction between processes and processes boundaries behaves quite differently from the one in {$\thbfo$}.%\nb{CM: qui bisogna dire che questi sono tutti assiomi di bfo, non credo serva introdurre gli assiomi di bfo esplicitamente}
%
\bflist

\item[\bfoax{opart_proc1}] $x \bfoiof{t} \procbcat \land \bfoopart(x,y) \to \exists t'(y \bfoiof{t'} \procbcat)$\hfill {\scriptsize [csk-1]}

\item[\bfoax{opart_proc3}] $x \bfoiof{t} \procbcat \to \exists yt'(y \bfoiof{t'} \pbndbcat \land \bfoopart(y,x))$
\hfill {\scriptsize [aff-1]}

\item[\bfoax{opart_pbnd2}] $x \bfoiof{t} \pbndbcat \land \bfoopart(y,x) \to \exists t'(y \bfoiof{t'} \pbndbcat)$
\hfill {\scriptsize [hdk-1]}

\item[\bfoax{pbndifif}] $\exists t(x\bfoiof{t}\pbndbcat) \ifif \exists y(\bfotpart(x,y) \land \exists t(y \bfoiof{t} \procbcat)) \land \exists t(\bfotregof(x,t) \land t \bfoiof{t} \tinstbcat)$
\hfill {\scriptsize [esh-1]}

\item[\bfoax{proctreg2tint}] $\exists t(x\bfoiof{t}\procbcat) \land \bfotregof(x,t) \to \exists t'(t' \bfoiof{t'}\tintbcat \land \bfotpart(t',t))$
\hfill {\scriptsize [fzy-1]}

\item[\dbth{pd_to_proc_or_pbnd}] $\thdolcedbmap \vdash \PDdcat(x) \ifif (\exists t(x \bfoiof{t} \procbcat) \lor \exists t(x \bfoiof{t} \pbndbcat))$
%
%\item[\dbth{d2b_procdissect}] $\thdolcedbmap \nvdash $ \refbfoax{opart_proc1}
%
%\item[\dbth{d2b_opart_proc3}] $\thdolcedbmap \nvdash $ \refbfoax{opart_proc3}
%
%\item[\dbth{d2b_opart_pbnd2}] $\thdolcedbmap \nvdash $ \refbfoax{opart_pbnd2}
%
%\item[\dbth{d2b_pbndifif}] $\thdolcedbmap \nvdash $ {\refbfoax{pbndifif}}
%
%\item[\dbth{d2b_proctreg2tint}] $\thdolcedbmap \nvdash $ {\refbfoax{proctreg2tint}}
\eflist


{\bfo} presupposes that processes and process boundaries have a different temporal nature, and constrains their relationship, which is quite complex, via a set of axioms. On the other hand, \refdbdf{d2b_tinst} and \refdbdf{d2b_tint}---together with \refdbdf{d2b_pbnd} and \refdbdf{d2b_proc}\nb{CM: ho messo il rif. a pbnd}---reduce this difference to atomicity and to the existence of strictly larger (relatively to temporal parthood) perdurants. Looking at the counterexamples used in the proof of the previous theorems, this different behavior about processes and process boundaries seems mainly due to the poor approximation of the notions of temporal instant and temporal interval provided by \refdbdf{d2b_tinst} and \refdbdf{d2b_tint} together with the low commitment of {\dolce} on the existence of perdurants.  

For instance, in {\dolce} it is possible to have three temporally co-localized perdurants $p_1$, $p_2$, and $p_{12}$ all with atomic temporal locations and such that  the latter is the mereological sum of the other two. %, i.e., $\SUMd(p_{12}, p_1,p_2)$. 
There can also be two additional perdurants $p_3$ and $p_{123}$ such that the temporal location of $p_3$ does not overlap the one of $p_1$ and $p_{123}$ is the mereological sum of $p_{12}$ and $p_{3}$. %\nb{SB: questo dovrebbe essere $p_{3}$, vero?} %also $\SUMd(p_{123}, p_{12},p_3)$ holds.
 In this scenario, according to \refdbdf{d2b_proc} and \refdbdf{d2b_treg}, $p_{1}$ is a process because, though it has an atomic temporal location, it is not a temporal proper part of anything; $p_1$ is part of $p_{12}$, but $p_{12}$ is a process boundary (against \refbfoax{opart_proc1} and \refbfoax{opart_pbnd2}) because it has an atomic temporal location and it is a proper temporal part of $p_{123}$. For another example, in {\dolce} it is possible to have perdurants that are not proper temporal parts of any other perdurant and such that all their parts are temporally co-localized with them (possibly with an atomic temporal location) and in their turn are not proper temporal part of any other perdurant (e.g., discard $p_3$ and $p_{123}$ from the previous example, keeping only $p_1, p_2$ and $p_{12}$).\nb{SB: a me questo esempio non è chiaro}\nb{CM: cos'è che non ti è chiaro}\nb{SB: no ricordo :)} According to \refdbdf{d2b_pbnd} and \refdbdf{d2b_proc},\nb{CM: ho messo il rif. a pbnd} these perdurants as well as all their parts are classified as processes against \refbfoax{opart_proc3}, \refbfoax{pbndifif}, and \refbfoax{proctreg2tint}. These examples may look `exotic', yet it is not easy to rule out them. One could get rid of some of these cases by requiring that processes have a non-atomic temporal location. Then, one needs to remove \refdbth{pd_to_proc_or_pbnd}, otherwise it would be possible to have perdurants with an atomic temporal location that are not temporal proper part of any other perdurant. 

There is a further difference concerning the `temporal behavior' of {\dolce} perdurants vs.~{\bfo} occurrents. %by \refdbth{stregof_opart_equiv}, which is relative to \refbfoax{stregof_opart_equiv_ax} (meaning that the thesis of \refdbth{stregof_opart_equiv} is a modified version of \refbfoax{stregof_opart_equiv_ax}, which does not use the predicate {$\bfostregof$}). 
In {\bfo}, occurrent parthood between processes or process boundaries is equivalent to occurrent parthood between the corresponding spatiotemporal regions, therefore different processes or process boundaries cannot be spatiotemporally co-localized. %\nb{CM: non sono sicuro su identifies [FC: magari così?]} 
%{\bfo} identifies\nb{CM: non sono sicuro su identifies} occurrent parthood between processes or process boundaries with spatiotemporal inclusion, it follows that different processes/process boundaries cannot be spatiotemporally co-localized. 
{\dolce} makes the opposite choice and allows for spatiotemporally co-localized perdurants. A similar situation arises between {\dolce} endurants and {\bfo} continuants as highlighted by the fact that neither \refbfoax{sregof_maten} nor \refbfoax{id_idcnt} can be proved in $\thdolcedbmap$. %\nb{SB: era scritto "both ... cannot...."}
%\refdbth{d2b_sregof_maten} and \refdbth{d2b_id_idcnt}. 
In {\dolce}, an amount of matter constituting a statue at a given time $t$ is different from the statue and it is not a $\TPd$-part of the statue at $t$ (and vice versa) even though the two endurants are spatially co-localized at $t$ (and possibly during their whole life), see \refdolceth{Kd_to_diff} and \refdolceax{Kd_colocalization}. Similarly, in {\dolce}, a sum of bricks is different from a wall even though they can mereologically coincide at a given time.
This view allows for the co-existence of distinct entities in the same spatial and temporal locations. Such entities are further distinguished on the basis of their `modal' properties. In comparison, {\bfo} embraces a `reductionist' perspective by assuming that a given spatial or spatiotemporal region cannot be the location of different continuants or occurrents. In other words, space and time locations are not fundamental for the identity of entities in {\dolce}. %\nb{CM: nel teorema \refdbth{stregof_opart_equiv} manca un riferimento al mapping che riguarda lo spazio tempo, da capire se vogliamo tenere questo o invece toglierlo} 
Thus, at first sight endurants and occurrents on the one hand, and $\TPd$ and $\bfocpart$ on the other, seem to be different ways to capture the `same' ontological category. Nonetheless, a conceptual and formal analysis shows that ${\thdolcedbmap \nvdash \refbfoax{id_idcnt}}$, highlighting that the views embraced by these systems, while apparently similar, remain deeply incompatible. %\nb{SB: spero di non aver enfatizzato troppo} These modeling differences are among the most important we found between the two ontologies. 
%
\bflist
%\item[\bfoax{stregof_opart_equiv_ax}] $\exists t(x \bfoiof{t} \procbcat \lor x \bfoiof{t} \pbndbcat) \land \exists t(y \bfoiof{t} \procbcat \lor y \bfoiof{t} \pbndbcat) \to \\
%\mbox{}\hfill{}(\bfoopart(x,y) \ifif \exists rs(\bfostregof(x,r) \land \bfostregof(y,s) \land \bfoopart(r,s)))$
\item[\bfoax{sregof_maten}]  $x \bfoiof{t} \mtenbcat \land y \bfoiof{t} \mtenbcat \land \bfosregof(x,r,t) \land \bfosregof(y,r,t) \to \bfocpart(x,y,t) \land \bfocpart(y,x,t)$ 
\hfill {\scriptsize [scr-1]}

\item[\bfoax{id_idcnt}] $\exists t(x \bfoiof{t} \idcntbcat \land y \bfoiof{t} \idcntbcat \land \neg(x \bfoiof{t} \objaggbcat) \land \neg(y \bfoiof{t} \objaggbcat) \land  \bfocpart(x,y,t) \land \bfocpart(y,x,t)) \to x=y$  
\hfill {\scriptsize [tab-1]}

\item[\dolceax{Kd_colocalization}] $\Kd(x,y,t) \to \forall s(\SLCd(x,s,t) \ifif \SLCd(y,s,t))$ 

\item[\dolceth{Kd_to_diff}] $\Kd(x,y,t) \to x \neq y$ 
%\item[\dbth{stregof_opart_equiv}] $\thdolcedbmap \cup \{$\refdbdf{d2b_sregofocc}$\} \nvdash \exists t(x \bfoiof{t} \procbcat \lor x \bfoiof{t} \pbndbcat) \land \exists t(y \bfoiof{t} \procbcat \lor y \bfoiof{t} \pbndbcat) \to \\
%\mbox{}\hfill{} \bfoopart(x,y) \ifif \forall t(\bfoexist(x,t) \to \exists rs(\bfosregofocc(x,r,t) \land \bfosregofocc(y,s,t) \land \bfocpart(r,s,t)))$\nb{FC: ricordarsi sezione STREG}
\eflist

These are not the only differences, of course. From ${\thdolcedbmap \nvdash \refbfoax{cpart_wext}}$ we see that the $\bfocpart$ (as defined in \refdbdf{d2b_cpart}) does not satisfy the supplementation principle, and from ${\thdolcedbmap \nvdash \refbfoax{ex_cprod}}$ that the existence of the product is not guaranteed. %(where $\bfocoverlap$ is standardly defined as in \refbfodf{coverlap}). 
Note that the existence of products cannot be inferred for $\bfoopart$ either since ${\thdolcedbmap \nvdash \refbfoax{existence_oprod}}$. % where $\bfoooverlap$ is defined as in \refbfodf{ooverlap}.%\nb{CM: forse portare la nota nel testo e aggiungere i teoremi/assiomi necessari [FC: fatto]} 
%\footnote{There are other differences: \refdbth{d2b_cpart_wext} shows that the $\bfocpart$ (as defined in \refdbdf{d2b_cpart}) does not satisfy the supplementation axiom, and \refdbth{d2b_ex_cprod} that the existence of the product is not guaranteed. Note that the existence of products cannot be inferred for $\bfoopart$ \refdbth{d2b_existence_oprod} either.}\nb{CM: forse portare la nota nel testo e aggiungere i teoremi/assiomi necessari} 
%
\bflist
%\item[\bfoax{stregof_opart_equiv_ax}] $\exists t(x \bfoiof{t} \procbcat \lor x \bfoiof{t} \pbndbcat) \land \exists t(y \bfoiof{t} \procbcat \lor y \bfoiof{t} \pbndbcat) \to \\
%\mbox{}\hfill{}(\bfoopart(x,y) \ifif \exists rs(\bfostregof(x,r) \land \bfostregof(y,s) \land \bfoopart(r,s)))$
%\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[\bfoax{cpart_wext}] $\bfocpart(x,y,t) \land x \neq y \to \exists z(\bfocpart(z,y,t) \land z \neq y\land \neg\bfocoverlap(z,x,t))$
\hfill {\scriptsize [fyf-1]}

\item[\bfoax{ex_cprod}] $\exists z(\bfocpart(z,x,t) \land \bfocpart(z,y,t)) \to \exists z(\forall w(\bfocpart(w,z,t) \ifif \bfocpart(w,x,t) \land 	\bfocpart(w,y,t)))$
\hfill {\scriptsize [gzr-1]}

\item[\bfoax{existence_oprod}] $\exists z(\bfoopart(z,x) \land \bfoopart(z,y)) \to \exists z(\forall w(\bfoopart(w,z) \ifif \bfoopart(w,x) \land \bfoopart(w,y)))$
\hfill {\scriptsize [hpc-1]} 

%\item[\dbth{d2b_sregof_maten}]  $\thdolcedbmap \nvdash $ \refbfoax{sregof_maten}

%\item[\dbth{d2b_id_idcnt}] $\thdolcedbmap \nvdash $ {\refbfoax{id_idcnt}}

%\item[\dbth{d2b_cpart_wext}] $\thdolcedbmap \nvdash $ {\refbfoax{cpart_wext}}
%
%\item[\dbth{d2b_ex_cprod}] $\thdolcedbmap \nvdash $ {\refbfoax{ex_cprod}}
%
%\item[\dbth{d2b_existence_oprod}] $\thdolcedbmap \nvdash $ {\refbfoax{existence_oprod}}
%
%\item[\dbth{stregof_opart_equiv}] $\thdolcedbmap \cup \{$\refdbdf{d2b_sregofocc}$\} \nvdash \exists t(x \bfoiof{t} \procbcat \lor x \bfoiof{t} \pbndbcat) \land \exists t(y \bfoiof{t} \procbcat \lor y \bfoiof{t} \pbndbcat) \to \\
%\mbox{}\hfill{} \bfoopart(x,y) \ifif \forall t(\bfoexist(x,t) \to \exists rs(\bfosregofocc(x,r,t) \land \bfosregofocc(y,s,t) \land \bfocpart(r,s,t)))$\nb{FC: ricordarsi sezione STREG}


\eflist


According to \refdbdf{d2b_cpart} and the definitions of the subclasses of $\cntbcat$, for independent continuants that are not spatial regions, $\bfocpart$ reduces to $\TPd$. However, for independent continuants that are not object aggregates, the original $\bfocpart$ is antisymmetric, but is not so the relation defined by \refdbdf{d2b_cpart}, that in this case is equivalent to $\TPd$. As we have seen, this fact has an important impact on the entities that are classified as endurant or as continuant in the two theories. One could recover the antisymmetry by changing the definition of $\bfocpart$. This amounts to break the correspondence between $\TPd$ and $\bfocpart$ for independent continuants by `injecting' antisymmetry into \refdbdf{d2b_cpart}, e.g.,
\bflist
\item[] $\bfocpart(x,y,t) \sdef x \bfoiof{t} \cntbcat \land y \bfoiof{t} \cntbcat \land ((\TPd(x,y,t) \land (\neg \TPd(y,x,t) \lor x=y)) \lor \Pd(x,y) \lor \\ 
\mbox{} \hfill \exists zu(\DQTd(x,z) \land \DQTd(y,u) \land \TPd(z,u,t)))$
\eflist
%
This alternative definition has some advantages: $(i)$ it preserves antisymmetry as in the original {\bfo}; and $(ii)$ it states explicitly one difference between $\bfocpart$ and  $\TPd$. However, some differences remain. We can have endurants that in {\dolce} satisfy $\TPd$ and are mapped to $\idcntbcat$ but do not satisfy the newly defined $\bfocpart$. %\nb{SB: ho modificato il testo che mi sembrava impreciso} 
Take our previous example, the (sum of the) bricks and the wall do not satisfy the new $\bfocpart$. In all these cases, \refbfoax{sregof_maten} fails. 

Another approach could be to explicitly specialize the definition of $\bfocpart$ to take into account the different cases, e.g.,  
\bflist
\item[] $\bfocpart(x,y,t) \sdef $\parbox[t]{\textwidth} {$x \bfoiof{t} \cntbcat \land y \bfoiof{t} \cntbcat \land 
($\parbox[t]{\textwidth} {$(\TPd(x,y,t) \land (\neg \TPd(y,x,t) \lor x=y)) \lor \\ 
\exists sr(\SLCd(x,s,t) \land \SLCd(y,r,t) \land \Pd(s,r)) \lor \\ 
\Pd(x,y) \lor \exists zu(\DQTd(x,z) \land \DQTd(y,u) \land \TPd(z,u,t)))$}}
\eflist
Note that the antisymmetry of $\bfocpart$ is again lost: the bricks and the wall $\bfocpart$-coincide at $t$ even though they are different. One could further change the definition of $\bfosregof$ stating that the bricks (or the wall) have no spatial location at $t$, or that at $t$ they have different spatial locations. One could proceed similarly in the case of the statue and the clay. However, this option seems to go against the intuitive interpretation of $\bfosregof$ assumed in $\bfo$.%\nb{SB: cosa significa `too strong'? bisogna dire qualcosa di più}\nb{CM: modificato}
\footnote{A similar analysis holds on occurrents.}% as highlighted by \refdbth{stregof_opart_equiv}.}

%\medskip
These examples suggest to follow a different approach, possibly closer to the original commitments of the two ontologies. Consider again the example of the statue and the clay, or the brick and the wall. There are two different endurants that are spatially coincident at least at a given time. One can think that \refbfoax{sregof_maten} and \refbfoax{id_idcnt} aim at ruling out these kinds of examples: it is not a matter of avoiding spatial coincidence or parthood between the brick and the wall, their goal, one could argue, is to rule out one of these two entities, i.e., to rule out from the domain  of quantification of $\bfo$, either the brick or the wall (both of them are in the domain of $\dolce$).\footnote{This is in contrast with (M\ref{Ass2}) and with the mappings that, vice versa, allow to import all the endurants of {\dolce} into {\bfo}.}
%\nb{SB: il testo della nota mi confonde}\nb{CM: provato a cambiare la fine della frase prima della nota} 
One can then adopt a strategy that `filters out' some of the {\dolce} endurants. Setting this filter is not trivial. For the case of the statue and the clay, one can rely on the fact that constitution is a sort of order relation in {\dolce}. One can maintain the substratum (the clay) as an element in the domain, and discard the statue due to the fact that it is the substratum that constitutes the statue. However, in the case of the bricks and the wall we cannot use $\TPd$ to do the same, because $\TPd$ is not asymmetric while constitution is.
%we cannot rely on $\TPd$ because the sum of the bricks is part of the wall and the wall is part of the sum of the bricks. 
One needs to find a different relation or some other principle to rule out one of these. But this is not all. Let us assume that we do not import the statue into {\bfo}. Does it mean that {\bfo} cannot talk about statues or that it relies on a different representation? After all, it classifies the clay under amount of matter as well as under statue. One would need to translate the {\dolce} claims about the statue into {\bfo} claims about the amount of clay %that (in {\dolce}) constitutes the statue 
(since it is the only element left in the domain of {\bfo}). The consequences of this approach---in particular how to track statues through the change of their substratum---deserve more investigation.  It is however important to note that this first analytical step allows us to understand the differences and to individuate the main problems that a mapping needs to address.%\nb{CM: forse aggiungere qualche dettaglio su questo punto e sul come si re-identificano gli amounts of clay che nel tempo costituiscono la *stessa* statua}

The analysis of more refined correspondences, like \refdbth{MorPOB_not_cnt}, \refdbth{inst_MorPOB_to_mten}, and \refdbth{mten_not_PED}, confirms that temporally extended amounts of matters and physical objects are material entities. The other direction does not hold since non-physical endurants could very well be material entities. However,  \refdbth{pd_to_proc_or_pbnd}, \refdbth{MorPOB_not_cnt}, together with \refdbth{F_not_cnt}, \refdbth{Q_not_cnt}, and \refdbth{NPED_not_cnt}, show that there are endurants and qualities, all of which are particulars (see \refdbth{-AB_particulars}), that are neither continuants nor occurrents. This means that the partition of particulars into continuants and occurrents, assumed by {\bfo}, is not preserved by the mapping: some endurants and qualities end up in an ontological `limbo'. 
%
\bflist
\item[\dbth{MorPOB_not_cnt}] $\thdolcedbmap \nvdash (\Mdcat(x) \lor \POBdcat(x)) \to \exists t(x \bfoiof{t} \cntbcat)$

\item[\dbth{inst_MorPOB_to_mten}] $\thdolcedbmap \vdash (\Mdcat(x) \lor \POBdcat(x)) \land \exists t(\TLCd(x,t) \land \neg \ATd(t)) \to \exists t(x \bfoiof{t} \mtenbcat)$

\item[\dbth{mten_not_PED}] $\thdolcedbmap \nvdash \exists t(x \bfoiof{t} \mtenbcat) \to \PEDdcat(x)$

\item[\dbth{F_not_cnt}] $\thdolcedbmap \nvdash \Fdcat(x) \to \exists t(x \bfoiof{t} \cntbcat)$

\item[\dbth{Q_not_cnt}] $\thdolcedbmap \nvdash \Qdcat(x) \to \exists t(x \bfoiof{t} \cntbcat)$

\item[\dbth{NPED_not_cnt}] $\thdolcedbmap \nvdash \NPEDdcat(x) \to \exists t(x \bfoiof{t} \cntbcat)$
\eflist

On the other hand, the imported entities do not necessarily cover all the categories of {\bfo}. There are at least two reasons for that, one factual and one structural. The factual reason is that some of the {\dolce} categories may be empty. For instance, if there are no features, then $\imenbcat$ would be empty. Consequently, axiom \refbfoax{univ_are_insta}, which states that all universals are non-empty, is not preserved. The structural reason is that, according to the mapping, some categories (as defined in the definitions) are necessarily empty. 
This is the case of universals (assuming that there is at least a time in the domain of quantification, see \refdbth{all_particulars}). One solution is to consider some types of entities, e.g., those that earlier we said are in an ontological `limbo', as {\bfo} universals. We already saw that some regions (e.g., abstracts) could be seen as universals. Similarly, one could assume that specific subclasses of non-physical endurant ($\NPEDdcat$) are actually concepts behaving like {\bfo} universals. Note that this approach has an important impact on the theorems one can prove.%\nb{CM: ci sarebbero un sacco di altre osservazioni da fare sui teoremi che non seguono%, ma questo richiederebbe di entrare in più dettagli tecnici ancora e di come minimo raddoppiare la sez., non so se ritenete che le considerazioni sopra siano sufficienti \nb{SB: il problema di mettere più materiale è che si accumulano i casi senza che si possa dare una visione globale/unificante}


%\medskip
One way to choose among the alternative approaches in developing the mapping, is to look at what the mapping optimizes. For instance, strict and restrictive mappings, carefully set to not allow exchanges of entities that would be in the ontological `limbo' of the target ontology, might be preferred in the context of data transfer, they are safer in this context. Mappings focusing on ontological significance and the maximization of the number of imported entities are instead arguably better for the goals of comparing ontologies, highlighting core differences, and establishing general interoperability results.

%=====================================
\section{The mapping from {\bfo} to {\dolce}}\label{sect_b2d}
%=====================================

%======================================
\subsection{The definitions of {\dolce} primitives in the language of {\bfo}}\label{sect_mappings_b2d}
%======================================

In this section we introduce syntactic definitions of {\dolce} notions in terms of {\bfo} primitives. 
The starting point is the domain of {\bfo}. We aim to classify and relate the entities in this domain in terms of the categories and relations of {\dolce}.
Analogously to the {\dolce} to {\bfo} direction of Sect. \ref{sect_d2b} and with similar motivations (see the analysis of Sect. \ref{sect_analysis_b2d}), we obtain only a partial mapping covering a subset of the categories and primitives of {\dolce}.  

As discussed in Sect.~\ref{sect_diff_resolution}, in {\dolce} the agentive and social dimensions play an important role in characterizing the subcategories of physical object ($\POBdcat$) and non-physical endurant ($\NPEDdcat$) but those dimensions are not considered in {\bfo}. Similarly, the subcategories of perdurant ($\PDdcat$) rely on the notions of homeomericity and cumulativity, but these notions are beyond the scope of {\bfo}. This leads to exclude these subcategories from the mapping. Furthermore, while it is not clear how the distinction between amounts of matter and physical objects can be made, regarding features we can rely on the {\bfo} categories of site, continuant fiat boundary and fiat object. Thus, within the category of physical endurants ($\PEDdcat$) we include in the mapping only the category of features ($\Fdcat$). 

We will see that physical endurants correspond to independent continuants that are not regions,
see \refbddf{b2d_PEDdcat}, while the only entities that can be mapped to non-physical endurants are generically dependent continuants, see \refbddf{b2d_NPEDdcat}. In {\dolce}, arbitrary sums ($\ASdcat$) have necessarily a physical and a non-physical part, see \refdolceax{TPd_AS}. To match this axiom, in {\bfo} we should find continuants that are not spatial regions and are neither independent nor generically dependent continuants. The only option is that of specifically dependent continuants. However, following our guidelines in Sect. \ref{sect_methodology}, these are mapped to {\dolce} physical qualities, as formalized in \refbddf{b2d_PQdcat}. As a result, the category $\ASdcat$ of arbitrary sums would be empty. For this reason, $\ASdcat$ is not covered in the mapping.   
%
\bflist
\item[\dolceax{TPd_AS}] $\ASdcat(x) \to \exists yzut(\TPd(y,x,t) \land \PEDdcat(y) \land \TPd(z,x,u) \land \NPEDdcat(z))$  
\eflist

In Sect.~\ref{sect_analysis_d2b} we have seen that one of the main differences between {\dolce} and {\bfo} concerns the reduction of the parthood relations to spatial and spatiotemporal inclusions. In particular, in {\bfo} there are no spatially co-localized distinct independent continuants (that are not object aggregates) and there are no spatiotemporally co-localized distinct occurrents. We then lack one of the main basis to build a constitution relation among endurants and perdurants. In principle, one could see the relation between a generic dependent continuant and the mereological sum of its carriers at a given time as a form of constitution. This solution is debatable and would model only a very limited notion of constitution, quite different from the general one in {\dolce}. Thus, we refrain from introducing $\Kd$ in the mapping.  

Concerning qualities, {\bfo} accepts only qualities inhering in independent continuants. From the point of view of {\dolce}, this restricts the mapping to physical qualities only, see \refbddf{b2d_Qdcat}. 

Regarding regions, there are time intervals and space regions. To locate entities in time and space we need to rely on $\TLCd$ and $\SLCd$ only because {\dolce}'s temporal and spatial locations have no correspondent entities in {\bfo}. In particular, the $\QLd$ and $\TQLd$ relations do not make sense in this setting. Alternatively, as previously discussed, one could import some {\bfo} universals into {\dolce} regions and assume that instance-of corresponds to ($\DQTd$ composed with) $\TQLd$. In this case, the ISA relation would correspond to the primitive $\Pd$, that in {\dolce} is defined on regions. This alternative, which we do not investigate here, seems worth developing. %We leave it for future work. 
%

Finally, the categories for facts and for sets, that in the original taxonomy of {\dolce} \citep{D18} appear under abstract ($\ABdcat$), have not been taken into account in {\dolce}-\textsc{cl}, thus we ignore them here. 
 

\smallskip
Summing up, in the following we discuss these {\dolce} notions: 
\begin{enumerate}[$(i)$]
\item syntactic definitions for the primitive relations: $\Pd$, $\TPd$, $\TLCd$, $\SLCd$, $\PCd$, $\DQTd$, $\EXDd$; and 
\item syntactic definitions for the categories: $\EDdcat$, $\PDdcat$, $\Qdcat$, $\ABdcat$, $\Fdcat$, $\PEDdcat$, $\NPEDdcat$, $\PQdcat$, $\Rdcat$, $\TRdcat$, $\PRdcat$, $\Tdcat$, and $\Sdcat$.
\end{enumerate}

Below we list these syntactic definitions where inherence ($\bfoinh$) used in \refbddf{b2d_DQTd} is defined in $\bfo$ as
%
\bflist
\item[] $\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
%
and where, to simplify the writing of some definitions, we use the shortcut $x \bfoiof{} \cn{u} \sdef \exists t(x \bfoiof{t} \cn{u})$ for every universals $\cn{u}$ explicitly considered.
%
Here we provide just short informal descriptions of the definitions, a deeper analysis about these definitions and their impact on the preservation of the axioms of {\dolce} is done in Sect.~\ref{sect_analysis_b2d}. 
%
\bflist
\item[\bddf{b2d_PDdcat}] $\PDdcat(x)\sdef x \bfoiof{} \procbcat \lor x \bfoiof{} \pbndbcat$

\vspace{1pt}
Perdurants coincide with the disjunction of processes and process boundaries. 

\item[\bddf{b2d_EDdcat}] $\EDdcat(x)\sdef x \bfoiof{} \cntbcat \land \neg(x \bfoiof{} \sregbcat) \land \neg(x \bfoiof{} \sdcntbcat)$

\vspace{1pt}
We rule out from endurants temporal and spatial regions that are mapped, respectively, to time intervals and space regions, see \refbddf{b2d_Tdcat} and \refbddf{b2d_Sdcat}.

\item[\bddf{b2d_PEDdcat}] $\PEDdcat(x)\sdef x \bfoiof{} \idcntbcat \land \neg(x \bfoiof{} \sregbcat)$

\vspace{1pt}
Physical endurants are independent continuants that are not spatial regions.

\item[\bddf{b2d_Fdcat}] $\Fdcat(x)\sdef x \bfoiof{} \sitebcat \lor x \bfoiof{} \cfbndbcat \lor x \bfoiof{} \fobjbcat$

\vspace{1pt}
Features are the union of sites, continuant fiat boundaries, and fiat objects.

\item[\bddf{b2d_NPEDdcat}] $\NPEDdcat(x)\sdef x \bfoiof{} \gdcntbcat$

\vspace{1pt}
Non-physical endurants coincide with generically dependent continuants.

%{\color{red} ****the class of arbitrary sum is necessarily empty because continuants that are not specifically dependent are partitioned in idcnt e gdcnt and sreg are mapped to regions, però devo cedo mettere un mapping del genere $\ASdcat(x) \sdef \EDdcat(x) \land \neg \PEDdcat(x) \land \neg \NPEDdcat(x)$}

\item[\bddf{b2d_PQdcat}] $\PQdcat(x)\sdef x \bfoiof{} \sdcntbcat$

\vspace{1pt}
Physical qualities coincide with specifically dependent continuants. Note that relational qualities and realizable entities, like roles and dispositions, are imported into physical qualities. %\nb{CM: vedi nota importante tolta}\nb{SB: ci sono varie note commentate...} 

%{\color{red} ****however we do not have spatial locations, i.e., here we are defining only physical qualities that are not spatial locations... do we need to add something like $\SLdcat(x) \sdef \bfopartic(x) \land \neg \bfopartic(x)$ ?}

%{\color{blue} old definition:
%
%$\PQdcat(x)\sdef x \bfoiof{} \sdcntbcat \land \neg(x \bfoiof{} \rqltbcat)$
%
%****actually {\dolce} seems compatible with relational qualities, it is enough to distinguish $\DQTd$ from other kinds of specifically dependencies and add a double $\DQTd$/$\SDd$ dependence for these qualities}  

%{\color{red} ****this mapping is maybe too `weak', it includes into {\dolce} qualities also {\bfo}-roles and {\bfo}-dispositions that, from the examples in the documentation, I'm not sure are {\dolce} qualities;
%however, in the new version of {\dolce} the temporal extension of qualities is included in, but possibly different from, the temporal extension their bearers (in any case I don't see an axiom guaranteeing the temporal co-extensionality of {\bfo} qualities too)}
%
%{\color{red} ****more generally, one can try to understand $(i)$ if roles can be mapped to  \emph{qua-entities}; and $(ii)$ if dispositions can be organized in a space (following what done for capabilities by Stefano and Laure) one could have a single disposition-quality changing its location in this space}
%
%{\color{red} ****{\bfo} does not have temporal or abstract qualities}

\item[\bddf{b2d_Qdcat}] $\Qdcat(x) \sdef \PQdcat(x)$ 

\vspace{1pt}
Only physical qualities exist ({\bfo} has only qualities of independent continuants)

\item[\bddf{b2d_Tdcat}] $\Tdcat(x)\sdef x \bfoiof{} \tregbcat$

\vspace{1pt}
Time intervals coincide with temporal regions. One could consider a stronger definition, i.e., assume that $\Tdcat$ corresponds to $\tintbcat$. However, following (M\ref{Ass2}) we aim to import all the temporal regions.

\item[\bddf{b2d_TRdcat}] $\TRdcat(x) \sdef \Tdcat(x)$

\vspace{1pt}
Among temporal regions there are only time intervals.

\item[\bddf{b2d_Sdcat}] $\Sdcat(x)\sdef x \bfoiof{} \sregbcat$

\vspace{1pt}
Space regions coincide with spatial regions.

\item[\bddf{b2d_PRdcat}] $\PRdcat(x)\sdef \Sdcat(x)$

\vspace{1pt}
Among physical regions there are only space regions.

%\vspace{1pt}
%{\color{blue} {old definition}: 
%
%$\PRdcat(x)\sdef \Sdcat(x) \lor \exists y(\Qdcat(y) \land y \bfoiof{} x)$
%
% ****this old definition ATTEMPT to include universals classifying {\bfo} sdcnt-entitites under physical region; in this way instantiation could represent the TQL and the isa relation could approximate parthood (actually parthood is intensional while isa is extensional)}

\item[\bddf{b2d_Rdcat}] $\Rdcat(x) \sdef \TRdcat(x) \lor \PRdcat(x)$

\vspace{1pt}
Regions are temporal regions or spatial regions.

\item[\bddf{b2d_ABdcat}] $\ABdcat(x)\sdef \Rdcat(x)$

\vspace{1pt}
Among abstracts there are only time intervals and space regions.


%\item[\bddf{b2d_PTdcat}] $\PTdcat(x) \sdef \EDdcat(x) \lor \PDdcat(x) \lor \Qdcat(x) \lor \ABdcat(x)$

\item[\bddf{b2d_TLCd}] $\TLCd(x,t)\sdef (\PDdcat(x) \lor \EDdcat(x) \lor \Qdcat(x)) \land \Tdcat(t) \land \forall u(\bfoexist(x,u) \ifif \bfotpart(u,t))$

\vspace{1pt}
The temporal location of $x$ is the maximal time at which $x$ exists. (In {\bfo}, $\bfotregof$ is defined only on processes and process boundaries). 

%{\color{blue} ****added $\Tdcat(t)$}

\item[\bddf{b2d_Pd}] $\Pd(x,y)\sdef (((\PDdcat(x) \land \PDdcat(y)) \lor (\Tdcat(x) \land \Tdcat(y))) \land \bfoopart(x,y)) \lor (\Sdcat(x) \land \Sdcat(y) \land \forall t(\bfoexist(x,t) \to \bfocpart(x,y,t)))$

\vspace{1pt}
For perdurant and time intervals $\Pd$ coincides with $\bfoopart$ while for space regions it reduces to constant parthood, i.e., $x$ is a temporary part of $y$ during its whole existence (note that in {\bfo}, all the spatial regions exist at least at a time). 

%\vspace{1pt}
%{\color{blue} {old definition}: 
%
%$\Pd(x,y)\sdef \ $\parbox[t]{\textwidth} {$(((\PDdcat(x) \land \PDdcat(y)) \lor (\Tdcat(x) \land \Tdcat(y))) \land \bfoopart(x,y)) \lor \\ (\Sdcat(x) \land \Sdcat(y) \land \exists t(\bfocpart(x,y,t)))  \lor \\
% (\PRdcat(x) \land \PRdcat(y) \land \neg\Sdcat(x) \land \neg\Sdcat(y) \land \bfoisa(x,y))$}
%
%****the extensionality of $\Pd$ probably is not provable in general because we don't have this kind of property for $\bfoisa$}

\item[\bddf{b2d_TPd}] $\TPd(x,y,t) \sdef \EDdcat(x) \land \EDdcat(y) \land \bfocpart(x,y,t)$

\vspace{1pt}
For endurants $\TPd$ coincides with $\bfocpart$. 

\item[\bddf{b2d_PCd}] $\PCd(x,y,t) \sdef \EDdcat(x) \land \PDdcat(y) \land \exists z(\bfotpart(y,z) \land \bfoparticin(x,z,t))$

\vspace{1pt}
$\bfoparticin$ is not defined on process boundaries while {\dolce} does not impose any constraint on the kind of the process involved in $\PCd$. The existential quantification on $z$ aims to mitigate this difference. 


\item[\bddf{b2d_DQTd}] $\DQTd(x,y) \sdef \bfoinh(x,y)$

\vspace{1pt}
The relation of direct quality coincides with inheritance. %\nb{SB: aggiunto}
%{\color{red} ****this seems too restrictive because in {\bfo}  specifically dependent continuants specifically depend only on independent continuant \refbfoax{sdcnt_def} while in {\dolce} qualities can inhere also in dependent endurants and in perdurants; we are `interpreting' $\DQTd$ in a restrictive way, also in this case we would have $\bfoinh(x,y) \to \DQTd(x,y)$ but not vice versa (again, see discussion done for \refbddf{b2d_EDdcat}, \refbddf{b2d_PEDdcat}, and \refbddf{b2d_NPEDdcat})}

\item[\bddf{b2d_EXDd}] $\EXDd(x,y,t) \sdef (\bfosdep(x,y) \land \bfoexist(x,t)) \lor \bfogdep(x,y,t) \lor \bfoparticin(x,y,t) \lor \bfoparticin(y,x,t)$


\vspace{1pt}
$\EXDd$ is the generalization of $\bfosdep$, $\bfogdep$, and $\bfoparticin$ ($\bfoparticin$ counts as a sort of mutual dependence).

%{\color{red} ****this definition is bad; $\EXDd$ is strictly stronger than $\bfosdep$/$\bfogdep$ because  it can hold $(i)$ only at some times (differently from $\bfosdep$) and $(ii)$ between specifically/generically dependent endurants (according to \refbddf{b2d_Qdcat} specifically dependent continuants are mapped to qualities; also in this case it seems more an inclusion (right to left direction) than a definition (but see the discussion relative to \refbddf{b2d_EDdcat}, \refbddf{b2d_PEDdcat}, and \refbddf{b2d_NPEDdcat})}

\item[\bddf{b2d_SLCd}] $\SLCd(x,s,t) \sdef $\parbox[t]{\textwidth} {$(x \bfoiof{t} \idcntbcat \land \neg(x \bfoiof{t} \sregbcat) \land \bfosregof(x,s,t)) \lor \\ 
(x \bfoiof{t} \gdcntbcat \land \exists y(\bfogdep(x,y,t) \land \forall z(\bfogdep(x,z,t) \to \bfocpart(z,y,t)) \land \bfosregof(y,s,t))) \lor  \\  
(\Qdcat(x) \land \exists y(\bfoinh(x,y) \land \forall z(\bfoinh(x,z) \to \bfocpart(z,y,t)) \land \bfosregof(y,s,t))) \lor  \\  
(\PDdcat(x) \land \exists y(\bfostregof(x,y) \land \bfosproj(y,s,t)))$}

\vspace{6pt}
For independent continuants that are not spatial regions, $\SLCd$ coincides with $\bfosregof$ (first disjunct). The spatial location, at $t$, of a generically dependent continuant $x$ is the spatial region of the maximal entity (if it exists) on which $x$ generically depends on at $t$ (second disjunct).  The spatial location of a quality $x$ at $t$ is the spatial region of the maximal (at $t$) entity (if it exists) in which $x$ inheres (third disjunct). The spatial location of a perdurant is the spatial projection of its spatiotemporal location (fourth disjunct).  
Note that in {\bfo}, no axiom guarantees that a specifically dependent continuant $x$ inheres in a unique continuant, therefore for qualities we define the spatial location only when there is a `maximal continuant' in which $x$ inheres in. A similar argument applies for generic dependent continuants.

%%\vspace{3pt}
%%
%%{\color{red} ****in {\dolce} spatial location applies to endurants, qualities, and perdurants.}
%%
%%{\color{red} ****in {\bfo}, no axiom guarantees that a specifically dependent continuant $x$ inheres in a unique continuant, therefore for qualities we define the spatial location only when there is a `maximal continuant' in which $x$ inheres in; similarly for generic dependent continuants (alternatively on could rely on the sum of the spatial regions occupied by the continuants $x$ inheres in or depends on, but {\bfo} does not commit on the existence of sums).}
%
%\item[--] $\Kd(x,y,t) \sdef \ ????$
%
%{\color{red} ****I don't think this can be defined because {\bfo} does not allow different endurants to be spatially co-localized (see also the example changing a leg in the paper of Neil and Alan in the special issues on top-levels)}
%
%{\color{red} ****this also make explicit that some classes of {\dolce} are necessary empty, namely all the classes of entities that depends on other entities spatially co-localized. One could then try to build these entities in a complex way: (1) reify the instantiation of given universals, e.g., one can reify the fact that an amount of matter $m$ is a statue at a given time $m \bfoiof{t} \cn{statue}$; (2) collect all the reified states of the same kind (e.g., statue-states) that are in given relations defined in terms of (spatio-temporal) relations between amount of matters, or given kinds of transformation processes that apply on the amount of matter. This is interesting but complex, it would be better done at the level of models in order to avoid to modify the domain of quantification of {\bfo}.}
%
%\item[--] $\QLd(x,y) \sdef \ ????$
%
%{\color{red} ****{\bfo} qualities are defined only for continuants (and in any case qualities  do not have qualia, see discussion in \refbddf{b2d_TQLd})}
%
%\item[--] $\TQLd(x,y,t) \sdef \ ????$
%
%{\color{blue} old definition:
%
%$\TQLd(x,y,t) \sdef \Qdcat(y) \land y \bfoiof{t} x \land \neg \exists z(y \bfoiof{t} z \land \bfoisa(z,x) \land \neg \bfoisa(x,z))$
%
%****the only ``abstract entities'' considered by {\bfo} are temporal and spatial regions (also spatiotemporal regions that however are not considered by {\dolce})
%
%****in general one could try a link with universals, i.e., one could assume that the instances of $\qltbcat$ are partitioned by means of a set of universals (identified by a predicate $U$) each one corresponding to a quality space in {\dolce}, and then assume that the quale of a quality $q$ at $t$ is the more refined universal under one $U$-universal of which $q$ is an instance of at $t$, i.e.,  $\TQLd(x,y,t) \sdef U(x) \land y \bfoiof{t} x \land \neg \exists u(y \bfoiof{t} u \land u \neq x \land \forall z(z \bfoiof{t} u \to z \bfoiof{t} x))$}
\eflist

One may think that the mapping given by these definitions is too restrictive: in {\dolce} physical and non-physical endurants are not limited to, respectively, independent continuants and generically dependent continuants (the latter are a quite special kind of entities), and so on. This may suggest to include  $x \bfoiof{} \idcntbcat \land \neg(x \bfoiof{} \sregbcat) \to \PEDdcat(x)$ as well as $x \bfoiof{} \gdcntbcat \to \NPEDdcat(x)$, but not the converse formulas. Howewer, we need to remember that we are considering the mapping from {\bfo} to {\dolce}. The starting point is the domain of {\bfo}, i.e., we need first of all to try to classify the entities that belong to the domain of {\bfo} in terms of the categories of {\dolce}. 
By looking at the mappings it is easy to see that all the particulars\footnote{For the possibility to import universals as regions or non-physical endurants, see Sect. \ref{sect_analysis_d2b}.} of {\bfo} are classified in terms of {\dolce} categories except for spatiotemporal regions:\footnote{On the fact that spatiotemporal regions seem superfluous see Sect. \ref{sect_mappings_d2b}. It is simple to modify the definitions to include spatiotemporal regions under {\dolce} regions.} $(i)$ independent continuants which are not spatial regions are mapped to physical endurants; $(ii)$ spatial regions to space regions; $(iii)$ generically dependent continuants to non-physical endurants; $(iv)$ specifically dependent continuants to {\dolce} qualities; $(v)$ process and process boundaries to perdurants; and $(vi)$ temporal regions to time intervals. The fact that {\dolce} intuitively accepts, for instance, additional physical or non-physical endurants shows that, in general, {\dolce} has a domain larger than the domain of {\bfo}. Our methodological choice (M\ref{Ass3}) does not allow the mappings to `enrich' the domain of {\bfo} with new entities. %\nb{CM: per (M\ref{Ass3}) non per (M\ref{Ass2}) come dicevamo, le def. sintattiche non toccano il dominio, introducono una (parziale) riclassificazione delle entità su cui si quantifica}  
However, by introducing the mapping at the semantic level, i.e., in this case, as an operator translating {\bfo}-structures into a {\dolce}-structure, one could enrich the original domain of {\bfo} by set-theoretically building new entities. This is the approach followed in the literature to map theories of time based on points to theories based on intervals, see \citep{Van-Benthem:1983ka}. %\footnote{See van Benthem, J., \emph{The Logic of Time}, Springer, 2nd ed., 1991.} %\nb{CM: riferimento in bibliografia} 
The theory based on intervals does not admit points, but points can be built as sets of intervals staying in a given relation that is definable in the theory of intervals.  Analogously, one can think of building some entities, e.g., statues as opposed to amounts of clay, starting from the amounts of clay and the specific kinds of universals they instantiate. Like in Section \ref{sect_d2b}, the investigation of this kind of `semantic mapping' is not considered in this work.%\nb{CM: es. per fare capire di cosa si tratta?} \nb{SB: secondo me non serve, c'è la citazione}

%{\color{red} ****The last three definitions (PED, NPED, F) nicely illustrate the problem of mappings when one has ontologies with different domains. These definitions approximate $\EDdcat$, $\PEDdcat$, and $\NPEDdcat$ from the point of view of {\bfo}, i.e., they individuate \emph{among the entities in the domain of {\bfo}} the ones that reasonably match the idea of $\EDdcat$, $\PEDdcat$, and $\NPEDdcat$ in {\dolce}. However, concerning these kinds of entities, {\dolce} seems to have a larger domain, i.e., on would want to say, for instance for $\NPEDdcat$s, just $x \bfoiof{} \gdcntbcat \to \NPEDdcat(x)$ while in general one could have other $\NPEDdcat$s. This however is true only by considering the domain of {\dolce} while in the domain of {\bfo}, generically dependent continuant cover the whole possible $\NPEDdcat$s, there are no additional entities in {\bfo} that can be seen as $\NPEDdcat$s. In terms of semantic links between structures, the set of mappings can be seen as a sort of `operator' that (possibly) translates a {\bfo}-structure into a {\dolce}-structure, but one always needs to start from the entities in the domain of {\bfo} and to construct a {\dolce}-structure in terms of these entities. One could introduce in the {\dolce}-structure some entities that are set-theoretical constructions, but the basic elements of these set-theoretical constructions always are in the {\bfo}-domain. This is different from the perspective where we consider a sort of `union' of the two theories (that are assumed to have disjoint vocabularies) and where we have a common domain that allows us to determine set-theoretical relations between the primitives classes and relations.}
%
%{\color{red} ****{\dolce} features contains other kinds of entities, it is only an inclusion, but see the discussion relative to \refbddf{b2d_EDdcat}, \refbddf{b2d_PEDdcat}, and \refbddf{b2d_NPEDdcat}}

%%=================================
%\subsection{Preservation of the original {\dolce} axioms}\label{sect_check_dolce_preservation}
%%=================================

Furthermore, notice that \refbfoax{univ_are_insta} states that all the universals are non-empty. From an applicative perspective, this is a strong constraint because it forces the user to model even entities which might not be relevant to the application (and perhaps time consuming to analyze). Note that, once \refbfoax{univ_are_insta} is removed, the existential constraints in $\bfo$ are compatible with the instantiation of only some categories. From a technical perspective, \refbfoax{univ_are_insta} requires very large models that make the identification and management of counterexamples very difficult even with the support dedicated software. For these reasons, we do not consider \refbfoax{univ_are_insta} in the comparison.   

In the following, $\thbfobdmap$ is the set $\thbfo{\setminus}\{$\refbfoax{univ_are_insta}$\}$ with the definitions of Sect.~\ref{sect_mappings_b2d}, %together with the syntactic definitions introduced in Sect.~\ref{sect_dolce}, 
i.e., $\thbfobdmap = \{\thbfo{\setminus}\{$\refbfoax{univ_are_insta}$\}\} \cup \{$\refdbdf{b2d_PDdcat},\ldots,\refdbdf{b2d_SLCd}$\}$. %\nb{CM: controllare se non consideriamo anche altri assiomi [assiomi in arancio (commento tra me e Francesco)]}\nb{CM: tolto discorso sulle def. sintattiche non usate nei mappings se non le due già citate}
%
%In the following, $\thbfo$ is the set of axioms characterizing {\bfo} as presented in Section \ref{sect_bfo},  $\bdmap$ is the set of mappings from {\bfo} to {\dolce}, i.e., $\dbmap = \{\refdbdf{b2d_PDdcat}$-$\refdbdf{b2d_SLCd}\}$, and $\thbfobdmap =  \thbfo \cup \dbmap$.
%
%Some of the axioms in {\dolce} involve several subcategories and/or relations of {\dolce} that has not been defined in terms of {\bfo}. In the following we do not consider these axioms. 
%
%For this direction of the mappings, we still lack the proofs or the counterexamples for some axioms (expressible by the limited vocabulary taken into account in the mappings) among the ones reported in Sect.~\ref{sect_dolce}. We label these formulas in red by prefixing an asterisk. In some cases, we provide our expectation (just an expert guessing at this stage) followed by a short motivation.
Some axioms of {\dolce} use relations or categories that have not been defined in the definitions. When possible and relevant we considered approximations of these axioms as expressible in the {\dolce} language, otherwise we set them aside. Additional details as well as the proofs of all the theorems can be found in \citep{D24}. Again, in the following analysis we mainly focus on the results that point out some ontological differences between $\dolce$ and $\bfo$. 


%Let us include \refdbdf{d2b_mten}-\refdbdf{d2b_gdep} into $\dbmap$.


%{\color{red} Several proofs has been verified by using theorems provers...}\nb{CM: aggiungere qualche considerazione generale su numero assiomi dimostrati ecc.?}\nb{SB: forse si potrebbe dare il n. tot. e la percentuale provata (ma allora da aggiungere anche nella sez. 5)}

%======================================
\subsection{Analysis}\label{sect_analysis_b2d}
%======================================

The results obtainable starting from $\thbfobdmap$ %discussed in Sect.~\ref{sect_mappings_b2d} 
show that, with the exception of the spatiotemporal regions, all the particulars of {\bfo} find their place in {\dolce}. The possibility to avoid spatiotemporal regions, once one has the temporal and the spatial locations of entities, has aleady been briefly discussed. % analyzed in Sect.~\ref{occupies_streg}.\nb{FC: attuare o eliminare} 
For importing {\bfo} universals into {\dolce} we already suggested some possibilities, e.g. mapping universals to regions or to non-physical endurants. Both alternatives would require to reconsider the mappings \refbddf{b2d_NPEDdcat} and  \refbddf{b2d_Rdcat}, and perhaps \refbddf{b2d_TRdcat} and \refbddf{b2d_PRdcat}. On the other hand, some of the original categories of {\dolce} remain empty with this mapping. It is the case of $\ASdcat$, $\ARdcat$, $\TQdcat$, and $\AQdcat$. Other categories are drastically reduced: physical qualities/regions reduce to spatial locations/space regions and temporal regions reduce to time intervals. In agreement with earlier observations, this suggests that {\dolce} accepts a larger variety of entities. This is also confirmed by the possibility to have in {\dolce} spatially co-localized, and possibly layered, entities related by temporal parthood (mutual $\TPd$-parthood at a time) and constitution (see the discussion in Sect.~\ref{sect_analysis_d2b}). Whether this larger variety of entities translates into a higher expressive power needs to be investigated. As discussed in the case of spatiotemporal regions, the introduction of more complex definitions could mitigate the gap.

Concerning the preservation of {\dolce}, our results show that the majority of the original axioms of {\dolce}  cannot be proved in $\thbfobdmap$. One could suggest that this result is due to an insufficient development of the definitions, or claim that there a genuine difference between the two ontologies, or even conclude that a comparison of the mappings in the two directions shows that {\bfo} is someway weaker than {\dolce}. At this stage, we do not have enough elements to assess the issue. A deeper analysis of the counterexamples to some theorems is needed and, most likely, a more complex situation with pros and cons on both sides may emerge.  

Few, and quite technical, differences between the two theories seem to cause several systematic problems for a comprehensive mapping. In {\dolce}, $\PREd$ is defined only for the entities that have a temporal extension, see \refdolcedf{dfPREd}, while in {\bfo} $\bfoexist$ is a primitive relation.\footnote{One could think that $\bfotregof$ corresponds to $\TLCd$ but actually $\bfotregof$ is defined only for occurents and it is only minimally related to $\bfoexist$.} % The counterexample\nb{rivedere dopo aver posizionato i controesempi} for \refbdth{b2d_d_partictime} shows that i
In {\bfo} an entity may exist at two non overlapping temporal regions without existing at any bigger temporal region. In these situations the condition $\forall u(\bfoexist(x,u) \ifif \bfotpart(u,t))$ in the definition of $\TLCd(x,t)$, see \refbddf{b2d_TLCd}, is never satisfied and the relation $\PREd$ is not satisfied. This problem impacts the preservation of several axioms of {\dolce}  %on the proofs in Sect.~\ref{sect_check_dolce_preservation} 
because $\PREd$ is heavily used in the characterization of the primitives of {\dolce} (in particular ${\thbfobdmap \nvdash \refdolceax{d_partictime}}$). At the same time, this problem seems to have a technical, more than ontological, nature; after all, in both ontologies the entity exists at both times. A similar problem affects axioms like  \refdolceax{TPd_temp_addictivity} and \refdolceax{PCd_temp_addictivity} where from the holding of a given relation at two times, one would expect to infer that the relation holds also at the sum of the times (provided such sum exists). 
However, the fact that an entity exists at two times but not at their sum prevents, for the majority of relations, the possibility for the relation to hold at the sum.%\nb{CM: la frase che avevi scritto tu secondo me non andava bene, ho quindi rimesso la precedente modificandola un po'}\nb{SB: ok}
%Generally, a temporary relation does not hold at a time unless all the related entities exist at that time, thus when it applies to two entities that exist at different temporal regions that relation may not hold at the temporal region which is their sum.\nb{SB: mancava qualcosa in questa frase, ho cercato di dare un senso. Da controllare!!}
 %, a theorem analogous to \refbdth{b2d_TPd_temp_addictivity} and \refbdth{b2d_PCd_temp_addictivity} is falsified.
%
%
The {\bfo} relation $\bfosregof$ is one of these relations: a continuant can occupy spatial regions (even the same spatial region) at two given times without having a spatial location at the sum of these times. % (see the counterexample for \refbdth{b2d_TPd_up_slc})\nb{anche qui sarà da modificare dopo inserimento controesempi}. %In these cases we would not have the spatial location at the sum of the times. 
%In these cases, the fact that the entity does not exist at the sum of the times rules out (for the majority of relations) the possibility for the relation to hold at the sum. The {\bfo} relation $\bfosregof$ suffers this problem, i.e., a continuant can occupy spatial regions (even the same spatial region) at two given times without having a spatial location at the sum of these times (see the counterexample for \refbdth{b2d_TPd_up_slc}). %In these cases we would not have the spatial location at the sum of the times. 
This fact, together with the definition of $\SLCd$ \refbddf{b2d_SLCd}, clarifies why \refdolceax{TPd_up_slc} and several other {\dolce} theorems involving $\SLCd$ are falsified.
%The presence of spatiotemporal regions and $\bfotproj/\bfosproj$ relations together with the intricate links between $\bfosregof$, $\bfoopart$, $\bfocpart$, $\bfolocated$, and $\bfooccurs$ further complicates the domain of space and spatial location (at least from the formal perspective), impacting all the theorems involving $\SLCd$.
%
\bflist
\item[\dolcedf{dfPREd}] $\PREd(x,t) \sdef \exists u(\TLCd(x,u) \land \Pd(t,u))$ 

%\item[\dolceax{d_partictime}] $(\EDdcat(x) \lor \PDdcat(x) \lor \Qdcat(x)) \to \exists t(\TLCd(x,t))$ 

\item[\dolceax{TPd_temp_addictivity}] $\TPd(x,y,t) \land \TPd(x,y,u) \land \SUMd(s,t,u) \to \TPd(x,y,s)$ 

\item[\dolceax{PCd_temp_addictivity}] $\PCd(x,y,t) \land \PCd(x,y,u) \land \SUMd(s,t,u) \to \PCd(x,y,s)$ 

\item[\dolceax{TPd_up_slc}] $\TPd(x,y,t) \land \SLCd(x,s,t) \to \exists r (\SLCd(y,r,t))$ 

%\item[\bdth{b2d_d_partictime}] $\thbfobdmap \nvdash $ {\refdolceax{d_partictime}} 

%\item[\bdth{b2d_TPd_temp_addictivity}] $\thbfobdmap \nvdash $ {\refdolceax{TPd_temp_addictivity}} 
%
%\item[\bdth{b2d_PCd_temp_addictivity}] $\thbfobdmap \nvdash $ {\refdolceax{PCd_temp_addictivity}}
%
%\item[\bdth{b2d_TPd_up_slc}] $\thbfobdmap \nvdash $ {\refdolceax{TPd_up_slc}} 
\eflist


This analysis suggests that a different mapping technique may be needed. Rather than encapsulating the relation between $\bfoexist$ and $\TLCd$ into the mapping  \refbddf{b2d_TLCd}, one could take a more articulated procedure: first introduce a direct mapping between $\bfoexist$ and $\PREd$, then define $\TLCd$ by using $\PREd$ (as defined in the mapping), e.g.,
%
\bflist
\item[] $\PREd(x,t) \sdef (\PDdcat(x) \lor \EDdcat(x) \lor \Qdcat(x)) \land \bfoexist(x,t)$
\item[] $\TLCd(x,t) \sdef \forall u(\PREd(x,u) \ifif \Pd(u,t))$
\eflist
%  
In this way, entities that, for instance, exist at two times but not at their mereological sum would still lack a temporal location $\TLCd$ but this would not prevent $\PREd$ to hold when applied to them (due to the first mapping). We can then try to recover some theorems that do not require $\TLCd$ at the price of possibly losing the original connection between $\PREd$ and $\TLCd$. The applicability of this mapping technique to other primitives and its actual impact are not further studied in this paper. 

%\medskip
The problems highlighted up to this point were discussed because of their impact but are primarily of technical nature. The mapping highlights also genuine ontological differences.
% that do not depend on technical choices in the mapping.\nb{SB: ho riscritto} 
First, the defined $\Pd$, like $\bfoopart$, does not satisfy the supplementation axiom \refdolceax{PdSupp} assumed in {\dolce}. Second, the relation $\bfoinh$ is not equivalent to the original $\DQTd$, in particular it does not satisfy the non-migration principle \refdolceax{DQTdUnicity}. For relational qualities this can be problematic if, for instance, one wants to distinguish ``Mary loves John'' from ``John loves Mary'': in both cases we obtain a relational quality inhering in both John and Mary. Third, the reflexivity of the defined $\TPd$, like the one of $\bfocpart$, does not hold for all the continuants. It follows that in {\bfo} one can have continuants for which $\bfocpart$ is not defined.  Fourth, while in {\dolce} all the perdurants have participants at every time they exist \refdolceax{PCd_existence_participant}, in {\bfo}, processes need to have at least a participant but this does not hold for process boundaries. Furthermore, in {\bfo}, continuants do not necessarily participate in processes while in {\dolce} all the endurants participate in a process when they exist \refdolceax{PCd_existence_perdurant}.
%
\bflist
\item[\dolceax{PdSupp}] $(\ABdcat(x) \lor \PDdcat(x)) \land \neg\Pd(x,y) \to \exists z (\Pd(z,x) \land \neg \Od(z,y))$ 

\item[\dolceax{DQTdUnicity}] $\DQTd(x,y) \land \DQTd(x,z) \to y=z$ 

\item[\dolceax{PCd_existence_participant}] $\PDdcat(x) \land \PREd(x,t) \to \exists yu(\Pd(u,t) \land \PCd(y,x,u))$ 

\item[\dolceax{PCd_existence_perdurant}] $\EDdcat(x) \land \PREd(x,t) \to \exists yu (\Pd(u,t) \land \PCd(x,y,u))$ 

%\item[\bdth{b2d_PdSupp}] $\thbfobdmap \nvdash $ {\refdolceax{PdSupp}} 
%
%\item[\bdth{b2d_DQTdUnicity}] $\thbfobdmap \nvdash $ {\refdolceax{DQTdUnicity}} 
%
%\item[\bdth{b2d_PCd_existence_participant}] $\thbfobdmap \nvdash $ {\refdolceax{PCd_existence_participant}} 
%
%\item[\bdth{b2d_PCd_existence_perdurant}] $\thbfobdmap \nvdash $ {\refdolceax{PCd_existence_perdurant}} 
\eflist

%============================================
\section{Grounding OWL mappings on FOL mappings}\label{sect_FOL_OWL}
%============================================

For both $\bfo$ and $\dolce$ an OWL version exists. These versions are used when usability and tractability become important applicative factors that prevail over the deep and explicit characterization of ontological commitments. Given the low expressive power of OWL, the majority of the axioms in the FOL versions and the majority of the mappings introduced in the previous sections---mappings that, in their turn, are expressed in the form of FOL syntactic definitions---cannot be preserved or can be only very roughly approximated. The semantic correspondences established via the FOL mappings can however be used to {ground} and justify OWL mappings.

In OWL, $\mathit{subClassOf}$ mappings are arguably among the most important ones. A $\mathit{subClassOf}$ mapping assures that a class of an ontology is subsumed by a class of another ontology. To justify a $\mathit{subClassOf}$ mapping from $\pr{C_b}$ to $\pr{C_d}$ where, for instance, $\pr{C_b}$ is a $\bfo$ category and $\pr{C_d}$ is a $\dolce$ category, the following two conditions must hold (where $\pr{SUB}(\pr{C_d})$ is the set of all the subcategories of $\pr{C_d}$ in the $\dolce$ taxonomy in Fig.~\ref{fig_tax_dolce} that have been explicitly considered in the mapping from $\bfo$ to $\dolce$):
\bflist
\item[(c1)] $\thbfobdmap \vdash \exists t(x \bfoiof{t} \cn{C_b}) \to \pr{C_d}(x)$ 
\item[(c2)] $\thbfobdmap \nvdash \exists t(x \bfoiof{t}  \cn{C_b}) \to \pr{C}(x)$, for all $\pr{C} \in \pr{SUB}(\pr{C_d})$ 
%\item[] $\thbfobdmap \nvdash \exists t(x \bfoiof{t} \mtenbcat) \to \NPEDdcat(x)$ 
\eflist
%
Condition (c1) assures that $\pr{C_b}$ is subsumed by $\pr{C_d}$ while (c2) assures that $\pr{C_b}$ is not subsumed by any subcategory of $\pr{C_d}$, i.e., (c1)+(c2) guarantee that $\pr{C_d}$ is the minimal $\dolce$ category subsuming $\pr{C_b}$.  

For instance, the holding of:
%
\bflist
%\item $\mathtt{sucClassOf(BFO{:}}$`$\mathtt{material \ entity}$' $\mathtt{DOLCE{:}Endurant)}$
\item[] $\thbfobdmap \vdash \exists t(x \bfoiof{t} \mtenbcat) \to \EDdcat(x)$ 
\item[] $\thbfobdmap \nvdash \exists t(x \bfoiof{t} \mtenbcat) \to \PEDdcat(x)$ 
\item[] $\thbfobdmap \nvdash \exists t(x \bfoiof{t} \mtenbcat) \to \NPEDdcat(x)$ 
\eflist
 %
justifies a $\mathit{subClassOf}$ mapping from $\bfo$ material entities to $\dolce$ endurants (the category $\ASdcat$ of arbitrary sums has been ruled out from the mapping from $\bfo$ to $\dolce$). 

A similar reasoning can be done for $\mathit{disjointWith}$ and $\mathit{subPropertyOf}$ mappings. Note however that sub-properties mappings often require to restrict the domain and range of the source relation to conjunctions of classes.  To explicitly express this kind of mappings, the Semantic Web Rule Language (SWRL)  \citep{swirl} %is
might be needed.\nb{CM: non sono sicurissimo di questo, non ricordo più bene, inoltre serve un riferimento}\nb{SB: ho indebolito mettendo "might", direi di lasciare così}

The OWL-versions of $\bfo$ and $\dolce$ and all the identified OWL-mappings are available at the GitHub repository at \url{https://github.com/OntoCommons/OntologyFramework}.  

%{\color{red} qualche cosa anche vedendo la presentazione per Ontocommons?}\nb{[FC: non ho visto bene i mapping owl]}\nb{SB: cosa pensavate di mettere in questa sezione?}

%============================================
\section{Conclusion}\label{sect_conclusion}
%============================================
The construction of an ontology ecosystem for information classification and exchange requires formal alignments across ontologies. From the theoretical viewpoint, the most essential alignments are those across foundational ontologies. This paper has presented a general strategy and has motivated some methodological assumptions for such a construction.
Furthermore, it has applied this approach to two well-known ontologies, namely {\bfo} and {\dolce}, which might seem to provide an ideal test for formal alignments due to their overall similarity. The analysis has revealed that similarities may hide deep differences and that even apparently minor modeling differences have a relevant impact when formal alignments are sought.

The applied ontology research community has not yet investigated in depth the formal alignment of foundational ontologies. One can imagine the development of a toolkit of strategies, assumptions and methodologies to guide the construction of formal ontology alignments depending on what one aims to preserve across the systems. Some alternatives have been already highlighted in the paper, including a discussion of their consequences. Yet, there are many alternatives and we lack even a general framework to systematically classify them. 
Overall, the study in this paper has made clear that the strong interactions existing across the notions used in a foundational ontology, let them be categories or relations, may turn even small changes in the adopted definitions into important changes in how much of the two systems the mapping may hope to align.

As foundational ontologies mature in terms of their formalization and conceptual coherence, the exploitation of formal alignments across these systems acquires more relevance and gets the community closer to the construction of ontology-based marketplace for reliable data and information exchange.

In the future, we plan to deepen the analysis here presented comparing what can be gained and lost depending on the strategy, assumptions and methodologies. We are also investigating formal alignments across other ontological systems that rely on with quite different ontological viewpoints like the EMMO ontology \citep{EMMO}.

%=================================================

\begin{acks}
This material has been developed within the OntoCommons project (GA 958371, ontocommons.eu). The authors thank the participants of the OntoCommons project for their support and in particular Emanuele Ghedini, Francesco A. Zaccarini, Nicola Guarino, Daniele Porello, and Laure Vieu.
\end{acks}

\nocite{label} 
\bibliographystyle{ios2-nameyear}
\bibliography{biblioFC}

\end{document}