Reasoning Support for CASL with Automated Theorem Proving Systems
WADT 2006, 4409, page 74-91. Springer-Verlag Heidelberg, (2007)Abstract
We connect the algebraic specification language CASL with a variety
of automated first-order provers. The heart of this connection is an
institution comorphism from CASL to SoftFOL (softly typed
first-order logic); the latter is then translated to the provers'
input syntaxes. We also describe a GUI integrating the translations
and the provers into the Heterogeneous Tool Set. We report on
experiences with provers, which led to fine-tuning of the
translations. This framework can also be used for checking
consistency of specifications.