Newer
Older
---
layout: page
title: Formal Methods
menu_title: 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.
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.
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.
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.
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).