"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

Cornell University

Dean CIS