diff --git a/.gitignore b/.gitignore
index 372b93d..4706036 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 .vscode/
 _build/
+venv/
diff --git a/conf.py b/conf.py
index 612d387..f8e4ffc 100644
--- a/conf.py
+++ b/conf.py
@@ -30,7 +30,7 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = ['breathe', 'sphinx.ext.graphviz', 'sphinxcontrib.plantuml', 'sphinx.ext.extlinks']
+extensions = ['breathe', 'sphinx.ext.graphviz', 'sphinxcontrib.plantuml', 'sphinx.ext.extlinks', 'sphinx.ext.autosummary', 'sphinx.ext.autodoc']
 
 graphviz_output_format='png'
 graphviz_dot_args=[
@@ -75,12 +75,12 @@
 #
 # This is also used if you do content translation via gettext catalogs.
 # Usually you set "language" from the command line for these cases.
-language = None
+language = "en"
 
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.
 # This patterns also effect to html_static_path and html_extra_path
-exclude_patterns = ['_build','_themes','scripts' ]
+exclude_patterns = ['_build','_themes','scripts', 'venv' ]
 
 # The name of the Pygments (syntax highlighting) style to use.
 pygments_style = 'sphinx'
diff --git a/index.rst b/index.rst
index 2c047a6..6129694 100644
--- a/index.rst
+++ b/index.rst
@@ -21,6 +21,7 @@ CoreSense Project (CoreSense in short) is a project... TBD
    opensourecommunity/index.rst
    build_instructions/index.rst
    design/index.rst
+   understanding-logic/index.rst
    tutorials/index.rst
    testbeds/index.rst
    demos/index.rst
diff --git a/understanding-logic/concepts/agent.rst b/understanding-logic/concepts/agent.rst
new file mode 100644
index 0000000..abf0621
--- /dev/null
+++ b/understanding-logic/concepts/agent.rst
@@ -0,0 +1,13 @@
+Types
+=====
+
+.. _agent:
+
+**agent** ``$tType``
+--------------------
+
+A **CoreSense** agent which may posess `engines <engine.html>`_ and `modelets <modelet.html>`_.
+
+.. warning:: “Unimplemented” To be introduced later, as collective awareness is considered.
+
+Source: ``fundamental-concepts.tff``
diff --git a/understanding-logic/concepts/concept.rst b/understanding-logic/concepts/concept.rst
new file mode 100644
index 0000000..f62dc6c
--- /dev/null
+++ b/understanding-logic/concepts/concept.rst
@@ -0,0 +1,19 @@
+Types
+=====
+
+.. _concept:
+
+**concept** ``$tType``
+----------------------
+
+An instance of a class of `phenomenon <phenomenon.html>`_ in the agent’s world model.
+
+A `concept <#concept>`_ is a `property <property.html>`_ of a `modelet <modelet.html>`_.
+
+.. example::
+   - chair 
+   - dog
+   - the color pink
+   - sunrise
+
+Source: ``fundamental-concepts.tff``
diff --git a/understanding-logic/concepts/datatype.rst b/understanding-logic/concepts/datatype.rst
new file mode 100644
index 0000000..921f298
--- /dev/null
+++ b/understanding-logic/concepts/datatype.rst
@@ -0,0 +1,216 @@
+Types
+=====
+
+.. _datatype:
+
+**datatype** ``$tType``
+-----------------------
+
+A precise information encoding that is taken as granted. As the name suggests, the fundamental types of data considered.
+
+.. example:: 
+   - real number
+   - uint8
+   - pixel
+
+Source: ``fundamental-concepts.tff``
+
+ROS 2 Interface builtins
+========================
+
+ROS 2 interfaces (messages, services, and actions) are `formalisms <formalism.html>`_ constructed from semantically named builtin `datatypes <#datatype>`_ and arrays of these builtins. See the ROS 2 `documentation <https://docs.ros.org/en/rolling/Concepts/Basic/About-Interfaces.html>`_
+for more details.
+
+.. important:: 
+   These individuals are not associated with a particular semantic label. The intention (WIP) is to match a particular `datatype <#datatype>`_ (the ``fieldtype``) and a `concept <concept.html>`_ (the ``fieldname``) in some `formalism <formalism.html>`_ representing the ROS 2 interface.
+
+.. _ros2-msg-bool:
+
+**‘ROS2.msg.Bool’** `datatype <#datatype>`_
+------------------------------------------------
+
+The builtin ``bool`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-byte:
+
+**‘ROS2.msg.Byte’** `datatype <#datatype>`_
+------------------------------------------------
+
+The builtin ``byte`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-char:
+
+**‘ROS2.msg.Char’** `datatype <#datatype>`_
+------------------------------------------------
+
+The builtin ``char`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-float32:
+
+**‘ROS2.msg.Float32’** `datatype <#datatype>`_
+---------------------------------------------------
+
+The builtin ``float32`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-float64:
+
+**‘ROS2.msg.Float64’** `datatype <#datatype>`_
+---------------------------------------------------
+
+The builtin ``float64`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-int8:
+
+**‘ROS2.msg.Int8’** `datatype <#datatype>`_
+------------------------------------------------
+
+The builtin ``int8`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-uint8:
+
+**‘ROS2.msg.Uint8’** `datatype <#datatype>`_
+-------------------------------------------------
+
+The builtin ``uint8`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-int16:
+
+**‘ROS2.msg.Int16’** `datatype <#datatype>`_
+-------------------------------------------------
+
+The builtin ``int16`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-uint16:
+
+**‘ROS2.msg.Uint16’** `datatype <#datatype>`_
+--------------------------------------------------
+
+The builtin ``uin16`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-int32:
+
+**‘ROS2.msg.Int32’** `datatype <#datatype>`_
+-------------------------------------------------
+
+The builtin ``int32`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-uint32:
+
+**‘ROS2.msg.Uint32’** `datatype <#datatype>`_
+--------------------------------------------------
+
+The builtin ``uint32`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-int64:
+
+**‘ROS2.msg.Int64’** `datatype <#datatype>`_
+-------------------------------------------------
+
+The builtin ``int64`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-uint64:
+
+**‘ROS2.msg.Uint64’** `datatype <#datatype>`_
+--------------------------------------------------
+
+The builtin ``uint64`` field type of a ROS 2 interface.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-string:
+
+**‘ROS2.msg.String’** `datatype <#datatype>`_
+--------------------------------------------------
+
+The builtin (unbounded) ``string`` field type of a ROS 2 interface. These strings use 8-bit characters.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-wstring:
+
+**‘ROS2.msg.Wstring’** `datatype <#datatype>`_
+---------------------------------------------------
+
+The builtin ``wstring`` field type of a ROS 2 interface. These strings use 16-bit characters.
+
+Source: ``datatypes.tff``
+
+ROS 2 Interface arrays
+======================
+
+ROS 2 interfaces support arrays of builtins, optionally with a fixed or bounded size.
+
+.. warning::
+   Sizes of array datatypes are assumed to be natural numbers. This is **NOT** enforced by the type checker or logic.
+
+.. _ros2-msg-bounded-string:
+
+**‘ROS2.msg.BoundedString’** ( **$int** > `datatype <#datatype>`_ )
+-------------------------------------------------------------------
+
+A bounded ``string<=n`` field type of a ROS 2 interface. ``n`` is a natural number.
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-unbounded-dynamic-array:
+
+**‘ROS2.msg.UnboundedDynamicArray’** ( `datatype <#datatype>`_ > `datatype <#datatype>`_ )
+------------------------------------------------------------------------------------------
+
+An array of any builtin with an unbouned size field type in a ROS 2 interface. 
+
+.. example:: 
+   - ``char[]``
+   - ``float32[]``
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-bounded-dynamic-array:
+
+**‘ROS2.msg.BoundedDynamicArray’** (( `datatype <#datatype>`_ * **$int** ) > `datatype <#datatype>`_ )
+------------------------------------------------------------------------------------------------------
+
+A dynamic array of any builtin with a bounded size field type in a ROS 2 interface. The size must be a natural number.
+
+.. example::
+   -``char[<=5]``
+   - ``float32[<=4]``
+
+Source: ``datatypes.tff``
+
+.. _ros2-msg-static-array:
+
+**‘ROS2.msg.StaticArray’** (( `datatype <#datatype>`_ * **$int** ) > `datatype <#datatype>`_ )
+----------------------------------------------------------------------------------------------
+
+A static array of any builtin with a fixed size field type in a ROS 2 interface. The size must be a natural number.
+
+.. example::
+   - ``char[5]``
+   - ``float32[4]``
+
+Source: ``datatypes.tff``
diff --git a/understanding-logic/concepts/engine.rst b/understanding-logic/concepts/engine.rst
new file mode 100644
index 0000000..264ceea
--- /dev/null
+++ b/understanding-logic/concepts/engine.rst
@@ -0,0 +1,94 @@
+Types
+=====
+
+
+
+**engine** ``$tType``
+---------------------
+
+Does work within a **CoreSense** `agent <agent.html>`_ to produce `modelets <modelet.html>`_.
+
+-  Takes multiple `modelets <modelet.html>`_ as an input `modelet_set <modelet.rst#modelet_set>`_
+-  Uses semantic information to identify valid input modelet `formalisms <formalism.html>`_
+
+   -  semantics could be external (part of the type definition) or internal (modeled within the `modelet <modelet.html>`_ itself)
+-  Produces one output `modelet <modelet.html>`_
+
+   -  May or may not impart semantic meaning to the output `modelet <modelet.html>`_
+   -  May (re)define the output modelet `origin <origin.html>`_, `concept <concept.html>`_, or characteristics
+-  Has `exertion <exertion.html>`_ characteristics
+
+   -  e.g. time delay, resource usage, power consumption
+
+.. admonition:: Example
+
+   - DroneStateEngine (see tff/tests/test-wind-estimation.tff)
+
+      - Input Model: 
+ 
+         - Modelet
+
+            - formalism: IMU.msg 
+            - modelled concept: inertia 
+
+         - Modelet:
+         
+            - formalism: NavSatFix.msg
+            - modelled concept: geolocation
+     
+      - Output Modelet:
+       
+         - modelet:
+            
+            - formalism: DroneState.msg
+            - modelled concept: drone_state
+
+Source: ``engines-and-modelets.tff``
+
+Relations
+=========
+
+.. _interface_of:
+
+**interface_of** ( `engine <#engine>`_ > `template_set <template.rst#template_set>`_ )
+--------------------------------------------------------------------------------------
+
+An `engine <#engine>`_ requires a set of input `modelets <modelet.html>`_ which matches the `template_set <template.rst#template_set>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _output_modelet_formalism:
+
+**output_modelet_formalism** ( `engine <#engine>`_ > `formalism <formalism.html>`_ )
+------------------------------------------------------------------------------------
+
+The `formalism <formalism.html>`_ of an `engine <#engine>`_ output `modelet <modelet.html>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _is_output_modelet_concept:
+
+**is_output_modelet_concept** ( `engine <#engine>`_ > `phenomenon <phenomenon.html>`_ )
+---------------------------------------------------------------------------------------
+
+The `concept <concept.html>`_ of an `engine <#engine>`_ output `modelet <modelet.html>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _output_property_of_e:
+
+**output_property_of_engine** ( `engine <#engine>`_ > `property <property.html>`_ )
+-----------------------------------------------------------------------------------
+
+The `property <property.html>`_ an `engine <#engine>`_ imparts on its output `modelet <modelet.html>`_.
+
+Source: ``properties.tff``
+
+.. _engine_imparts_representation_class:
+
+**engine_imparts_representation_class** ( `engine <#engine>`_ > `representation_class <representation_class.html>`_ )
+---------------------------------------------------------------------------------------------------------------------
+
+The `representation_class <representation_class.html>`_ an `engine <#engine>`_ imparts on its output `modelet <modelet.html>`_.
+
+Source: ``engines-and-modelets.tff``
diff --git a/understanding-logic/concepts/exertion.rst b/understanding-logic/concepts/exertion.rst
new file mode 100644
index 0000000..52e5927
--- /dev/null
+++ b/understanding-logic/concepts/exertion.rst
@@ -0,0 +1,70 @@
+
+
+
+
+
+
+Relations
+=========
+
+.. _inputs_match:
+
+**inputs_match** (( `modelet <modelet.html>`_ * `template <template.html>`_ ) > **$o** )
+----------------------------------------------------------------------------------------
+
+Check if a `modelet <modelet.html>`_ matches a `template <template.html>`_.
+
+-  Check if they are `formally equivalent <#formally_equivalent>`_
+-  Check if the `modelet <modelet.html>`_ contains *permissible* values
+   for each of the `properties <property.html>`_ of `requirements <requirement.html>`_ of the `template <template.html>`_.
+
+Source: ``engines-and-modelets.tff``, ``properties.tff``
+
+.. _formally_equivalent:
+
+**formally_equivalent** (( `template <template.html>`_ * `modelet <modelet.html>`_ ) > **$o** )
+-----------------------------------------------------------------------------------------------
+
+A `template <template.html>`_ and a `modelet <modelet.html>`_ share the same *phenomenon* and `formalism <formalism.html>`_.
+
+Source: ``properties.tff``
+
+.. _interfaces_match:
+
+**interfaces_match** (( `modelet_set <modelet.rst#modelet_set>`_ * `template_set <template.rst#template_set>`_ ) > **$o** )
+---------------------------------------------------------------------------------------------------------------------------
+
+Check if all of the `templates <template.html>`_ in the `template_set <template.rst#template_set>`_ have a corresponding `modelet <modelet.html>`_ in the `modelet_set <modelet.rst#modelet_set>`_ with matching profile.
+
+-  Check if they are `formally equivalent <#formally_equivalent>`_
+-  Check if their `inputs match <#inputs_match>`_
+
+Source: ``engines-and-modelets.tff``, ``properties.tff``
+
+.. _exert:
+
+**exert** (( `engine <engine.html>`_ * `modelet_set <modelet.rst#modelet_set>`_ * `modelet <modelet.html>`_ ) > **$o** )
+------------------------------------------------------------------------------------------------------------------------
+
+Exert an `engine <engine.html>`_ on a `modelet_set <modelet.rst#modelet_set>`_ to produce an output `modelet <modelet.html>`_. 
+
+Source: ``engines-and-modelets.tff``
+
+.. _exertable:
+
+**exertable** (( `modelet_set <modelet.rst#modelet_set>`_ * `engine <engine.html>`_ ) > **$o** )
+------------------------------------------------------------------------------------------------
+
+A `modelet_set <modelet.rst#modelet_set>`_ can be exerted by an `engine <engine.html>`_ iff their `interfaces match <#interfaces_match>`_. 
+
+Source: ``engines-and-modelets.tff``
+
+.. _exertion:
+
+**exertion** (( `engine <engine.html>`_ * `modelet_set <modelet.rst#modelet_set>`_ * `modelet <modelet.rst#modelet>`_ * `modelet_set <modelet.rst#modelet_set>`_ ) >  `modelet_set <modelet.rst#modelet_set>`_ )
+----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+
+
+The act of exerting an `engine <engine.html>`_ on a `modelet_set <modelet.rst#modelet_set>`_, resulting in a `modelet <modelet.html>`_, in defined state of knowledge, resulting in the addition of the output modelet to that state of knowledge. 
+
+Source: ``understanding-calculus.tff``
diff --git a/understanding-logic/concepts/extent.rst b/understanding-logic/concepts/extent.rst
new file mode 100644
index 0000000..053e95f
--- /dev/null
+++ b/understanding-logic/concepts/extent.rst
@@ -0,0 +1,50 @@
+Types
+=====
+
+
+
+**extent** ``$tType``
+---------------------
+
+A 4-dimensional size (3 space, 1 time). .. note:: Not to be confused with a 4-dimentional `spacetime_point <spacetime_point.html>`_.
+
+Source: ``fundamental-concepts.tff``
+
+Relations
+=========
+
+.. _extent_width:
+
+**extent_width** ( `extent <#extent>`_ > **$real** )
+-----------------------------------------------------------------------------
+
+The width of an (`extent <#extent>`_).
+
+Source: ``fundamental-concepts.tff``
+
+.. _extent_height:
+
+**extent_height** ( `extent <#extent>`_ > **$real** )
+------------------------------------------------------------------------------
+
+The height of an (`extent <#extent>`_).
+
+Source: ``fundamental-concepts.tff``
+
+.. _extent_depth:
+
+**extent_depth** ( `extent <#extent>`_ > **$real** )
+-----------------------------------------------------------------------------
+
+The depth of an (`extent <#extent>`_).
+
+Source: ``fundamental-concepts.tff``
+
+.. _extent_duration:
+
+**extent_duration** ( `extent <#extent>`_ > **$real** )
+--------------------------------------------------------------------------------
+
+The duration of an (`extent <#extent>`_).
+
+Source: ``fundamental-concepts.tff``
diff --git a/understanding-logic/concepts/formalism.rst b/understanding-logic/concepts/formalism.rst
new file mode 100644
index 0000000..5c33dea
--- /dev/null
+++ b/understanding-logic/concepts/formalism.rst
@@ -0,0 +1,23 @@
+Types
+=====
+
+.. _formalism:
+
+**formalism** ``$tType``
+------------------------
+
+The language and structure in which a `phenomenon <phenomenon.html>`_ could be described. Methods used to express `modelets <modelet.html>`_; class in the *Data Model*.
+
+-  The information structure used to capture the `concept <concept.html>`_ and `origin <origin.html>`_
+-  Highlights some aspects of the *phenomenon* while hiding others
+-  Defines `engine <engine.html>`_ I/O compatibility and usability with other models
+
+New `formalism <#formalism>`_ could be defined or old ones modified.
+
+.. admonition:: Example
+
+   - ROS message
+   - Image format
+   - Language grammar
+
+Source: Understanding presentation
diff --git a/understanding-logic/concepts/index.rst b/understanding-logic/concepts/index.rst
new file mode 100644
index 0000000..741c996
--- /dev/null
+++ b/understanding-logic/concepts/index.rst
@@ -0,0 +1,165 @@
+Concepts
+========
+
+.. danger::
+
+   These concepts are still in development and highly susceptible to change. Use the provided terms, definitions, and types with caution.
+
+The **Understanding System** (a.k.a Understanding Core) is a CoreSense
+module for generating understanding within a *CoreSense* agent. The main
+idea is to: .. quote:: Intuition Find *strategies* of **Engine**
+*exertions* to **create** required **Modelets**.
+
+.. admonition:: TODO
+
+   Add a map of the concepts or something more elegant here… We should also include the triangle of meaning.
+
+Types
+-----
+
+`agent <agent.html>`_
+~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: agent.rst
+   :start-line: 8
+   :end-line: 9
+
+`datatype <datatype.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: datatype.rst
+   :start-line: 8
+   :end-line: 9
+
+`engine <engine.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: engine.rst
+   :start-line: 8
+   :end-line: 9
+
+`exertion <exertion.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: exertion.rst
+   :start-line: 67
+   :end-line: 68
+
+`extent <extent.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: extent.rst
+   :start-line: 8
+   :end-line: 9
+
+`formalism <formalism.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: formalism.rst
+   :start-line: 8
+   :end-line: 9
+
+`modelet <modelet.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: modelet.rst
+   :start-line: 8
+   :end-line: 9
+
+`modelet_set <modelet.html#modelet_set>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: modelet.rst
+   :start-line: 21
+   :end-line: 22
+
+`origin <origin.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: origin.rst
+   :start-line: 8
+   :end-line: 9
+
+`phenomenon <phenomenon.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: phenomenon.rst
+   :start-line: 8
+   :end-line: 9
+
+`property <property.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: property.rst
+   :start-line: 8
+   :end-line: 9
+
+`requirement <requirement.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: requirement.rst
+   :start-line: 8
+   :end-line: 9
+
+`representation_class <representation_class.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: representation_class.rst
+   :start-line: 8
+   :end-line: 9
+
+`spacetime_point <spacetime_point.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: spacetime_point.rst
+   :start-line: 8
+   :end-line: 9
+
+`strategy <strategy.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: strategy.rst
+   :start-line: 8
+   :end-line: 9
+
+`template <template.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: template.rst
+   :start-line: 8
+   :end-line: 9
+
+`template_set <template.html#template_set>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: template.rst
+   :start-line: 19
+   :end-line: 20
+
+`concept <concept.html>`_
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. include:: concept.rst
+   :start-line: 8
+   :end-line: 9
+
+
+.. toctree::
+   :hidden:
+
+   agent.rst
+   concept.rst
+   datatype.rst
+   engine.rst
+   exertion.rst
+   extent.rst
+   formalism.rst
+   modelet.rst
+   origin.rst
+   phenomenon.rst
+   property.rst
+   representation_class.rst
+   requirement.rst
+   spacetime_point.rst
+   strategy.rst
+   template.rst
diff --git a/understanding-logic/concepts/modelet.rst b/understanding-logic/concepts/modelet.rst
new file mode 100644
index 0000000..c43e931
--- /dev/null
+++ b/understanding-logic/concepts/modelet.rst
@@ -0,0 +1,114 @@
+Types
+=====
+
+
+
+**modelet** ``$tType``
+----------------------
+
+Models a `phenomenon <phenomenon.html>`_ as the *thought* in the triangle of meaning. All modelets describe an instance of a `concept <concept.html>`_, have an `origin <origin.html>`_, and are modeled in a specific `formalism <formalism.html>`_.
+
+-  `Concept <concept.html>`_: the *phenomenon* of the
+   `modelet <modelet.html>`_, an instance of a class in the world model.
+-  `Origin <origin.html>`_: the agent’s perspective on the *phenomenon*
+-  `Formalism <formalism.html>`_: the representation of the *phenomenon*
+
+Source: ``engines-and-modelets.tff``
+
+
+**modelet_set** ``$tType``
+--------------------------
+
+Some particular set of `modelets <modelet.html>`_ which the reasoner has assembled. Used to collect the inputs to an `engine <engine.html>`_. 
+
+.. admonition:: Example
+
+
+   - {m1, m2, m3} 
+   - {m2}
+   - {}
+
+Source: ``engines-and-modelets.tff``
+
+Relations
+=========
+
+.. _modelet_models_concept:
+
+**modelet_models_concept** ( `modelet <modelet.html>`_ > `phenomenon <phenomenon.html>`_ )
+--------------------------------------------------------------------------------------------------------------
+
+The `phenomenon <phenomenon.html>`_ symbolizing the *phenomenon* of a `modelet <modelet.html>`_. 
+
+Source: ``engines-and-modelets.tff``
+
+.. _formalism_of_modelet:
+
+**formalism_of_modelet** ( `modelet <modelet.html>`_ > `formalism <formalism.html>`_ )
+----------------------------------------------------------------------------------------------------------
+
+The `formalism <formalism.html>`_ used by a `modelet <modelet.html>`_ to describe the *phenomenon*.
+
+Source: ``engines-and-modelets.tff``
+
+.. _modelet_creation_date:
+
+**modelet_creation_date** ( `modelet <modelet.html>`_ > **$real** )
+----------------------------------------------------------------------------------------
+
+The date a `modelet <modelet.html>`_ was created.
+
+.. admonition:: TODO
+
+   The date is represented as a ``$real`` but we don’t make any assumptions about what that number represents. Unix time? time since last restart? seconds? This may be solved by integration with ``spacetime_point``.
+
+Source: ``engines-and-modelets.tff``
+
+.. _modelet_has_location:
+
+**modelet_has_location** ( `modelet <modelet.html>`_ > `spacetime_point <spacetime_point.html>`_ )
+----------------------------------------------------------------------------------------------------------------------
+
+The time and spatial location a `modelet <modelet.html>`_ refers to. `Modelets <modelet.html>`_ may have a specific temporal scope or make an observation at a specific `spacetime_point <spacetime_point.html>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _modelet_has_extent:
+
+**modelet_has_extent** ( `modelet <modelet.html>`_ > `extent <extent.html>`_ )
+--------------------------------------------------------------------------------------------------
+
+The time and spatial `extent <extent.html>`_ a `modelet <modelet.html>`_ refers to. `Modelets <modelet.html>`_ may have an area/volume/duration of reference.
+
+Source: ``engines-and-modelets.tff``
+
+.. _modelet_has_representation_class:
+
+**modelet_has_representation_class** ( `modelet <modelet.html>`_ > `representation_class <representation_class.html>`_ )
+--------------------------------------------------------------------------------------------------------------------------------------------
+
+The `representation_class <representation_class.html>`_ a `modelet <modelet.html>`_’s relation to its parents has after being created by an `engine <engine.html>`_. 
+
+.. hint::
+   
+   This looks like it will turn out to be HOL.
+
+Source: ``engines-and-modelets.tff``
+
+.. _modelet_has_creator:
+
+**modelet_has_creator** ( `modelet <modelet.html>`_ > `engine <engine.html>`_ )
+---------------------------------------------------------------------------------------------------
+
+The `engine <engine.html>`_ that created the `modelet <modelet.html>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _is_in_modelet_set:
+
+**is_in_modelet_set** (( `modelet <modelet.html>`_ * `modelet_set <modelet.html_set>`_ ) > **$o** )
+-------------------------------------------------------------------------------------------------------------------------------
+
+Check if a `modelet <modelet.html>`_ is a member of a `modelet_set <modelet.html_set>`_.
+
+Source: ``engines-and-modelets.tff``
diff --git a/understanding-logic/concepts/origin.rst b/understanding-logic/concepts/origin.rst
new file mode 100644
index 0000000..6fc8be1
--- /dev/null
+++ b/understanding-logic/concepts/origin.rst
@@ -0,0 +1,18 @@
+Types
+=====
+
+.. _origin:
+
+**origin** ``$tType``
+---------------------
+
+An agent’s perspective on the *phenomenon* captured in a particular `modelet <modelet.html>`_.
+
+-  Observation is *situated* in time and space
+-  Measured with sensors that have certain characteristics and limitations
+
+   -  (inferred) physical quality (e.g. distance inferred from delay)
+   -  resolution and frame rate
+   -  reflections and transparencies could be misinterpreted
+
+Source: Understanding presentation
diff --git a/understanding-logic/concepts/phenomenon.rst b/understanding-logic/concepts/phenomenon.rst
new file mode 100644
index 0000000..07391a9
--- /dev/null
+++ b/understanding-logic/concepts/phenomenon.rst
@@ -0,0 +1,22 @@
+Types
+=====
+
+.. _phenomenon:
+
+**phenomenon** ``$tType``
+-------------------------
+
+Some space or object or being or process in the real world that the system represents using `modelets <modelet.html>`_.
+
+-  *Situated* in time and space
+-  May change over time
+-  Associated with a mission-dependent *meaning*
+
+.. admonition:: Example
+
+   - you 
+   - your office
+   - your tea
+   - your tea approaching room temperature
+
+Source: ``fundamental-concepts.tff``
diff --git a/understanding-logic/concepts/property.rst b/understanding-logic/concepts/property.rst
new file mode 100644
index 0000000..4b94f62
--- /dev/null
+++ b/understanding-logic/concepts/property.rst
@@ -0,0 +1,55 @@
+Types
+=====
+
+
+
+**property** ``$tType``
+-----------------------
+
+A specific characteristic of a `modelet <modelet.html>`_ or `engine <engine.html>`_. Multiple things can exhibit the same `property <property.html>`_.
+
+.. admonition:: example
+
+   - color: red 
+   - age: 14 years
+
+Source: ``properties.tff``
+
+Relations
+=========
+
+.. _has_value:
+
+**has_value** ( `property <#property>`_ > **$real** )
+------------------------------------------------------------------------------
+
+The value of a certain `property <#property>`_.
+
+Source: ``properties.tff``
+
+.. _datatype_of_p:
+
+**datatype_of_property** ( `property <#property>`_ > `datatype <datatype.html>`_ )
+-----------------------------------------------------------------------------------------------------------
+
+The `datatype <datatype.html>`_ of a certain `property <#property>`_.
+
+Source: ``properties.tff``
+
+.. _is_property_of_m:
+
+**is_property_of_modelet** (( `property <#property>`_ * `modelet <modelet.html>`_ ) > **$o** )
+---------------------------------------------------------------------------------------------------------------------------------
+
+Check if a `modelet <modelet.html>`_ is described by a certain `property <#property>`_.
+
+Source: ``properties.tff``
+
+.. _is_property_of_e:
+
+**is_property_of_engine** (( `property <#property>`_ * `engine <engine.html>`_ ) > **$o** )
+------------------------------------------------------------------------------------------------------------------------------
+
+Check if an `engine <engine.html>`_ is described by a certain `property <#property>`_.
+
+Source: ``properties.tff``
diff --git a/understanding-logic/concepts/representation_class.rst b/understanding-logic/concepts/representation_class.rst
new file mode 100644
index 0000000..19dabc4
--- /dev/null
+++ b/understanding-logic/concepts/representation_class.rst
@@ -0,0 +1,11 @@
+Types
+=====
+
+.. _representation_class:
+
+**representation_class** ``$tType``
+-----------------------------------
+
+The relation a `modelet <modelet.html>`_ has with its parents, i.e. the inputs to the `engine <engine.html>`_ `exertion <exertion.html>`_. Class of their relation in the *Processing/Modelling Model*.
+
+Source: ``fundamental-concepts.tff``
diff --git a/understanding-logic/concepts/requirement.rst b/understanding-logic/concepts/requirement.rst
new file mode 100644
index 0000000..d187479
--- /dev/null
+++ b/understanding-logic/concepts/requirement.rst
@@ -0,0 +1,41 @@
+Types
+=====
+
+
+
+**requirement** ``$tType``
+--------------------------
+
+A restriction on the `property <property.html>`_ values that a `template <template.html>`_ may enforce on a `modelet <modelet.html>`_.
+
+Source: ``properties.tff``
+
+Relations
+=========
+
+.. _datatype_of_p:
+
+**datatype_of_requirement** ( `requirement <#requirement>`_ > `datatype <datatype.html>`_ )
+--------------------------------------------------------------------------------------------------------------------
+
+The `datatype <datatype.html>`_ of a certain `requirement <#requirement>`_.
+
+Source: ``properties.tff``
+
+.. _is_permissible:
+
+**is_permissible** (( `requirement <#requirement>`_ * **$real** ) > **$o** )
+---------------------------------------------------------------------------------------------------------------
+
+Check if a value is *permissible* under a certain `requirement <#requirement>`_.
+
+Source: ``properties.tff``
+
+.. _is_part_of:
+
+**is_part_of** (( `requirement <#requirement>`_ * `template <template.html>`_ ) > **$o** )
+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+
+Check if a `requirement <#requirement>`_ is part of a `template <template.html>`_.
+
+Source: ``properties.tff``
diff --git a/understanding-logic/concepts/spacetime_point.rst b/understanding-logic/concepts/spacetime_point.rst
new file mode 100644
index 0000000..0a2cb0b
--- /dev/null
+++ b/understanding-logic/concepts/spacetime_point.rst
@@ -0,0 +1,53 @@
+Types
+=====
+
+
+
+**spacetime_point** ``$tType``
+------------------------------
+
+4-dimensional coordinates (3 space, 1 time).
+
+.. note::
+   Not to be confused with a 4-dimentional `extent <extent.html>`_.
+
+Source: ``fundamental-concepts.tff``
+
+Relations
+=========
+
+.. _point_x:
+
+**point_x** ( `spacetime_point <#spacetime_point>`_ > **$real** )
+------------------------------------------------------------------------------------------
+
+The spatial ``x`` coordinate of a point in space and time (`spacetime_point <#spacetime_point>`_).
+
+Source: ``fundamental-concepts.tff``
+
+.. _point_y:
+
+**point_y** ( `spacetime_point <#spacetime_point>`_ > **$real** )
+------------------------------------------------------------------------------------------
+
+The spatial ``y`` coordinate of a point in space and time (`spacetime_point <#spacetime_point>`_).
+
+Source: ``fundamental-concepts.tff``
+
+.. _point_z:
+
+**point_z** ( `spacetime_point <#spacetime_point>`_ > **$real** )
+------------------------------------------------------------------------------------------
+
+The spatial ``z`` coordinate of a point in space and time (`spacetime_point <#spacetime_point>`_).
+
+Source: ``fundamental-concepts.tff``
+
+.. _point_t:
+
+**point_t** ( `spacetime_point <#spacetime_point>`_ > **$real** )
+------------------------------------------------------------------------------------------
+
+The time ``t`` coordinate of a point in space and time (`spacetime_point <#spacetime_point>`_).
+
+Source: ``fundamental-concepts.tff``
diff --git a/understanding-logic/concepts/strategy.rst b/understanding-logic/concepts/strategy.rst
new file mode 100644
index 0000000..092f0ea
--- /dev/null
+++ b/understanding-logic/concepts/strategy.rst
@@ -0,0 +1,15 @@
+Types
+=====
+
+.. _strategy:
+
+**strategy** (( `modelet_set <modelet.rst#modelet_set>`_ * `modelet <modelet.rst#modelet>`_ ) > **$o** )
+----------------------------------------------------------------------------------------------------------------------------------------
+
+A succession of `exertions <exertion.html>`_ of `engines <engine.html>`_ connects `modelets <modelet.html>`_. `Strategies <strategy.html>`_ are transitive.
+
+-  Must respect engine `requirements <requirement.html>`_
+-  Matches `modelet <modelet.html>`_ *phenomenon* semantics to physical reality
+   -  e.g. “on the living room table” to coordinates
+
+Source: ``transitive-strategies.tff``
diff --git a/understanding-logic/concepts/template.rst b/understanding-logic/concepts/template.rst
new file mode 100644
index 0000000..f8bb7a1
--- /dev/null
+++ b/understanding-logic/concepts/template.rst
@@ -0,0 +1,85 @@
+Types
+=====
+
+
+
+**template** ``$tType``
+-----------------------
+
+Describes the features that a single `modelet <modelet.html>`_ should have for an `engine <engine.html>`_ to accept it as input.
+
+-  a semantic function signature
+-  `properties <property.html>`_ and `requirements <requirement.html>`_ of `modelets <modelet.html>`_ 
+
+Source: ``engines-and-modelets.tff``
+
+
+**template_set** ``$tType``
+---------------------------
+
+Some particular set of `templates <template.html>`_ which describe the inputs to an `engine <engine.html>`_.
+
+.. admonition:: Example 
+
+   - {t1, t2, t3} 
+   - {t2} 
+   - {}
+
+Source: ``engines-and-modelets.tff``
+
+Relations
+=========
+
+.. _template_has_concept_requirement:
+
+**template_has_concept_requirement** ( `template <#template>`_ > `concept <concept.html>`_ )
+---------------------------------------------------------------------------------------------------------------------
+
+The `concept <concept.html>`_ symbolizing the *phenomenon class* of a `template <template.html>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _template_formalism_requirement:
+
+**template_formalism_requirement** ( `template <#template>`_ > `formalism <formalism.html>`_ )
+-----------------------------------------------------------------------------------------------------------------------
+
+The `formalism <formalism.html>`_ this `template <#template>`_ expects the *phenomenon* to be described by.
+
+Source: ``engines-and-templates.tff``
+
+.. _template_has_location_requirement:
+
+**template_has_location_requirement** ( `template <#template>`_ > `spacetime_point <spacetime_point.html>`_ )
+--------------------------------------------------------------------------------------------------------------------------------------
+
+The time and spatial location a `template <#template>`_ refers to. A `template <template.html>`_ may have a specific temporal scope or expect an observation at a specific `spacetime_point <spacetime_point.html>`_.
+
+Source: ``engines-and-modelets.tff``
+
+.. _template_has_extent_requirement:
+
+**template_has_extent_requirement** ( `template <#template>`_ > `extent <extent.html>`_ )
+------------------------------------------------------------------------------------------------------------------
+
+The time and spatial `extent <extent.html>`_ a `template <#template>`_ covers. A `template <#template>`_ may expect an area/volume/duration of reference.
+
+Source: ``engines-and-modelets.tff``
+
+.. _template_has_creator_requirement:
+
+**template_has_creator_requirement** ( `template <#template>`_ > `engine <engine.html>`_ )
+-------------------------------------------------------------------------------------------------------------------
+
+The `engine <engine.html>`_ a `template <#template>`_ requires a `modelet <modelet.html>`_ to have been created by.
+
+Source: ``engines-and-modelets.tff``
+
+.. _is_in_template_set:
+
+**is_in_template_set** (( `template <#template>`_ * `template_set <#template_set>`_ ) > **$o** )
+------------------------------------------------------------------------------------------------------------------------------------
+
+Check if a `template <#template>`_ is a member of a `template_set <#template_set>`_.
+
+Source: ``engines-and-modelets.tff``
diff --git a/understanding-logic/index.rst b/understanding-logic/index.rst
new file mode 100644
index 0000000..ab3f49c
--- /dev/null
+++ b/understanding-logic/index.rst
@@ -0,0 +1,13 @@
+.. _understanding-logic:
+
+Understanding Logic
+###################
+
+This work is hosted at `CoreSenseEU/understanding-logic <https://github.com/CoreSenseEU/understanding-logic>`_.
+
+.. toctree::
+   :maxdepth: 1
+
+   concepts/index.rst
+   packages/index.rst
+   usage/index.rst
diff --git a/understanding-logic/packages/index.rst b/understanding-logic/packages/index.rst
new file mode 100644
index 0000000..1c81451
--- /dev/null
+++ b/understanding-logic/packages/index.rst
@@ -0,0 +1,2 @@
+Understanding Packages
+======================
diff --git a/understanding-logic/usage/index.rst b/understanding-logic/usage/index.rst
new file mode 100644
index 0000000..1ea03f5
--- /dev/null
+++ b/understanding-logic/usage/index.rst
@@ -0,0 +1,13 @@
+Usage and Installation
+======================
+
+The ``TFF`` models and tests can be run using the `latest
+release <https://github.com/vprover/vampire/releases/tag/v4.9casc2024>`__
+or ``master`` branch of the
+`Vampire <https://github.com/vprover/vampire>`__ theorem prover.
+
+If you want to run the ``THF`` models, you need to either install the
+`LEO-III <https://github.com/leoprover/Leo-III>`__ theorem prover or
+build the Vampire ``hol`` branch from source using these
+`instructions <https://github.com/vprover/vampire/wiki/Source-Build-for-Users>`__.
+Make sure to add the ``-DCMAKE_BUILD_HOL=ON`` flag.