From flirts@mail.informatik.uni-bremen.de Wed Jan 8 16:26:33 2003 From: flirts@mail.informatik.uni-bremen.de (Amilcar Sernadas) Date: Wed, 08 Jan 2003 16:26:33 +0000 Subject: [Flirts] new paper on fibring Message-ID: <5.1.0.14.0.20030108162538.03216478@pop.math.ist.utl.pt> C. Caleiro, P. Gouveia, and J. Ramos. Completeness results for fibred parchments: Beyond the propositional base. Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2003. Presented at WADT02. Submitted for publication. http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.ps http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From flirts@mail.informatik.uni-bremen.de Mon Jan 27 16:03:01 2003 From: flirts@mail.informatik.uni-bremen.de (Amilcar Sernadas) Date: Mon, 27 Jan 2003 16:03:01 +0000 Subject: [Flirts] 2 new papers Message-ID: <5.1.0.14.0.20030127160046.02ec48f0@pop.math.ist.utl.pt> C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Dyadic semantics for many-valued logics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic2.pdf C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Suszko's Thesis and dyadic semantics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic1.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From flirts@mail.informatik.uni-bremen.de Tue Apr 15 16:56:37 2003 From: flirts@mail.informatik.uni-bremen.de (Amilcar Sernadas) Date: Tue, 15 Apr 2003 16:56:37 +0100 Subject: [Flirts] new paper Message-ID: <5.1.0.14.0.20030415164602.022827a8@pop.math.ist.utl.pt> Dear friends, maybe you will be interested in our latest paper P. Mateus, A. Sernadas, C. Sernadas, and L. Viganò. Modal sequent calculi labelled with truth values: Completeness, duality and analyticity. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. available at http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.ps http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.pdf best wishes Amilcar ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From flirts@mail.informatik.uni-bremen.de Wed May 21 15:42:56 2003 From: flirts@mail.informatik.uni-bremen.de (Till Mossakowski) Date: Wed, 21 May 2003 16:42:56 +0200 Subject: [Flirts] Re: institution representations, junk models, and completeness In-Reply-To: <3ECB93C7.D5786D36@imm.dtu.dk> References: <3ECB93C7.D5786D36@imm.dtu.dk> Message-ID: <3ECB9070.4000800@informatik.uni-bremen.de> Dear Morten, I cc this to the Flirts mailing list since it may be of general interest. Indeed, for institution representations (now called comorphisms in a recent landmark paper by Jo Goguen and Grigore Rosu that has appeared in Formal ascpetcs of computing) with surjective partial model translations, soundness is preserved, but not completeness. Maura Cerioli has examined such translations in her thesis, where she also proved this statement (this is also contained in her WADT 91 paper, LNCS 655). Maura introduced also so-called "logical simulations", where the domain of the model translation is axiomatized with a theory, in order to restore completeness. These correspond to simple representations, simple maps of institutions, or, in the new terminology of Jo and Grigore, simple theoroidal comorphisms. Hence, in a nutshell, I always would give the advice to enrich your signature translation (by translating signatures to whole theories) such that the model translation becomes total. For RSL, this probably means that the HOL types have to be equipped with a cpo structure or something similar. Greetings, Till Morten Lindegaard wrote: > Dear Till, > > I hope everything is well in Bremen. > > I would be very grateful if you had some comments/ideas/experiences on > the following issue: > > When I try to define an institution representation, \rho, from RSL to > HOL, there are some difficulties regarding \beta_\Sigma. > > The RSL signatures may contain sort types, and \rho is defined such that > an RSL signature containing a sort "s" is mapped to a HOL presentation > containing the type constant "(s,0)". > > In an RSL model, the sort "s" is interpreted as some "value domain" > denoting an RSL type. In a HOL model, the type "s()" is interpreted as > some set in the universe U - and this set may not correspond directly to > a value domain in RSL. Consequently, there seems to be HOL models which > do not correspond to RSL models, making \beta_\Sigma partial. > > Althought \beta_\Sigma is partial, it is still surjective, and as far as > I can see, reusing a HOL theorem prover by translating specifications > along \rho is sound. > > But what about completeness? Is semantic consequence preserved when > translating specifications and sentences along \rho? Anne and I > discussed to which extend the occurence of "junk HOL models" makes it > difficult/impossible to prove translated RSL sentences in the "HOL > world", and we would like to ask you if you had ideas or experiences > with this matter. > > Greetings, > > Morten -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From flirts@mail.informatik.uni-bremen.de Thu May 29 08:28:41 2003 From: flirts@mail.informatik.uni-bremen.de (Till Mossakowski) Date: Thu, 29 May 2003 09:28:41 +0200 Subject: [Flirts] Re: hol institution; please send your FLIRTS publications In-Reply-To: <200305281907.h4SJ7WH18005@stoilow.imar.ro> References: <200305281907.h4SJ7WH18005@stoilow.imar.ro> Message-ID: <3ED5B6A9.4090308@informatik.uni-bremen.de> [This reminds me: could all of you send BiBTeX entries of your recent FLIRTS publications to me, so that I can update the bibliography accordingly? Till] Dear Razvan, > But I would like to ask you a question. This is related to the recent > flirts message which reminded me of something. > Do you know any nice definition for a higher order logic institution? > Of course I could invent something but it is better to use a good > existing one. A detailed description of a HOL institution is given in @inproceedings{Borzyszkowski99, author = "Tomasz Borzyszkowski", title = "Higher-Order Logic and Theorem Proving for Structured Specifications", booktitle = "Workshop on Algebraic Development Techniques 1999", pages = "401-418", year = "2000", editor = "Christine Choppy and Didier Bert and Peter Mosses", series = "LNCS", volume = "1827", } Acutally, this reference is missing in the FLIRTS bibliography - I will add it (sorry, Tomek!). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From flirts@mail.informatik.uni-bremen.de Thu May 29 08:28:57 2003 From: flirts@mail.informatik.uni-bremen.de (Till Mossakowski) Date: Thu, 29 May 2003 09:28:57 +0200 Subject: [Flirts] New paper on heterogeneous specification Message-ID: <3ED5B6B9.1080308@informatik.uni-bremen.de> Dear FLIRTers, I have recently completed a paper Foundations of heterogeneous specification to be found at http://www.tzi.de/~till/publications.html Besides general considerations about heterogeneous specifications, it also contains a sketch of an institution for CSP (there has been a discussion among this community about this point some years ago - unfortunately before the FLIRTS archive started to work). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From flirts@mail.informatik.uni-bremen.de Fri Jun 27 07:20:27 2003 From: flirts@mail.informatik.uni-bremen.de (Giuseppe Scollo) Date: Fri, 27 Jun 2003 08:20:27 +0200 (MET DST) Subject: [Flirts] graph colouring institutions Message-ID: Hello FLIRTerS, the 2-page abstract which I contributed to the latest FLIRTS workshop has evolved into a sequence of three papers, at different levels of completeness and detail, all available through my website: 1. A 10-page extended abstract G. Scollo, Graph colouring institutions, in: R. Berghammer, B. Moeller (Eds.), 7th Seminar RelMiCS, 2nd Workshop Kleene Algebra, Malente, Germany, 12-17 May 2003, pp. 288-297. Available from the RelMiCS 7 website: URL: http://www.informatik.uni-kiel.de/~relmics7 2. A 12-page conference proceedings' (draft) version G. Scollo, An institution isomorphism for planar graph colouring, U. of Verona, Dip. Informatica, June 2003, (short version of RR 03/2003, submitted). PDF: http://www.di.univr.it/~scollo/papers/IIPGC03.pdf 3. A 20-page research report G. Scollo, Morphism-driven design of graph colouring institutions, U. of Verona, Dip. Informatica, RR 03/2003, March 2003 (submitted). PDF: http://www.di.univr.it/~scollo/papers/dirr0303.pdf Comments are welcome, Pippo _____________ Dr. G. Scollo, Università di Verona, Dipartimento di Informatica mailto:giuseppe.scollo@univr.it http://www.sci.univr.it/~scollo From flirts@mail.informatik.uni-bremen.de Mon Oct 6 11:50:38 2003 From: flirts@mail.informatik.uni-bremen.de (Amilcar Sernadas) Date: Mon, 06 Oct 2003 11:50:38 +0100 Subject: [Flirts] CombLog04: Call for Contributions Message-ID: <5.1.0.14.0.20031006114909.01e53c18@mailcentral.math.ist.utl.pt> CombLog'04 Workshop on Combination of Logics: Theory and Applications CLC, Department of Mathematics, IST, Lisbon, Portugal July 28-30, 2004 http://www.cs.math.ist.utl.pt/comblog04/ -------------------------------------------------------------------------------- Call for Contributions The workshop aims to provide a forum for interaction and exchange of ideas among a limited number of participants in the general area of analysis and synthesis of logics and related topics. Prospective contributors are invited to submit an extended abstract (up to six pages) describing innovative proposals and results. Electronic submissions in the form of ps or pdf files to be sent to acs@math.ist.utl.pt by February 01, 2004. -------------------------------------------------------------------------------- Topics Different forms of composing and decomposing logics, such as fibring, fusion, splicing, splitting, synchronization and temporalization. Transference results between the whole and the component logics, such as preservation of completeness, interpolation properties and decidability. Application domains, such as security, software specification and verification, knowledge representation and formal ethics. Important dates February 01, 2004 - Deadline for submitting extended abstracts (up to 6 pages including references). April 01, 2004 - Notification of program and list of participants. May 01, 2004 - Deadline for reception of final version of extended abstracts. May 15, 2004 - Deadline for registration and hotel booking through the organization. Organization Walter A. Carnielli, CLE, University of Campinas. Marcelo E. Coniglio, CLE, University of Campinas. Paulo Mateus, CLC, IST, Technical University of Lisbon. Till Mossakowski, University of Bremen. Amílcar Sernadas (Chair), CLC, IST, Technical University of Lisbon. Keynote speakers (confirmed) Dov Gabbay, King's College, London. Joseph Halpern, Cornell University. Dick de Jongh, University of Amsterdam. Gabriel Sandu, University of Helsinki. Andrzej Tarlecki, Warsaw University. Frank Wolter, University of Liverpool. Other invited participants (to be confirmed) Carlos Areces, Langue et Dialog (LED), INRIA Lorraine. Marcelo Finger, IME, São Paulo University. Joseph Goguen, University of California, San Diego. Don Pigozzi, Iowa State University. Luca Viganò, ETH Zentrum, Zürich. Alberto Zanardo,University of Padova. Publication Electronic publication of extended abstracts at CLE e-Prints. Publication (planned) of selected full papers in the series Studies in Logic and Computation, King's College Publications, Research Studies Press, England. Sponsors ASL: The Association for Symbolic Logic, USA (ASL student members are encouraged to apply for the ASL travel funds available for sponsored meetings). CLC: Center for Logic and Computation, IST, Lisbon, Portugal. CLE: Centre for Logic, Epistemology and the History of Science, UNICAMP, Campinas, Brazil. FLIRTS Interest Group. -------------------------------------------------------------------------------- For further information contact acs@math.ist.utl.pt. Last update: October 6, 2003. -------------------------------------------------------------------------------- ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://cs.math.ist.utl.pt/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Wed Jan 8 17:26:33 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] new paper on fibring Message-ID: <5.1.0.14.0.20030108162538.03216478@pop.math.ist.utl.pt> C. Caleiro, P. Gouveia, and J. Ramos. Completeness results for fibred parchments: Beyond the propositional base. Research report, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Presented at WADT02. Submitted for publication. http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.ps http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Mon Jan 27 17:03:01 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] 2 new papers Message-ID: <5.1.0.14.0.20030127160046.02ec48f0@pop.math.ist.utl.pt> C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Dyadic semantics for many-valued logics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic2.pdf C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Suszko's Thesis and dyadic semantics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic1.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Tue Apr 15 17:56:37 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] new paper Message-ID: <5.1.0.14.0.20030415164602.022827a8@pop.math.ist.utl.pt> Dear friends, maybe you will be interested in our latest paper P. Mateus, A. Sernadas, C. Sernadas, and L. Vigan?. Modal sequent calculi labelled with truth values: Completeness, duality and analyticity. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. available at http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.ps http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.pdf best wishes Amilcar ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From till at Informatik.Uni-Bremen.DE Wed May 21 16:42:56 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] Re: institution representations, junk models, and completeness In-Reply-To: <3ECB93C7.D5786D36@imm.dtu.dk> References: <3ECB93C7.D5786D36@imm.dtu.dk> Message-ID: <3ECB9070.4000800@informatik.uni-bremen.de> Dear Morten, I cc this to the Flirts mailing list since it may be of general interest. Indeed, for institution representations (now called comorphisms in a recent landmark paper by Jo Goguen and Grigore Rosu that has appeared in Formal ascpetcs of computing) with surjective partial model translations, soundness is preserved, but not completeness. Maura Cerioli has examined such translations in her thesis, where she also proved this statement (this is also contained in her WADT 91 paper, LNCS 655). Maura introduced also so-called "logical simulations", where the domain of the model translation is axiomatized with a theory, in order to restore completeness. These correspond to simple representations, simple maps of institutions, or, in the new terminology of Jo and Grigore, simple theoroidal comorphisms. Hence, in a nutshell, I always would give the advice to enrich your signature translation (by translating signatures to whole theories) such that the model translation becomes total. For RSL, this probably means that the HOL types have to be equipped with a cpo structure or something similar. Greetings, Till Morten Lindegaard wrote: > Dear Till, > > I hope everything is well in Bremen. > > I would be very grateful if you had some comments/ideas/experiences on > the following issue: > > When I try to define an institution representation, \rho, from RSL to > HOL, there are some difficulties regarding \beta_\Sigma. > > The RSL signatures may contain sort types, and \rho is defined such that > an RSL signature containing a sort "s" is mapped to a HOL presentation > containing the type constant "(s,0)". > > In an RSL model, the sort "s" is interpreted as some "value domain" > denoting an RSL type. In a HOL model, the type "s()" is interpreted as > some set in the universe U - and this set may not correspond directly to > a value domain in RSL. Consequently, there seems to be HOL models which > do not correspond to RSL models, making \beta_\Sigma partial. > > Althought \beta_\Sigma is partial, it is still surjective, and as far as > I can see, reusing a HOL theorem prover by translating specifications > along \rho is sound. > > But what about completeness? Is semantic consequence preserved when > translating specifications and sentences along \rho? Anne and I > discussed to which extend the occurence of "junk HOL models" makes it > difficult/impossible to prove translated RSL sentences in the "HOL > world", and we would like to ask you if you had ideas or experiences > with this matter. > > Greetings, > > Morten -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From till at Informatik.Uni-Bremen.DE Thu May 29 09:28:41 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] Re: hol institution; please send your FLIRTS publications In-Reply-To: <200305281907.h4SJ7WH18005@stoilow.imar.ro> References: <200305281907.h4SJ7WH18005@stoilow.imar.ro> Message-ID: <3ED5B6A9.4090308@informatik.uni-bremen.de> [This reminds me: could all of you send BiBTeX entries of your recent FLIRTS publications to me, so that I can update the bibliography accordingly? Till] Dear Razvan, > But I would like to ask you a question. This is related to the recent > flirts message which reminded me of something. > Do you know any nice definition for a higher order logic institution? > Of course I could invent something but it is better to use a good > existing one. A detailed description of a HOL institution is given in @inproceedings{Borzyszkowski99, author = "Tomasz Borzyszkowski", title = "Higher-Order Logic and Theorem Proving for Structured Specifications", booktitle = "Workshop on Algebraic Development Techniques 1999", pages = "401-418", year = "2000", editor = "Christine Choppy and Didier Bert and Peter Mosses", series = "LNCS", volume = "1827", } Acutally, this reference is missing in the FLIRTS bibliography - I will add it (sorry, Tomek!). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From till at Informatik.Uni-Bremen.DE Thu May 29 09:28:57 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] New paper on heterogeneous specification Message-ID: <3ED5B6B9.1080308@informatik.uni-bremen.de> Dear FLIRTers, I have recently completed a paper Foundations of heterogeneous specification to be found at http://www.tzi.de/~till/publications.html Besides general considerations about heterogeneous specifications, it also contains a sketch of an institution for CSP (there has been a discussion among this community about this point some years ago - unfortunately before the FLIRTS archive started to work). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From giuseppe.scollo at univr.it Fri Jun 27 08:20:27 2003 From: giuseppe.scollo at univr.it (Giuseppe Scollo) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] graph colouring institutions Message-ID: Hello FLIRTerS, the 2-page abstract which I contributed to the latest FLIRTS workshop has evolved into a sequence of three papers, at different levels of completeness and detail, all available through my website: 1. A 10-page extended abstract G. Scollo, Graph colouring institutions, in: R. Berghammer, B. Moeller (Eds.), 7th Seminar RelMiCS, 2nd Workshop Kleene Algebra, Malente, Germany, 12-17 May 2003, pp. 288-297. Available from the RelMiCS 7 website: URL: http://www.informatik.uni-kiel.de/~relmics7 2. A 12-page conference proceedings' (draft) version G. Scollo, An institution isomorphism for planar graph colouring, U. of Verona, Dip. Informatica, June 2003, (short version of RR 03/2003, submitted). PDF: http://www.di.univr.it/~scollo/papers/IIPGC03.pdf 3. A 20-page research report G. Scollo, Morphism-driven design of graph colouring institutions, U. of Verona, Dip. Informatica, RR 03/2003, March 2003 (submitted). PDF: http://www.di.univr.it/~scollo/papers/dirr0303.pdf Comments are welcome, Pippo _____________ Dr. G. Scollo, Università di Verona, Dipartimento di Informatica mailto:giuseppe.scollo@univr.it http://www.sci.univr.it/~scollo From acs at math.ist.utl.pt Mon Oct 6 12:50:38 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Thu Aug 18 10:12:46 2005 Subject: [Flirts] CombLog04: Call for Contributions Message-ID: <5.1.0.14.0.20031006114909.01e53c18@mailcentral.math.ist.utl.pt> CombLog'04 Workshop on Combination of Logics: Theory and Applications CLC, Department of Mathematics, IST, Lisbon, Portugal July 28-30, 2004 http://www.cs.math.ist.utl.pt/comblog04/ -------------------------------------------------------------------------------- Call for Contributions The workshop aims to provide a forum for interaction and exchange of ideas among a limited number of participants in the general area of analysis and synthesis of logics and related topics. Prospective contributors are invited to submit an extended abstract (up to six pages) describing innovative proposals and results. Electronic submissions in the form of ps or pdf files to be sent to acs@math.ist.utl.pt by February 01, 2004. -------------------------------------------------------------------------------- Topics Different forms of composing and decomposing logics, such as fibring, fusion, splicing, splitting, synchronization and temporalization. Transference results between the whole and the component logics, such as preservation of completeness, interpolation properties and decidability. Application domains, such as security, software specification and verification, knowledge representation and formal ethics. Important dates February 01, 2004 - Deadline for submitting extended abstracts (up to 6 pages including references). April 01, 2004 - Notification of program and list of participants. May 01, 2004 - Deadline for reception of final version of extended abstracts. May 15, 2004 - Deadline for registration and hotel booking through the organization. Organization Walter A. Carnielli, CLE, University of Campinas. Marcelo E. Coniglio, CLE, University of Campinas. Paulo Mateus, CLC, IST, Technical University of Lisbon. Till Mossakowski, University of Bremen. Am?lcar Sernadas (Chair), CLC, IST, Technical University of Lisbon. Keynote speakers (confirmed) Dov Gabbay, King's College, London. Joseph Halpern, Cornell University. Dick de Jongh, University of Amsterdam. Gabriel Sandu, University of Helsinki. Andrzej Tarlecki, Warsaw University. Frank Wolter, University of Liverpool. Other invited participants (to be confirmed) Carlos Areces, Langue et Dialog (LED), INRIA Lorraine. Marcelo Finger, IME, S?o Paulo University. Joseph Goguen, University of California, San Diego. Don Pigozzi, Iowa State University. Luca Vigan?, ETH Zentrum, Z?rich. Alberto Zanardo,University of Padova. Publication Electronic publication of extended abstracts at CLE e-Prints. Publication (planned) of selected full papers in the series Studies in Logic and Computation, King's College Publications, Research Studies Press, England. Sponsors ASL: The Association for Symbolic Logic, USA (ASL student members are encouraged to apply for the ASL travel funds available for sponsored meetings). CLC: Center for Logic and Computation, IST, Lisbon, Portugal. CLE: Centre for Logic, Epistemology and the History of Science, UNICAMP, Campinas, Brazil. FLIRTS Interest Group. -------------------------------------------------------------------------------- For further information contact acs@math.ist.utl.pt. Last update: October 6, 2003. -------------------------------------------------------------------------------- ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://cs.math.ist.utl.pt/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Wed Jan 8 17:26:33 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Tue Aug 30 15:43:11 2005 Subject: [Flirts] new paper on fibring Message-ID: <5.1.0.14.0.20030108162538.03216478@pop.math.ist.utl.pt> C. Caleiro, P. Gouveia, and J. Ramos. Completeness results for fibred parchments: Beyond the propositional base. Research report, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Presented at WADT02. Submitted for publication. http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.ps http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Mon Jan 27 17:03:01 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Tue Aug 30 15:43:11 2005 Subject: [Flirts] 2 new papers Message-ID: <5.1.0.14.0.20030127160046.02ec48f0@pop.math.ist.utl.pt> C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Dyadic semantics for many-valued logics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic2.pdf C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Suszko's Thesis and dyadic semantics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic1.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Tue Apr 15 17:56:37 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Tue Aug 30 15:43:12 2005 Subject: [Flirts] new paper Message-ID: <5.1.0.14.0.20030415164602.022827a8@pop.math.ist.utl.pt> Dear friends, maybe you will be interested in our latest paper P. Mateus, A. Sernadas, C. Sernadas, and L. Vigan?. Modal sequent calculi labelled with truth values: Completeness, duality and analyticity. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. available at http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.ps http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.pdf best wishes Amilcar ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From till at Informatik.Uni-Bremen.DE Wed May 21 16:42:56 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Tue Aug 30 15:43:12 2005 Subject: [Flirts] Re: institution representations, junk models, and completeness In-Reply-To: <3ECB93C7.D5786D36@imm.dtu.dk> References: <3ECB93C7.D5786D36@imm.dtu.dk> Message-ID: <3ECB9070.4000800@informatik.uni-bremen.de> Dear Morten, I cc this to the Flirts mailing list since it may be of general interest. Indeed, for institution representations (now called comorphisms in a recent landmark paper by Jo Goguen and Grigore Rosu that has appeared in Formal ascpetcs of computing) with surjective partial model translations, soundness is preserved, but not completeness. Maura Cerioli has examined such translations in her thesis, where she also proved this statement (this is also contained in her WADT 91 paper, LNCS 655). Maura introduced also so-called "logical simulations", where the domain of the model translation is axiomatized with a theory, in order to restore completeness. These correspond to simple representations, simple maps of institutions, or, in the new terminology of Jo and Grigore, simple theoroidal comorphisms. Hence, in a nutshell, I always would give the advice to enrich your signature translation (by translating signatures to whole theories) such that the model translation becomes total. For RSL, this probably means that the HOL types have to be equipped with a cpo structure or something similar. Greetings, Till Morten Lindegaard wrote: > Dear Till, > > I hope everything is well in Bremen. > > I would be very grateful if you had some comments/ideas/experiences on > the following issue: > > When I try to define an institution representation, \rho, from RSL to > HOL, there are some difficulties regarding \beta_\Sigma. > > The RSL signatures may contain sort types, and \rho is defined such that > an RSL signature containing a sort "s" is mapped to a HOL presentation > containing the type constant "(s,0)". > > In an RSL model, the sort "s" is interpreted as some "value domain" > denoting an RSL type. In a HOL model, the type "s()" is interpreted as > some set in the universe U - and this set may not correspond directly to > a value domain in RSL. Consequently, there seems to be HOL models which > do not correspond to RSL models, making \beta_\Sigma partial. > > Althought \beta_\Sigma is partial, it is still surjective, and as far as > I can see, reusing a HOL theorem prover by translating specifications > along \rho is sound. > > But what about completeness? Is semantic consequence preserved when > translating specifications and sentences along \rho? Anne and I > discussed to which extend the occurence of "junk HOL models" makes it > difficult/impossible to prove translated RSL sentences in the "HOL > world", and we would like to ask you if you had ideas or experiences > with this matter. > > Greetings, > > Morten -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From till at Informatik.Uni-Bremen.DE Thu May 29 09:28:41 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Tue Aug 30 15:43:12 2005 Subject: [Flirts] Re: hol institution; please send your FLIRTS publications In-Reply-To: <200305281907.h4SJ7WH18005@stoilow.imar.ro> References: <200305281907.h4SJ7WH18005@stoilow.imar.ro> Message-ID: <3ED5B6A9.4090308@informatik.uni-bremen.de> [This reminds me: could all of you send BiBTeX entries of your recent FLIRTS publications to me, so that I can update the bibliography accordingly? Till] Dear Razvan, > But I would like to ask you a question. This is related to the recent > flirts message which reminded me of something. > Do you know any nice definition for a higher order logic institution? > Of course I could invent something but it is better to use a good > existing one. A detailed description of a HOL institution is given in @inproceedings{Borzyszkowski99, author = "Tomasz Borzyszkowski", title = "Higher-Order Logic and Theorem Proving for Structured Specifications", booktitle = "Workshop on Algebraic Development Techniques 1999", pages = "401-418", year = "2000", editor = "Christine Choppy and Didier Bert and Peter Mosses", series = "LNCS", volume = "1827", } Acutally, this reference is missing in the FLIRTS bibliography - I will add it (sorry, Tomek!). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From till at Informatik.Uni-Bremen.DE Thu May 29 09:28:57 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Tue Aug 30 15:43:12 2005 Subject: [Flirts] New paper on heterogeneous specification Message-ID: <3ED5B6B9.1080308@informatik.uni-bremen.de> Dear FLIRTers, I have recently completed a paper Foundations of heterogeneous specification to be found at http://www.tzi.de/~till/publications.html Besides general considerations about heterogeneous specifications, it also contains a sketch of an institution for CSP (there has been a discussion among this community about this point some years ago - unfortunately before the FLIRTS archive started to work). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From giuseppe.scollo at univr.it Fri Jun 27 08:20:27 2003 From: giuseppe.scollo at univr.it (Giuseppe Scollo) Date: Tue Aug 30 15:43:12 2005 Subject: [Flirts] graph colouring institutions Message-ID: Hello FLIRTerS, the 2-page abstract which I contributed to the latest FLIRTS workshop has evolved into a sequence of three papers, at different levels of completeness and detail, all available through my website: 1. A 10-page extended abstract G. Scollo, Graph colouring institutions, in: R. Berghammer, B. Moeller (Eds.), 7th Seminar RelMiCS, 2nd Workshop Kleene Algebra, Malente, Germany, 12-17 May 2003, pp. 288-297. Available from the RelMiCS 7 website: URL: http://www.informatik.uni-kiel.de/~relmics7 2. A 12-page conference proceedings' (draft) version G. Scollo, An institution isomorphism for planar graph colouring, U. of Verona, Dip. Informatica, June 2003, (short version of RR 03/2003, submitted). PDF: http://www.di.univr.it/~scollo/papers/IIPGC03.pdf 3. A 20-page research report G. Scollo, Morphism-driven design of graph colouring institutions, U. of Verona, Dip. Informatica, RR 03/2003, March 2003 (submitted). PDF: http://www.di.univr.it/~scollo/papers/dirr0303.pdf Comments are welcome, Pippo _____________ Dr. G. Scollo, Università di Verona, Dipartimento di Informatica mailto:giuseppe.scollo@univr.it http://www.sci.univr.it/~scollo From acs at math.ist.utl.pt Mon Oct 6 12:50:38 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Tue Aug 30 15:43:12 2005 Subject: [Flirts] CombLog04: Call for Contributions Message-ID: <5.1.0.14.0.20031006114909.01e53c18@mailcentral.math.ist.utl.pt> CombLog'04 Workshop on Combination of Logics: Theory and Applications CLC, Department of Mathematics, IST, Lisbon, Portugal July 28-30, 2004 http://www.cs.math.ist.utl.pt/comblog04/ -------------------------------------------------------------------------------- Call for Contributions The workshop aims to provide a forum for interaction and exchange of ideas among a limited number of participants in the general area of analysis and synthesis of logics and related topics. Prospective contributors are invited to submit an extended abstract (up to six pages) describing innovative proposals and results. Electronic submissions in the form of ps or pdf files to be sent to acs@math.ist.utl.pt by February 01, 2004. -------------------------------------------------------------------------------- Topics Different forms of composing and decomposing logics, such as fibring, fusion, splicing, splitting, synchronization and temporalization. Transference results between the whole and the component logics, such as preservation of completeness, interpolation properties and decidability. Application domains, such as security, software specification and verification, knowledge representation and formal ethics. Important dates February 01, 2004 - Deadline for submitting extended abstracts (up to 6 pages including references). April 01, 2004 - Notification of program and list of participants. May 01, 2004 - Deadline for reception of final version of extended abstracts. May 15, 2004 - Deadline for registration and hotel booking through the organization. Organization Walter A. Carnielli, CLE, University of Campinas. Marcelo E. Coniglio, CLE, University of Campinas. Paulo Mateus, CLC, IST, Technical University of Lisbon. Till Mossakowski, University of Bremen. Am?lcar Sernadas (Chair), CLC, IST, Technical University of Lisbon. Keynote speakers (confirmed) Dov Gabbay, King's College, London. Joseph Halpern, Cornell University. Dick de Jongh, University of Amsterdam. Gabriel Sandu, University of Helsinki. Andrzej Tarlecki, Warsaw University. Frank Wolter, University of Liverpool. Other invited participants (to be confirmed) Carlos Areces, Langue et Dialog (LED), INRIA Lorraine. Marcelo Finger, IME, S?o Paulo University. Joseph Goguen, University of California, San Diego. Don Pigozzi, Iowa State University. Luca Vigan?, ETH Zentrum, Z?rich. Alberto Zanardo,University of Padova. Publication Electronic publication of extended abstracts at CLE e-Prints. Publication (planned) of selected full papers in the series Studies in Logic and Computation, King's College Publications, Research Studies Press, England. Sponsors ASL: The Association for Symbolic Logic, USA (ASL student members are encouraged to apply for the ASL travel funds available for sponsored meetings). CLC: Center for Logic and Computation, IST, Lisbon, Portugal. CLE: Centre for Logic, Epistemology and the History of Science, UNICAMP, Campinas, Brazil. FLIRTS Interest Group. -------------------------------------------------------------------------------- For further information contact acs@math.ist.utl.pt. Last update: October 6, 2003. -------------------------------------------------------------------------------- ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://cs.math.ist.utl.pt/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Wed Jan 8 17:26:33 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] new paper on fibring Message-ID: <5.1.0.14.0.20030108162538.03216478@pop.math.ist.utl.pt> C. Caleiro, P. Gouveia, and J. Ramos. Completeness results for fibred parchments: Beyond the propositional base. Research report, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Presented at WADT02. Submitted for publication. http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.ps http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CGR-fiblog16.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Mon Jan 27 17:03:01 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] 2 new papers Message-ID: <5.1.0.14.0.20030127160046.02ec48f0@pop.math.ist.utl.pt> C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Dyadic semantics for many-valued logics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic2.pdf C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Suszko's Thesis and dyadic semantics. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. Get a preprint: http://www.cs.math.ist.utl.pt/ftp/pub/CaleiroC/03-CCCM-dyadic1.pdf ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From acs at math.ist.utl.pt Tue Apr 15 17:56:37 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] new paper Message-ID: <5.1.0.14.0.20030415164602.022827a8@pop.math.ist.utl.pt> Dear friends, maybe you will be interested in our latest paper P. Mateus, A. Sernadas, C. Sernadas, and L. Vigan?. Modal sequent calculi labelled with truth values: Completeness, duality and analyticity. Preprint, Section of Computer Science, Department of Mathematics, Instituto Superior T?cnico, 1049-001 Lisboa, Portugal, 2003. Submitted for publication. available at http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.ps http://www.cs.math.ist.utl.pt/ftp/pub/SernadasA/03-MSSV-fiblog19.pdf best wishes Amilcar ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://www.cs.math.ist.utl.pt/cs/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++ From till at Informatik.Uni-Bremen.DE Wed May 21 16:42:56 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] Re: institution representations, junk models, and completeness In-Reply-To: <3ECB93C7.D5786D36@imm.dtu.dk> References: <3ECB93C7.D5786D36@imm.dtu.dk> Message-ID: <3ECB9070.4000800@informatik.uni-bremen.de> Dear Morten, I cc this to the Flirts mailing list since it may be of general interest. Indeed, for institution representations (now called comorphisms in a recent landmark paper by Jo Goguen and Grigore Rosu that has appeared in Formal ascpetcs of computing) with surjective partial model translations, soundness is preserved, but not completeness. Maura Cerioli has examined such translations in her thesis, where she also proved this statement (this is also contained in her WADT 91 paper, LNCS 655). Maura introduced also so-called "logical simulations", where the domain of the model translation is axiomatized with a theory, in order to restore completeness. These correspond to simple representations, simple maps of institutions, or, in the new terminology of Jo and Grigore, simple theoroidal comorphisms. Hence, in a nutshell, I always would give the advice to enrich your signature translation (by translating signatures to whole theories) such that the model translation becomes total. For RSL, this probably means that the HOL types have to be equipped with a cpo structure or something similar. Greetings, Till Morten Lindegaard wrote: > Dear Till, > > I hope everything is well in Bremen. > > I would be very grateful if you had some comments/ideas/experiences on > the following issue: > > When I try to define an institution representation, \rho, from RSL to > HOL, there are some difficulties regarding \beta_\Sigma. > > The RSL signatures may contain sort types, and \rho is defined such that > an RSL signature containing a sort "s" is mapped to a HOL presentation > containing the type constant "(s,0)". > > In an RSL model, the sort "s" is interpreted as some "value domain" > denoting an RSL type. In a HOL model, the type "s()" is interpreted as > some set in the universe U - and this set may not correspond directly to > a value domain in RSL. Consequently, there seems to be HOL models which > do not correspond to RSL models, making \beta_\Sigma partial. > > Althought \beta_\Sigma is partial, it is still surjective, and as far as > I can see, reusing a HOL theorem prover by translating specifications > along \rho is sound. > > But what about completeness? Is semantic consequence preserved when > translating specifications and sentences along \rho? Anne and I > discussed to which extend the occurence of "junk HOL models" makes it > difficult/impossible to prove translated RSL sentences in the "HOL > world", and we would like to ask you if you had ideas or experiences > with this matter. > > Greetings, > > Morten -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From till at Informatik.Uni-Bremen.DE Thu May 29 09:28:41 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] Re: hol institution; please send your FLIRTS publications In-Reply-To: <200305281907.h4SJ7WH18005@stoilow.imar.ro> References: <200305281907.h4SJ7WH18005@stoilow.imar.ro> Message-ID: <3ED5B6A9.4090308@informatik.uni-bremen.de> [This reminds me: could all of you send BiBTeX entries of your recent FLIRTS publications to me, so that I can update the bibliography accordingly? Till] Dear Razvan, > But I would like to ask you a question. This is related to the recent > flirts message which reminded me of something. > Do you know any nice definition for a higher order logic institution? > Of course I could invent something but it is better to use a good > existing one. A detailed description of a HOL institution is given in @inproceedings{Borzyszkowski99, author = "Tomasz Borzyszkowski", title = "Higher-Order Logic and Theorem Proving for Structured Specifications", booktitle = "Workshop on Algebraic Development Techniques 1999", pages = "401-418", year = "2000", editor = "Christine Choppy and Didier Bert and Peter Mosses", series = "LNCS", volume = "1827", } Acutally, this reference is missing in the FLIRTS bibliography - I will add it (sorry, Tomek!). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From till at Informatik.Uni-Bremen.DE Thu May 29 09:28:57 2003 From: till at Informatik.Uni-Bremen.DE (Till Mossakowski) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] New paper on heterogeneous specification Message-ID: <3ED5B6B9.1080308@informatik.uni-bremen.de> Dear FLIRTers, I have recently completed a paper Foundations of heterogeneous specification to be found at http://www.tzi.de/~till/publications.html Besides general considerations about heterogeneous specifications, it also contains a sketch of an institution for CSP (there has been a discussion among this community about this point some years ago - unfortunately before the FLIRTS archive started to work). Greetings, Till -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till From giuseppe.scollo at univr.it Fri Jun 27 08:20:27 2003 From: giuseppe.scollo at univr.it (Giuseppe Scollo) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] graph colouring institutions Message-ID: Hello FLIRTerS, the 2-page abstract which I contributed to the latest FLIRTS workshop has evolved into a sequence of three papers, at different levels of completeness and detail, all available through my website: 1. A 10-page extended abstract G. Scollo, Graph colouring institutions, in: R. Berghammer, B. Moeller (Eds.), 7th Seminar RelMiCS, 2nd Workshop Kleene Algebra, Malente, Germany, 12-17 May 2003, pp. 288-297. Available from the RelMiCS 7 website: URL: http://www.informatik.uni-kiel.de/~relmics7 2. A 12-page conference proceedings' (draft) version G. Scollo, An institution isomorphism for planar graph colouring, U. of Verona, Dip. Informatica, June 2003, (short version of RR 03/2003, submitted). PDF: http://www.di.univr.it/~scollo/papers/IIPGC03.pdf 3. A 20-page research report G. Scollo, Morphism-driven design of graph colouring institutions, U. of Verona, Dip. Informatica, RR 03/2003, March 2003 (submitted). PDF: http://www.di.univr.it/~scollo/papers/dirr0303.pdf Comments are welcome, Pippo _____________ Dr. G. Scollo, Università di Verona, Dipartimento di Informatica mailto:giuseppe.scollo@univr.it http://www.sci.univr.it/~scollo From acs at math.ist.utl.pt Mon Oct 6 12:50:38 2003 From: acs at math.ist.utl.pt (Amilcar Sernadas) Date: Sun Oct 9 15:15:54 2005 Subject: [Flirts] CombLog04: Call for Contributions Message-ID: <5.1.0.14.0.20031006114909.01e53c18@mailcentral.math.ist.utl.pt> CombLog'04 Workshop on Combination of Logics: Theory and Applications CLC, Department of Mathematics, IST, Lisbon, Portugal July 28-30, 2004 http://www.cs.math.ist.utl.pt/comblog04/ -------------------------------------------------------------------------------- Call for Contributions The workshop aims to provide a forum for interaction and exchange of ideas among a limited number of participants in the general area of analysis and synthesis of logics and related topics. Prospective contributors are invited to submit an extended abstract (up to six pages) describing innovative proposals and results. Electronic submissions in the form of ps or pdf files to be sent to acs@math.ist.utl.pt by February 01, 2004. -------------------------------------------------------------------------------- Topics Different forms of composing and decomposing logics, such as fibring, fusion, splicing, splitting, synchronization and temporalization. Transference results between the whole and the component logics, such as preservation of completeness, interpolation properties and decidability. Application domains, such as security, software specification and verification, knowledge representation and formal ethics. Important dates February 01, 2004 - Deadline for submitting extended abstracts (up to 6 pages including references). April 01, 2004 - Notification of program and list of participants. May 01, 2004 - Deadline for reception of final version of extended abstracts. May 15, 2004 - Deadline for registration and hotel booking through the organization. Organization Walter A. Carnielli, CLE, University of Campinas. Marcelo E. Coniglio, CLE, University of Campinas. Paulo Mateus, CLC, IST, Technical University of Lisbon. Till Mossakowski, University of Bremen. Am?lcar Sernadas (Chair), CLC, IST, Technical University of Lisbon. Keynote speakers (confirmed) Dov Gabbay, King's College, London. Joseph Halpern, Cornell University. Dick de Jongh, University of Amsterdam. Gabriel Sandu, University of Helsinki. Andrzej Tarlecki, Warsaw University. Frank Wolter, University of Liverpool. Other invited participants (to be confirmed) Carlos Areces, Langue et Dialog (LED), INRIA Lorraine. Marcelo Finger, IME, S?o Paulo University. Joseph Goguen, University of California, San Diego. Don Pigozzi, Iowa State University. Luca Vigan?, ETH Zentrum, Z?rich. Alberto Zanardo,University of Padova. Publication Electronic publication of extended abstracts at CLE e-Prints. Publication (planned) of selected full papers in the series Studies in Logic and Computation, King's College Publications, Research Studies Press, England. Sponsors ASL: The Association for Symbolic Logic, USA (ASL student members are encouraged to apply for the ASL travel funds available for sponsored meetings). CLC: Center for Logic and Computation, IST, Lisbon, Portugal. CLE: Centre for Logic, Epistemology and the History of Science, UNICAMP, Campinas, Brazil. FLIRTS Interest Group. -------------------------------------------------------------------------------- For further information contact acs@math.ist.utl.pt. Last update: October 6, 2003. -------------------------------------------------------------------------------- ++++++++++++++++++++++++++++++++++++++++++++++++++ Amilcar Sernadas Departamento de Matematica Instituto Superior Tecnico Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL tel: 351-21-8417150 fax: 351-21-8417598 e-mail: acs@math.ist.utl.pt www: http://cs.math.ist.utl.pt/acs.html ++++++++++++++++++++++++++++++++++++++++++++++++++