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 Seiten 74-91 4409 Springer-Verlag Heidelberg 2007.


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.

Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence