@@ -8,15 +8,15 @@ This term usually identifies a set of technologies that presuppose representing
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.
### Entailment Systems
#### 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
#### 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
#### Interoperability in Formal Methods
There are literally hundreds of formal systems for representing, reasoning about, and computing with STEM knowledge.
There are literally hundreds of formal systems for representing, reasoning about, and computing with STEM knowledge. The KWARC group is developing a general, knowledge-based interoperability architecture: the Math-in-the-Middle (MitM) Approach to interoperability. We use modularly represented mathematical knowledge as a pivot point for connecting systems. In the [OpenDreamKit](/projects/odk) we instantiate this for computer algebra systems, and in the [OAF](/projects/oaf) for theorem prover (libraries).
