%0 Conference Paper %1 Mossakowski95b %A Mossakowski, T. %B Computer Science Logic. 9th Workshop, CSL'95. Paderborn, Germany, September 1995, Selected Papers %D 1996 %E Büning, H. Kleine %I Springer Verlag, London %K imported %P 403--433 %T Equivalences among various logical frameworks of partial algebras %U http://www.springerlink.com/(bt4qw245oavupgzdxw3zpuul)/app/home/contribution.asp?referrer=parent&backto=searchcitationsresults,1,38; %V 1092 %X We examine a variety of liberal logical frameworks of partial algebras. Therefore we use simple, conjunctive and weak embeddings of institutions which preserve model categories and may map sentences to sentences, finite sets of sentences, or theory extensions using unique-existential quantifiers, respectively. They faithfully represent theories, model categories, theory morphisms, colimit of theories, reducts etc. Moreover, along simple and conjunctive embeddings, theorem provers can be re-used in a way that soundness and completeness is preserved. Our main result states the equivalence of all the logical frameworks with respect to weak embeddability. This gives us compilers between all frameworks. Thus it is a chance to unify the different branches of specification using liberal partial logics. This is important for reaching the goal of formal interoperability of different specification languages for software development. With formal interoperability, a specification can contain parts written in different logical frameworks using a multiparadigm specification language, and one can re-use tools which are available for one framework also for other frameworks. %@ 3-540-61377-3

@inproceedings{Mossakowski95b, abstract = {We examine a variety of liberal logical frameworks of partial algebras. Therefore we use simple, conjunctive and weak embeddings of institutions which preserve model categories and may map sentences to sentences, finite sets of sentences, or theory extensions using unique-existential quantifiers, respectively. They faithfully represent theories, model categories, theory morphisms, colimit of theories, reducts etc. Moreover, along simple and conjunctive embeddings, theorem provers can be re-used in a way that soundness and completeness is preserved. Our main result states the equivalence of all the logical frameworks with respect to weak embeddability. This gives us compilers between all frameworks. Thus it is a chance to unify the different branches of specification using liberal partial logics. This is important for reaching the goal of formal interoperability of different specification languages for software development. With formal interoperability, a specification can contain parts written in different logical frameworks using a multiparadigm specification language, and one can re-use tools which are available for one framework also for other frameworks. }, added-at = {2016-08-05T15:59:03.000+0200}, author = {Mossakowski, T.}, biburl = {https://www.bibsonomy.org/bibtex/24de316943adb370e4631c24cb9658bfd/tillmo}, booktitle = {Computer Science Logic. 9th Workshop, CSL'95. Paderborn, Germany, September 1995, Selected Papers}, editor = {B{\"u}ning, H. Kleine}, interhash = {d42b92ab1f15c3a2e9b24941dd839d46}, intrahash = {4de316943adb370e4631c24cb9658bfd}, isbn = {3-540-61377-3}, keywords = {imported}, pages = {403--433}, psurl = {http://www.informatik.uni-bremen.de/~till/papers/equiv.ps}, publisher = {Springer Verlag, London}, series = {Lecture Notes in Computer Science}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {Equivalences among various logical frameworks of partial algebras}, url = {http://www.springerlink.com/(bt4qw245oavupgzdxw3zpuul)/app/home/contribution.asp?referrer=parent&backto=searchcitationsresults,1,38;}, volume = 1092, year = 1996 }