The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics

摘要

We are interested in developing a methodology for integrating mechanized reasoning sys- tems such as Theorem Provers, Computer Algebra Systems. And Model Checkers. Our approach is to provide a framework for integrating mechanized reasoning systems and to use specifications as a starting point for integration. We build on the work presented by Giunchiglia et al. (1994) which introduces the notion of Open Mechanized Reason- ing Systems (OMRS) as a specification framework for integrating reasoning systems.