From b549ca03f81491621e67c8bd5a8b8983897f505b Mon Sep 17 00:00:00 2001
From: Michael Kohlhase <m.kohlhase@jacobs-university.de>
Date: Sat, 1 Jul 2017 13:01:54 +0200
Subject: [PATCH] links and content
---
projects/meta/completed.md | 2 +-
projects/meta/index.md | 2 +-
research/formal-methods.md | 15 +++++++++++----
research/index.md | 14 +++++++-------
research/structural-semantics.md | 7 ++++---
5 files changed, 24 insertions(+), 16 deletions(-)
diff --git a/projects/meta/completed.md b/projects/meta/completed.md
index ff88309..9ec6dab 100644
--- a/projects/meta/completed.md
+++ b/projects/meta/completed.md
@@ -24,6 +24,6 @@ We also organize some of our research and development into Projects,
</ul>
#### System Projects
-Completed projects that focused on building particular systems can be found under [KWARC Systems](../../systems/historic/).
+Completed projects that focused on building particular systems can be found under [KWARC Systems](/systems/historic/).
diff --git a/projects/meta/index.md b/projects/meta/index.md
index cea1d32..339b5cb 100644
--- a/projects/meta/index.md
+++ b/projects/meta/index.md
@@ -30,4 +30,4 @@ external researchers:
</ul>
#### System Projects
-Internal projects that are focused on building particular systems can be found under [KWARC Systems](../../systems/).
+Internal projects that are focused on building particular systems can be found under [KWARC Systems](/systems/).
diff --git a/research/formal-methods.md b/research/formal-methods.md
index 855a46c..e95b8f2 100644
--- a/research/formal-methods.md
+++ b/research/formal-methods.md
@@ -4,12 +4,19 @@ title: Formal Methods
menu_title: Formal Methods
menu_order: 102
---
-## Formal Methods
-
-This term usually identifies a set of technologies that presuppose representing the objects involved in some kind of logic with a well-defined semantics. The term formal refers to the fact that any action on the objects can be based on their form only. This usually means that the representations are quite elaborate and can be tedious to work with for humans, but also that these actions can be performed by machines.
+This term usually identifies a set of technologies that presuppose representing the objects involved in some kind of logic with a well-defined semantics. The term ``formal`` refers to the fact that any action on the objects can be based on their form only. This usually means that the representations are quite elaborate and can be tedious to work with for humans, but also that these actions can be performed by machines.
Therefore formal methods are highly successful in applications where a high degree of confidence is desired, e.g. in program verification, as the foundation of mathematics, or even in legal frameworks. To accommodate for these applications a large zoo of logics has been developed and mechanized reasoning systems have been developed.
-## In a little more detail
+### Entailment Systems
The foundation of formal methods is the entailment relation ⊧, a relation between a set Φ of formulae (the assumptions) and a formula T : Φ ⊧ T signifies that T must be true in all situations, where the assumptions in Φ are. So, if Φ is empty, T must be true in all situations, and we call it a theorem. The relation ⊧ is usually defined by reference to some externally given semantics, but can be approximated by a calculus. This gives the notion of a proof: we know Φ ⊧ T , if there is a proof of T from Φ that conforms to the rules of the calculus. So Φ ⊧ T can be verified by purely syntactical means, giving us a way to establish theorem-hood by a machine.
+
+### Logical Systems
+
+Entailment systems usually induced by logics, i.e. formal languages for representing knowledge with a model and/or proof theory. The KWARC group develops meta-logical approaches for modeling logics and the relations between them. For instance, we have developed the [LATIN Logic Atlas](/projects/latin/); a graph of more than 1000 logic fragments and logic-translations.
+
+### Interoperability in Formal Methods
+
+There are literally hundreds of formal systems for representing, reasoning about, and computing with STEM knowledge.
+
diff --git a/research/index.md b/research/index.md
index 27b521c..4f06255 100644
--- a/research/index.md
+++ b/research/index.md
@@ -18,8 +18,8 @@ menu_order: 101
<span style="font-weight:bold">Applications</span>
eMath 3.0,
<a href="https://mathhub.info">Active Documents</a>,
- <a href="../projects/SiSsI/">Semantic Spreadsheets</a>,
- <a href="../projects/FormalCAD/">Semantic CAD/CAM</a>,
+ <a href="/projects/SiSsI/">Semantic Spreadsheets</a>,
+ <a href="/projects/FormalCAD/">Semantic CAD/CAM</a>,
Semantic Help Systems, Change Mangagement, ...
</td>
</tr>
@@ -29,9 +29,9 @@ menu_order: 101
<ul>
<li><a href="https://omdoc.org">OMDoc</a></li>
<li><a href="http://uniformal.github.io">MMT: Modular Math Theories</a></li>
- <li><a href="../projects/latin">Logic Morphisms/Atlas</a></li>
+ <li><a href="/projects/latin">Logic Morphisms/Atlas</a></li>
<li>advanced Type Theories</li>
- <li><a href="../projects/oaf/">Theorem Prover</a> and <a href="../projects/odk/">Computer Algebra</a> Interoperability</li>
+ <li><a href="/projects/oaf/">Theorem Prover</a> and <a href="../projects/odk/">Computer Algebra</a> Interoperability</li>
</ul>
</td>
<td>
@@ -49,12 +49,12 @@ menu_order: 101
<span style="font-weight:bold">Semantization</span>
</a>
<ul>
- <li><a href="../systems/arXMLiv/">LaTeX --> XML</a></li>
- <li><a href="../systems/sTeX/">sTeX: Semantic LaTeX</a></li>
+ <li><a href="/systems/arXMLiv/">LaTeX --> XML</a></li>
+ <li><a href="/systems/sTeX/">sTeX: Semantic LaTeX</a></li>
<li>invasive editors</li>
<li>Context-Aware IDEs</li>
<li>Mathematical Corpora</li>
- <li><a href="../systems/llamapun/">Linguistics of Math</a></li>
+ <li><a href="/systems/llamapun/">Linguistics of Math</a></li>
</ul>
</td>
</tr>
diff --git a/research/structural-semantics.md b/research/structural-semantics.md
index 7720fef..b2f3f66 100644
--- a/research/structural-semantics.md
+++ b/research/structural-semantics.md
@@ -4,9 +4,10 @@ title: Structural Semantics
menu_order: 103
---
-Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with formal methods.
-In many cases, useful services can be rendered by machines without having an entailment relation, for instance we can search for a formula, we can determine the concepts it depends upon, etc.
+Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with [formal methods](formal-methods/).
+In many cases, useful [mathematical services](kminteract/) can be rendered by machines without having an [entailment relation](formal-methos/), for instance we can search for a formula, we can determine the concepts it depends upon, etc.
The commonality of such services is that they are based on the structure of the formulae alone.
For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof.
+We speak of *structural semantics* as a lightweight form of meaning annotation.
-...more to be written ...
+So instead of formalizing mathematical knowledge to a level where an entailment relation can be induced, we can use structural descriptions instead, e.g. by annotating certain properties to mathematical documents turning them into [objects of flexible formality](https://mathhub.info/help/FlexiForms.html).
--
GitLab