%0 Conference Paper %1 LuettichEA06a %A Lüttich, Klaus %A Mossakowski, Till %B WADT 2006 %D 2007 %E Fiadeiro, J. %I Springer-Verlag Heidelberg %K CASL FOL MathServe SPASS SoftFOL Vampire automatic prover %P 74-91 %T Reasoning Support for CASL with Automated Theorem Proving Systems %V 4409 %X 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.

@inproceedings{LuettichEA06a, 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. }, added-at = {2016-08-05T15:59:03.000+0200}, author = {L{\"u}ttich, Klaus and Mossakowski, Till}, biburl = {https://www.bibsonomy.org/bibtex/2744c7e37e27241f3f180823b776bcf11/tillmo}, booktitle = {WADT 2006}, editor = {Fiadeiro, J.}, interhash = {f1cd4e92ed77680c4a09176ee8e946f2}, intrahash = {744c7e37e27241f3f180823b776bcf11}, keywords = {CASL FOL MathServe SPASS SoftFOL Vampire automatic prover}, pages = {74-91}, pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/casl2spass.pdf}, psurl = {http://www.informatik.uni-bremen.de/~till/papers/casl2spass.ps}, publisher = {Springer-Verlag Heidelberg}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems}, volume = 4409, year = 2007 }