This approach suggests a possible solution for the following issue : how to formalize environments related to a given process and how to exploit the information they provide in order to start appropriate actions ? For that purpose, we took an interest in the concepts of ontologies, contexts and actions. We have investigated the constructive type theory and extended it with extensional sub-typing (allowing for type hierarchies) and constants to result in what is called the Dependent Type Framework (DTF). DTF tries to combine a constructive logic with a functional programming language for the representation and reasoning about contexts and actions. It provides a high expressiveness, decidability of type checking and a powerful sub-typing mechanism. We show how to model both contexts with types in DTF from the given information about a problem and actions to start to solve it. Then, as a test of feasibility with the purpose of sensing the complexity of such a solution, a context prover has been built with a functional language. Finally, a test application called the wumpus world in which a software agent moves across a grid in an unknown environment is implemented.
