资 源 简 介
Takes proof obligations generated in development and models built with the RODIN platform and translates them in SMT-LIB format.
The rationale is not to find a universal translation system, but instead try to provide and implement a translation system for different sub-logics so that SMT-LIB provers can be used more effectively and efficiently.