Publikation
Reasoning Support for CASL with Automated Theorem Proving Systems
Klaus Lüttich; Till Mossakowski
In: J. Fiadeiro (Hrsg.). WADT 2006. International Workshop on Algebraic Development Techniques (WADT-06), 18th, June 1-3, La Roche en Ardenne, Belgium, Pages 74-91, Vol. 4409, Springer-Verlag, Heidelberg, 2007.
Zusammenfassung
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.