Technology Profile: F-Life

Developers: Marco Schorlemmer, Dave Robertson

Owner: The University of Edinburgh

Addresses KM Challenge(s): Knowledge Life Cycle

Builds on other technologies: SICStus Prolog

What's the Problem?

The knowledge engineering world provides a rich source of software components for transforming formally expressed knowledge on a large scale, such as induction systems, knowledge base refiners and ontology merging tools. Formal methods have traditionally been concentrated on the integrity of design of individual systems, but with the advent of the Semantic Web there is interest in making them openly accessible on the Internet, with the ultimate goal in mind that a knowledge engineer should be able, with a small amount of intellectual effort, to locate and assemble sequences of these components to perform complex transformations on large repositories of knowledge.

The sorts of transformations used in knowledge engineering are not always trustworthy: some may not preserve the semantics of the knowledge transformed; some may not be able to perform a given transformation reliably under all circumstances. Therefore, it is crucial to have ways of inspecting the key properties we expect to be preserved by each transformational component and of describing how these properties change as new transformations are applied. This raises a new need for formality, to describe how such distributed systems transform knowledge. The aim of formality in this area is twofold: to give a concise account of what is going, and to use this account for practical purposes in maintaining and analysing knowledge-management life cycles.

Towards a Solution

F-Life is a prototype tool comprising a life-cycle editor, alife-cycle interpreter and a property checker. Its architecture is based on a formal life-cycle claculus, whose semantics is expressed in terms of abstract knowledge transformations using techniques from abstract model theory and semantic information flow:


Life-Cycle Editor:

With the editor a knowledge engineer analyses and represents life-cycle patterns, which are formal
representations of sequences of abstract knowledge transformations.



In their attempte to create these patterns, knowledge engineers are highly constrained by the editor according to transformation steps grounded on a formal life-cycle calculus:


Life-Cycle Interpreter:

Life-cycles patterns are passed to the interpreter, which is capable of executing its formal representation.  To run a life cycle in a particular domain, specific solvers capable of performing abstract life-cycle steps are needed, because life cycles are described only at a generic level. F-Life supports two possible realisation for a life-cycle execution:

Property Checker:

A life-cycle execution terminates, yielding as a response a term that captures the life-cycle hisotry in terms of the semantically-rich life-cycle calculus. This life-cycle history is used by the property checker to prove arguments about properties of knowledge components by looking at their evolutionary paths rather than by inspecting the specification of the components themselves.



Example Applications

Ecolingua's life cycle

Further Reading

Key document:
Formal Knowledge Management in Distributed Environments