Body: <p><strong>Theory 1</strong>  shows three axioms and two definitions, written in First Order Logic (FOL), that represents a fragment 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 is considered as a <a href="https://en.wikipedia.org/wiki/Theory_(mathematical_logic)" rel="nofollow noreferrer">theory</a> (i.e. a set of axioms together with theorems as a logical consequence of those axioms). In the context of this question, the particular axioms are not significant. Any other set of axioms forming a consistent theory would be equally acceptable.</p>
  <p><strong>Theory 1</strong></p>
  <p><strong>Axioms</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><strong>Definitions</strong></p>
  <p><strong>Overlap</strong> : <span class="math-container">$\forall x,y \colon (overlap(x,y) \iff(\exists z \colon  (part(z,x) \land part(z,y)))$</span></p>
  <p><strong>Proper Part</strong> : <span class="math-container">$\forall x,y \colon (proprPart(x,y) \iff (part(x,y) \land \neg part(y,x)))$</span></p>
  <p>I am using <a href="https://cafeobj.org/" rel="nofollow noreferrer">CafeOBJ</a> to represent the above logical axioms and definitions, shown in <strong>Listing 1</strong>:</p>
  <p><strong>Listing 1</strong></p>
  <pre><code>   mod M{
      [E]
      preds overlap part properPart : E E
   -- axioms
   ax [M1] : \A[x:E] part(x,x) .  
   ax [M2] : \A[x:E]\A[y:E] ((part(x,y) &amp; part(y,x)) -&gt; (x = y))  .
   ax [M3] : \A[x:E]\A[y:E]\A[z:E]((part(x,y) &amp; part(y,z))  -&gt; part(x,z)) .
   -- definitions
   ax [DM1] : \A[x:E]\A[y:E] (properPart(x,y) &lt;-&gt; (part(x,y) &amp; ~(part(y,x)))) .  
   ax [DM2] : \A[x:E]\A[y:E] (overlap(x,y) &lt;-&gt;  (\E[z:E] (part(z,x) &amp; part(z,y)))) .  
      }
  </code></pre>
  <p>Note that the logical theory is contained in a <em>named module</em> called <code>M</code>. The variables are over a domain of generic entities <code>E</code>, universal and existential quantification are denoted  by  <code>\A[x:E]</code> and  <code>\A[x:E]</code> respectively. In CafeOBJ, named modules allow one to structure signatures, theories, sub/super theories, and models using the <a href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.74.5613&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">Theory of Institutions</a> (<a href="https://cseweb.ucsd.edu/%7Egoguen/pps/iccs05.pdf" rel="nofollow noreferrer">TOI</a>).</p>
  <p>Below is my naïve attempt to present the axioms as a set of <a href="https://en.wikipedia.org/wiki/Conceptual_graph" rel="nofollow noreferrer">conceptual graphs</a> (CG).  My motivation for using <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> is that they provide an intuitive visualization of logic and have a direct relation to <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>.</p>
  <p><a href="https://i.sstatic.net/KOZaE.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/KOZaE.png" alt="enter image description here" /></a></p>
  <p>The above CG was produced using <a href="https://www.cs.nmsu.edu/%7Ehdp/CGTools/proceedings/tools/1999Compliant/CharGer.zip" rel="nofollow noreferrer">CharGer</a> software as Java zip file (<a href="https://www.cs.nmsu.edu/%7Ehdp/CGTools/proceedings/papers/CharGer.pdf" rel="nofollow noreferrer">manual</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 three graphs are all related by conjunction, which is default for GC.</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 CG asserts a single proposition, labelled <strong>Proposition</strong>.</li>
  </ol>
  <p><strong>Question:</strong></p>
  <p>How do I present <strong>Theory 1</strong> using CGs?  Do I need some labeling that indicates that a set of concepts represent a theory. Or are theories represented by some enclosing <em>special</em> type of concept?</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2022-01-02T08:41:52.717Z
Comments.Text: DOL project may be helpful https://www.omg.org/spec/DOL. see for ex. [![Annex I](https://i.sstatic.net/yYs5n.png)](https://i.sstatic.net/yYs5n.png)
Comments.UserDisplayName: Alex Shkotin
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2022-01-03T10:01:20.003Z
Comments.Text: @Alex Thanks the link is useful, but I am more interested in FOL <-> CG mappings and model/theory representation using CGs.
Comments.UserDisplayName: Patrick Browne
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2022-01-04T09:35:45.687Z
Comments.Text: It seems that this post starts to become more complex. If you have multiple questions (even if they are related), I would recommend that you split them into multiple posts.
Comments.UserDisplayName: nbro
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2022-01-08T10:41:50.470Z
Comments.Text: @nbro I have tried to simplify the question.
Comments.UserDisplayName: Patrick Browne
Tags: <logic><knowledge-representation><ontology>
Title: How are theories represented using Conceptual Graphs?
UserDisplayName: Patrick Browne
ThreadText: # How are theories represented using Conceptual Graphs?
  
  (Asked by: username_0 on 2021-12-02)
  
  **Theory 1** shows three axioms and two definitions, written in First Order Logic (FOL), that represents a fragment of a [mereology](https://plato.stanford.edu/entries/mereology/) theory. For this posting, it is important that the set of axioms is considered as a [theory](https://en.wikipedia.org/wiki/Theory_(mathematical_logic)) (i.e. a set of axioms together with theorems as a logical consequence of those axioms). In the context of this question, the particular axioms are not significant. Any other set of axioms forming a consistent theory would be equally acceptable.
  
  **Theory 1**
  
  **Axioms**
  
  **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))$
  
  **Definitions**
  
  **Overlap** : $\forall x,y \colon (overlap(x,y) \iff(\exists z \colon (part(z,x) \land part(z,y)))$
  
  **Proper Part** : $\forall x,y \colon (proprPart(x,y) \iff (part(x,y) \land \neg part(y,x)))$
  
  I am using [CafeOBJ](https://cafeobj.org/) to represent the above logical axioms and definitions, shown in **Listing 1**:
  
  **Listing 1**
  
  ```
     mod M{
      [E]
      preds overlap part properPart : E E
   -- axioms
   ax [M1] : \A[x:E] part(x,x) .  
   ax [M2] : \A[x:E]\A[y:E] ((part(x,y) & part(y,x)) -> (x = y))  .
   ax [M3] : \A[x:E]\A[y:E]\A[z:E]((part(x,y) & part(y,z))  -> part(x,z)) .
   -- definitions
   ax [DM1] : \A[x:E]\A[y:E] (properPart(x,y) <-> (part(x,y) & ~(part(y,x)))) .  
   ax [DM2] : \A[x:E]\A[y:E] (overlap(x,y) <->  (\E[z:E] (part(z,x) & part(z,y)))) .  
      }
  
  ```
  
  Note that the logical theory is contained in a *named module* called `M`. The variables are over a domain of generic entities `E`, universal and existential quantification are denoted by `\A[x:E]` and `\A[x:E]` respectively. In CafeOBJ, named modules allow one to structure signatures, theories, sub/super theories, and models using the [Theory of Institutions](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.74.5613&rep=rep1&type=pdf) ([TOI](https://cseweb.ucsd.edu/%7Egoguen/pps/iccs05.pdf)).
  
  Below is my naïve attempt to present the axioms as a set of [conceptual graphs](https://en.wikipedia.org/wiki/Conceptual_graph) (CG). My motivation for using [CGs](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.460.8912&rep=rep1&type=pdf) is that they provide an intuitive visualization of logic and have a direct relation to [Common Logic](http://www.jfsowa.com/talks/clintro.pdf) [(ISO zipped PDF)](https://standards.iso.org/ittf/PubliclyAvailableStandards/c066249_ISO_IEC_24707_2018.zip).
  
  [![enter image description here](https://i.sstatic.net/KOZaE.png)](https://i.sstatic.net/KOZaE.png)
  
  The above CG was produced using [CharGer](https://www.cs.nmsu.edu/%7Ehdp/CGTools/proceedings/tools/1999Compliant/CharGer.zip) software as Java zip file ([manual](https://www.cs.nmsu.edu/%7Ehdp/CGTools/proceedings/papers/CharGer.pdf)).
  
  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 three graphs are all related by conjunction, which is default for GC.
  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 CG asserts a single proposition, labelled **Proposition**.
  
  **Question:**
  
  How do I present **Theory 1** using CGs? Do I need some labeling that indicates that a set of concepts represent a theory. Or are theories represented by some enclosing *special* type of concept?
  
  **Tags:** logic, knowledge-representation, ontology
  
  > **Comments:**
  > **username_1**: DOL project may be helpful https://www.omg.org/spec/DOL. see for ex. [![Annex I](https://i.sstatic.net/yYs5n.png)](https://i.sstatic.net/yYs5n.png)  
  > **username_0**: @username_1 Thanks the link is useful, but I am more interested in FOL <-> CG mappings and model/theory representation using CGs.  
  > **username_2**: It seems that this post starts to become more complex. If you have multiple questions (even if they are related), I would recommend that you split them into multiple posts.  
  > **username_0**: @username_2 I have tried to simplify the question.  
  
  ---
  
  ## 0 answers
  
  