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.
%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
}