|"The world is engaged in a grand scientific and technological enterprise to build a global information resource. Creating this global resource will be one of the great achievements of information technology. Our research
on applied logic, formal methods and automated reasoning will make the emerging
information resource more capable -- first by providing a basis for semantic
processing of information and for a logical accounting of its structure, and
second by including among the resources an interactive digital library of
formal computational mathematics. Such a library will bring into being a formal forum that will connect experts and practitioners together in building reliable software systems, educating the information technology work force, empowering the lay scientist, and in nucleating the creation of a broader open library of formally grounded knowledge."
Prof. Robert Constable, Project PI