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 firstorder 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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Lüttich, K., & Mossakowski, T. (2007). Reasoning support for CASL with automated theorem proving systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4409 LNCS, pp. 74–91). Springer Verlag. https://doi.org/10.1007/978-3-540-71998-4_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
