Answers.Body: <p>For the approach of formal ontology, it is usual to keep theory and its model together, and name this &quot;ontology&quot; subsuming &quot;formal&quot;. So, just put theory and model on one CG.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2022-01-02T14:47:07.013Z
Answers.Text: Your answer could be improved with additional supporting information. Please [edit] to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers [in the help center](/help/how-to-answer).
Answers.UserDisplayName: Community
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2022-01-03T09:31:49.463Z
Answers.Text: @Alex In general theories and models are distinct entities that are related by the satisfaction relation, M⊨T. So embedding the model and the theory in one graph does not seem to me to be appropriate. Further, the model and theory may be presented in different logical systems (see Goguen and Burstall's [Theory of Institutions](https://cseweb.ucsd.edu/~goguen/projs/inst.html))
Answers.UserDisplayName: Patrick Browne
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2022-01-02T09:06:32.263Z
Answers.LastActivityDate: 2022-01-02T09:06:32.263Z
Answers.UserDisplayName: Alex Shkotin
Body: <p>The <strong>Mereology Theory</strong> below contains three first-order axioms that represent a part of a <a href="https://plato.stanford.edu/entries/mereology/" rel="nofollow noreferrer">mereology</a> theory. For this posting, it is important that the set of axioms should be considered as a <a href="https://en.wikipedia.org/wiki/Theory_(mathematical_logic)" rel="nofollow noreferrer">theory</a>.</p>
  <p><strong>Mereology Theory</strong></p>
  <p><strong>Reflexivity</strong> <span class="math-container">$\forall x : part(x,x)$</span></p>
  <p><strong>Antisymmetry</strong> <span class="math-container">$\forall x  \forall y : ((part(x,y) \land part(y,x)) \implies (x = y))$</span></p>
  <p><strong>Transitivity</strong>  <span class="math-container">$\forall x  \forall y \forall z :((part(x,y) \land part(y,z))  \implies part(x,z))$</span></p>
  <p>Here is my naïve attempt to present the theory as a set of <a href="https://en.wikipedia.org/wiki/Conceptual_graph" rel="nofollow noreferrer">conceptual graphs</a> (CG).</p>
  <p><a href="https://i.sstatic.net/4A0hi.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/4A0hi.png" alt="enter image description here" /></a></p>
  <p>My understanding of the above CGs is as follows:</p>
  <ol>
  <li>The variables are universally quantified, not default for CGs, but allowed in extended CG (ECG).</li>
  <li>The inner graphs are all related by conjunction, which is default for GCs and I assume for ECGs.</li>
  <li>The arrow on graph representing reflexivity is bi-directional.</li>
  <li>Both antisymmetry and transitivity are represented by an IF-THEN contexts.</li>
  <li>Dotted lines are co-references.</li>
  <li>Equality (=) is actually commutative, but is represented as a directed relation .</li>
  <li>Each inner graph asserts a single proposition, labelled <strong>Proposition</strong>.</li>
  <li>The outer graph is labeled <strong>MereologyTheory</strong>, I am not sure that this is correct ECG syntax.</li>
  </ol>
  <p>Below is a <em>possible</em> model of the above theory:</p>
  <p><strong>Mereology Model</strong> Mathematical notation</p>
  <p><span class="math-container">$Entities = \{ a,b  \}$</span></p>
  <p><span class="math-container">$Relations = \{part(a,a),part(a,b),part(b.b)\}$</span></p>
  <p>Obviously there are many other possible models. <strong>MereologyModel</strong> below is my attempt to visualize this model as a CG. I am not sure that putting the label <strong>MereologyModel</strong> is correct CG syntax or denotes it as a model of  <strong>MereologyTheory</strong> .</p>
  <p><a href="https://i.sstatic.net/HQaIN.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/HQaIN.png" alt="enter image description here" /></a></p>
  <p><strong>Question:</strong></p>
  <p>In CG visual notation, how are theories and models related?
  It seems to me that basic CGs can represent FOL sentences and the relation between such sentences. According to <a href="https://rads.stackoverflow.com/amzn/click/com/1849967695" rel="nofollow noreferrer" rel="nofollow noreferrer">Chein and Mugnier</a> the subsumption relation is defined by graph homomorphisms between CGs. Is  the model/theory relation for CGs also defined in terms of graph homomorphisms? I am aware that in general a model satisfies a theory i.e. <span class="math-container">$M \vDash T$</span>. Does the graph homomorphism provide the necessary syntactic mapping to enable model and theory to be related?</p>
  <p>Note  <a href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.460.8912&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">CGs</a> can be represented in <a href="http://www.jfsowa.com/talks/clintro.pdf" rel="nofollow noreferrer">Common Logic</a> <a href="https://standards.iso.org/ittf/PubliclyAvailableStandards/c066249_ISO_IEC_24707_2018.zip" rel="nofollow noreferrer">(ISO zipped PDF)</a>, which would permit a formal proof that all the axioms of the theory are satisfied in the model.</p>
  
Tags: <logic><knowledge-representation><ontology>
Title: How do I show the relationship between theories and models using Conceptual Graphs?
UserDisplayName: Patrick Browne
ThreadText: # How do I show the relationship between theories and models using Conceptual Graphs?
  
  (Asked by: username_0 on 2021-12-21)
  
  The **Mereology Theory** below contains three first-order axioms that represent a part of a [mereology](https://plato.stanford.edu/entries/mereology/) theory. For this posting, it is important that the set of axioms should be considered as a [theory](https://en.wikipedia.org/wiki/Theory_(mathematical_logic)).
  
  **Mereology Theory**
  
  **Reflexivity** $\forall x : part(x,x)$
  
  **Antisymmetry** $\forall x \forall y : ((part(x,y) \land part(y,x)) \implies (x = y))$
  
  **Transitivity** $\forall x \forall y \forall z :((part(x,y) \land part(y,z)) \implies part(x,z))$
  
  Here is my naïve attempt to present the theory as a set of [conceptual graphs](https://en.wikipedia.org/wiki/Conceptual_graph) (CG).
  
  [![enter image description here](https://i.sstatic.net/4A0hi.png)](https://i.sstatic.net/4A0hi.png)
  
  My understanding of the above CGs is as follows:
  
  1. The variables are universally quantified, not default for CGs, but allowed in extended CG (ECG).
  2. The inner graphs are all related by conjunction, which is default for GCs and I assume for ECGs.
  3. The arrow on graph representing reflexivity is bi-directional.
  4. Both antisymmetry and transitivity are represented by an IF-THEN contexts.
  5. Dotted lines are co-references.
  6. Equality (=) is actually commutative, but is represented as a directed relation .
  7. Each inner graph asserts a single proposition, labelled **Proposition**.
  8. The outer graph is labeled **MereologyTheory**, I am not sure that this is correct ECG syntax.
  
  Below is a *possible* model of the above theory:
  
  **Mereology Model** Mathematical notation
  
  $Entities = \{ a,b \}$
  
  $Relations = \{part(a,a),part(a,b),part(b.b)\}$
  
  Obviously there are many other possible models. **MereologyModel** below is my attempt to visualize this model as a CG. I am not sure that putting the label **MereologyModel** is correct CG syntax or denotes it as a model of **MereologyTheory** .
  
  [![enter image description here](https://i.sstatic.net/HQaIN.png)](https://i.sstatic.net/HQaIN.png)
  
  **Question:**
  
  In CG visual notation, how are theories and models related?
  It seems to me that basic CGs can represent FOL sentences and the relation between such sentences. According to [Chein and Mugnier](https://rads.stackoverflow.com/amzn/click/com/1849967695) the subsumption relation is defined by graph homomorphisms between CGs. Is the model/theory relation for CGs also defined in terms of graph homomorphisms? I am aware that in general a model satisfies a theory i.e. $M \vDash T$. Does the graph homomorphism provide the necessary syntactic mapping to enable model and theory to be related?
  
  Note [CGs](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.460.8912&rep=rep1&type=pdf) can be represented in [Common Logic](http://www.jfsowa.com/talks/clintro.pdf) [(ISO zipped PDF)](https://standards.iso.org/ittf/PubliclyAvailableStandards/c066249_ISO_IEC_24707_2018.zip), which would permit a formal proof that all the axioms of the theory are satisfied in the model.
  
  **Tags:** logic, knowledge-representation, ontology
  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_1 on 2022-01-02. Score: 0
  
  For the approach of formal ontology, it is usual to keep theory and its model together, and name this "ontology" subsuming "formal". So, just put theory and model on one CG.
  
  > **Comments:**
  > **username_2**: Your answer could be improved with additional supporting information. Please [edit] to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers [in the help center](/help/how-to-answer).  
  > **username_0**: @username_1 In general theories and models are distinct entities that are related by the satisfaction relation, M⊨T. So embedding the model and the theory in one graph does not seem to me to be appropriate. Further, the model and theory may be presented in different logical systems (see Goguen and Burstall's [Theory of Institutions](https://cseweb.ucsd.edu/~goguen/projs/inst.html))  
  
  ---
  
  