Abstraction-based information technology: A framework for open mechanized reasoning

Abstract

OMRS (Open Mechanized Reasoning Systems) was designed for Automated Theorem Proving and then extended to Computer Algebra. These are the two domains at the heart of the Calculemus approach. An obvious question is to assess whether such an approach can be extended to new domains either within AI or outside of AI. There have been several attempts to turn the world into a computational system. This talk stays away from such general attempts and introduces a framework that is fully set within AI. It extends the basic concepts of OMRS to diverse fields ranging from information technology to sociology through law as illustrated by examples. The main motivation is to claim that whatever the selected approach, Artificial Intelligence is gaining enough strength and power to reach new frontiers and to turn challenges that are not a priori of a purely computational nature into AI domains. © 2009 Springer-Verlag Berlin Heidelberg.