Developers: Marco Schorlemmer, Dave Robertson
Owner: The University of Edinburgh
Addresses KM Challenge(s): Knowledge Life Cycle
Builds on other technologies: SICStus Prolog
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.
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:
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-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:
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.
Key document:
Formal Knowledge Management in Distributed Environments