KWARC: From Formal Methods to Structural Semantics

The KWARC research group conducts research in knowledge representation with a view towards applications in knowledge management. We extend techniques from formal methods so that they can be used in settings where formalization is either infeasible or too costly. We concentrate on developing techniques for marking up the structural semantics in technical documents. This level of markup allows for offering interesting knowledge management services without forcing the author to formalize the document contents.

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 $\Phi$ of formulae (the assumptions) and a formula $T$: $\Phi \vDash T$ signifies that T must be true in all situations, where the assumptions in $\Phi$ are. So, if $\Phi$ is empty, T must be true in all situations, and we call it a theorem. The relation $\vDash$ 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 $\Phi \vDash T$, if there is a proof of $T$ from $\Phi$ that conforms to the rules of the calculus. So $\Phi \vDash T$ can be verified by purely syntactical means, giving us a way to establish theoremhood by a machine.

Structural Semantics

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 depents 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 theoremhood, we only insist that there be an object that has the structure of a proof. ...more to be written ...