Skip to content
Snippets Groups Projects
formal-methods.md 1.53 KiB
Newer Older
Michael Kohlhase's avatar
Michael Kohlhase committed
---
layout: page
title: Formal Methods
menu_title: Formal Methods
Tom Wiesing's avatar
Tom Wiesing committed
menu_order: 102
Michael Kohlhase's avatar
Michael Kohlhase committed
---
## 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.

## In a little more detail

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.