[Hol-info] FLoC 2010: Call for Participation
2010 FEDERATED LOGIC CONFERENCE (FLoC'10) Edinburgh, Scotland, U.K. July 9-21, 2010 http://www.floc-conference.org Early registration deadline: 17 May 2010. * The fifth Federated Logic Conference (FLoC'10) will be held in Edinburgh, Scotland, U.K. (www.edinburgh.org), in July 2010, at the School of Informatics at the University of Edinburgh (www.inf.ed.ac.uk). * FLoC'10 promises to be the premier scientific meeting in computational logic in 2010. The following conferences will participate in FLoC: - CAV 2010: Int'l Conference on Computer-Aided Verification - CSF 2010: IEEE Computer Security Foundations Symposium - ICLP 2010: Int'l Conference on Logic Programming - IJCAR 2010: Int'l Joint Conference on Automated Reasoning - ITP 2010: Int'l Conference on Interactive Theorem Proving - LICS 2010: IEEE Symposium on Logic in Computer Science - RTA 2010: Int'l Conference on Rewriting Techniques and Applications - SAT 2010: Int'l Conference on Theory and Applications of Satisfiability Testing The eight major conferences will be accompanied by more than fifty workshops and a number of other affiliated events. * Program: The FLoC'10 program includes plenary talks by David Basin, Georg Gottlob, David Harel, and Gordon Plotkin, as well as keynote talks by Deepak Kapur and J Strother Moore. Please consult the FLoC website for further information on invited speakers and contributed talks of all the participating conferences. * The city of Edinburgh: Edinburgh (http://www.ed.ac.uk/about/city/introduction), one of the most vibrant, cosmopolitan cities in Europe, has been regularly voted one of the most desirable places to live in the world - and the University is at the heart of it all. Located throughout the centre of the city, the campus plays an integral part in the activities of Scotland's lively capital. Set against a beautiful backdrop of stunning architecture, Edinburgh is a welcoming, cosmopolitan city with a large and diverse student population. The city offers an exciting array of entertainment, history, culture and sport, with the lush Scottish countryside and coastline just a few miles away. It is a safe and prosperous city, with an abundance of parks and green spaces for recreation and reflection. FLoC receptions will be held at the Edinburgh Castle (11 July) and the National Galleries of Scotland (16 July). * Registration: For online registration for FLoC, please follow the link on the FLoC website at http://floc-conference.org/registration.html Registration is now open. The deadline for early registration is 17 May. Standard rates will apply for those who register between 18 May and 30 June. For those who register after 30 June, late rates will apply. Note that it is possible to register early, and then add components (e.g., additional workshops, additional registration days, etc.) later on. * Accomodation: Very affordable accommodation has been booked at the University's Pollock Halls campus, about 15-minute walk from the conference site. Room types include single/double rooms with shared facilities/ensuite, and standard hotel rooms in a 3-star Victorian mansion. Alternatively, blocks of rooms have been booked at several hotels in the cite centre. For details, see http://floc-conference.org/accommodation.html * Student Travel Grants: FLoC has raised funds to help students with participating in the 2010 meeting. See details on the conference website. * FLoC'10 Steering Committee: - General Chair: Moshe Y. Vardi - Conference Co-chairs: Leonid Libkin, Gordon Plotkin - CAV Representative: Edmund Clarke - ICLP Representative: Manuel Hermenegildo - IJCAR Representative: Alan Bundy - ITP Representative: Tobias Nipkow - LICS Representative: Martin Abadi - RTA Representative: Juergen Giesl - SAT Representative: Enrico Giunchiglia - EasyChair Representative: Andrei Voronkov -- You are subscribed to the FLoC 2010 mailing list. To unsubscribe please send an email to majord...@informatik.uni-frankfurt.de with the keywords unsubscribe floc2010 in the message body. -- Download Intel#174; Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] prove a goal in HOL4
I have to prove a goal in HOL4 as following: g `!a b c. (indep bern a c) /\ (indep bern b c) == (a IN events bern) /\ (b IN events bern) /\ (c IN events bern) /\ (prob bern (a INTER b INTER c) = prob bern (a INTER b) * prob bern c)`; Here, a and c are independant, also b and c are independant. However, a depends b. Could anybody give me some hints? I really appreciate! Regards, Liya -- Download Intel#174; Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FMICS 2010: Call for Papers (deadline extended)
--- Apologies for multiple copies --- ** * 15th International Workshop on * * Formal Methods for Industrial Critical Systems * * FMICS 2010 * * http://es.fbk.eu/events/fmics2010 * ** * September 20-21, 2010* * Antwerp, Belgium * ** IMPORTANT DATES --- Deadline for abstracts (extended):17 April 2010 Deadline for papers (extended): 25 April 2010 Acceptance notification (extended):7 June 2010 Camera-ready version (extended): 7 July 2010 Workshop: 20-21 September 2010 SCOPE OF THE WORKSHOP - The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops bring together scientists and engineers that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. These workshops also strive to promote research and development for the improvement of formal methods and tools for industrial applications. Topics include, but are not restricted to: * Design, specification, code generation and testing based on formal methods. * Methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, real-time systems and embedded systems. * Verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues). * Tools for the development of formal design descriptions. * Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions. * Impact of the adoption of formal methods on the development process and associated costs. * Application of formal methods in standardization and industrial forums. INVITED SPEAKERS To be announced CO-CHAIRS - Stefan Kowalewski (RWTH-Aachen, Germany) Marco Roveri(FBK-irst, Italy) PROGRAM COMMITTEE --- Aarti Gupta (NEC Labs, US) Andreas Podelski(University of Freiburg, Germany) Andy King (Portcullis Computer Security) Barbara Jobstman(VERIMAG, France) Christophe Joubert (Technical University of Valencia, Spain) Daniel Kroening (ETH Zürich, Switzerland) Diego Latella (CNR/IST Pisa, It) Dino Distefano (Queen Mary, University of London, UK) Francois Pilarski (Airbus, France) Holger Hermanns (Universität des Saarlandes, Germany) Hubert Garavel (INRIA Rhône-Alpes, France) Jaco van de Pol (Universiteit Twente, The Netherlands) Jakob Rehof (Technische Universität Dortmund, Germany) J. José Moreno-Navarro (Universidad Politécnica de Madrid, Spain) Jörg Brauer (RWTH Aachen, Germany) Lubos Brim (Masarykova Univerzita, Czech Republic) Maria Alpuente (Technical University of Valencia, Spain) Marco Roveri(FBK-irst, Italy) Pedro Merino(Universidad de Málaga, Spain) Radu Mateescu (INRIA Rhone-Alpes, France) Stefan Kowalewski (RWTH Aachen, Germany) Stefania Gnesi (ISTI-CNR, Italy) Thierry Lecomte (ClearSy, France) Thomas Kropf(Bosch, Germany) Thomas Santen (Microsoft European Innovation Center) Wan Fokkink (Vrije Universiteit Amsterdam, Netherlands) Wilfried Steiner(TTTech, Austria) ERCIM FMICS WG COORDINATOR -- Alessandro Fantechi (Univ. degli Studi di Firenze and ISTI-CNR, Italy) PAPER SUBMISSIONS - Submissions must be made electronically. Papers should be up to 16 pages in LNCS format, with the names and affiliations of the authors and a clear and informative abstract. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. All submissions must report on original research. Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any such
Re: [Hol-info] prove a goal in HOL4
liy_...@encs.concordia.ca wrote: I have to prove a goal in HOL4 as following: g `!a b c. (indep bern a c) /\ (indep bern b c) == (a IN events bern) /\ (b IN events bern) /\ (c IN events bern) /\ (prob bern (a INTER b INTER c) = prob bern (a INTER b) * prob bern c)`; Here, a and c are independant, also b and c are independant. However, a depends b. Could anybody give me some hints? I really appreciate! Regards, Liya I can't guess what bern and events mean, but if prob and indep have a usual meaning, then it's not true. eg let 3 coins, X, Y, Z be tossed independently. Let event A be coins X and Y fall the same way Let event B be coins X and Z fall the same way Let event C be coins Z and Y fall the same way Then each two of the three events A,B,C are independent. But A B is not independent of C (which is what, I understand, the last line of your conclusion says) Regards, Jeremy -- Download Intel#174; Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
