Robert White | 21 May 22:05 2015
Picon

(no subject)

Dear all,

I wonder if there is better way to handle proofs like (((A==>B)==> C)==> D)==> E (in top-down proofs, I also wonder how I should do it in bottom up proofs), 

After doing a UNDISCH, all the A...D will go to the hypothesis part. I understand that in natural deduction, we don't do much on the hypothesis side. So apart from doing MP to get:

K ==> (((A==>B)==> C)==> D)==> E       K
---------------------------------------------------------- UNDISCH
(((A==>B)==> C)==> D)==> E   


--

Regards,
Robert White (Shuai Wang)
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Robert White | 21 May 15:18 2015
Picon

Intuitionistic basic_rewrites?

Hello again,

I understand that HOL is a reasoner for classical logic so there is no surprise when I want to prove something using rewriting I get a set of rules as basic_rewrites where we can find ~ ~t <=> t; there.

So here comes the question, is there a way we can get intuitionistic set or rewriting rules in HOL Light already to do pure constructive logic reasoning?

Thanks again.

-- 

Regards,
Robert White (Shuai Wang)
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Robert White | 21 May 14:00 2015
Picon

EQ_MP as a TAC?

Dear all,


I wonder if there is a way I can use TAC for EQ_MP.

I'm sorry I'm not very familiar with bottom up proofs.
A1 |- t1 <=> t2 A2 |- t1' ----------------------------- EQ_MP A1 u A2 |- t2

Thanks!
--

Regards,
Robert
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Robert White | 21 May 13:39 2015
Picon

Question about rewriting in proofs

Dear all,

Happy proving :)

1) I wonder how I suppose to tackle situation like this
A, B, C |- D. 
and D is a complicated term with D1 and D2 somewhere in it.

D1 can be rewrite to D1' under assumption of A,B,C while if I simply use the ASM_REWRITE_RULE  then I will do some other changes in D which I don't want to.

2) Another related question: is there any way I can deal with situation like 
A, B, C |- D but I want to replace C by C' where C = C'
one way in my mind is to get 
A, B |- C ==> D then use rewrite to get C' ==> D as concl but, that may lead to the change in D as well.

It would be very nice if you can give me some advice.

Thanks very much!

--

Regards,
Robert
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
fabio.zanasi | 19 May 15:16 2015
Picon
Picon

MFPS XXXI/CALCO 2015 : Call for Participation


>From June 22, in a galaxy far, far away... https://coalg.org/calco15/images/poster.jpg

=========================================================

          JOINT CALL FOR PARTICIPATION  

                      MFPS XXXI

31st Conference on the Mathematical Foundations of Programming Semantics

                 June 22 - 25, 2015

     http://events.cs.bham.ac.uk/mfps31/

		     CALCO 2015

6th International Conference on Algebra and Coalgebra in Computer Science

                 June 24 - 26, 2015

               http://coalg.org/calco15/

          In cooperation with ACM SIGLOG

                Nijmegen, Netherlands

==========================================================

       Early registration deadline:    June 14, 2015

==========================================================

-- SCOPE --

MFPS conferences are devoted to those areas of mathematics, logic,
and computer science that are related to models of computation, in
general, and to the semantics of programming languages, in
particular. The series has particularly stressed providing a forum
where researchers in mathematics and computer science can meet and
exchange ideas about problems of common interest. As the series also
strives to maintain breadth in its scope, the conference strongly
encourages participation by researchers in neighbouring areas.

CALCO aims to bring together researchers and practitioners with
interests in foundational aspects, and both traditional and emerging
uses of algebra and coalgebra in computer science.
It is a high-level, bi-annual conference formed by joining the forces
and reputations of CMCS (the International Workshop on Coalgebraic
Methods in Computer Science), and WADT (the Workshop on Algebraic
Development Techniques). Previous CALCO editions took place in
Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009),
Winchester (UK, 2011) and Warsaw (Poland, 2013).

-- INVITED SPEAKERS --

Invited speaker of MFPS and CALCO

* Andy Pitts - University of Cambridge, UK

MFPS invited speakers

* Thierry Coquand - Chalmers University of Technology, Sweden
* Paul B. Levy - University of Birmingham, UK
* Guy McCusker - University of Bath, UK
* Sam Staton - Radboud University, Nijmegen, NL

CALCO invited speakers

* Chris Heunen - University of Oxford, UK
* Matteo Mio - CNRS, ENS Lyon, FR
* Daniela Petrisan - Radboud University, Nijmegen, NL

-- PROGRAMME AND SATELLITE EVENTS --

The detailed programme will appear soon on the conference web sites:

http://events.cs.bham.ac.uk/mfps31/ (MFPS)    https://coalg.org/calco15/  (CALCO)

*MFPS special sessions*

MFPS will host four special sessions:

* Game semantics, organised by Andrzej Murawski, Warwick
* Concurrent separation logic, organised by Philippa Gardner, Imperial College
* Nominal techniques, organised by Daniela Petrisan, Radboud
* Algebraic effects, organised by Matija Pretnar, Ljubljana

The special session will include an invited tutorial talk, delivered by the session
organiser.

*CALCO Early Ideas workshop*

CALCO 2015 will run together with the CALCO Early Ideas Workshop, with 
dedicated Early Ideas sessions at the end of each conference day. Additional 
information is available at https://coalg.org/calco15/ei.html .

-- REGISTRATION --

To register for MFPS/CALCO, please fill out the registration form available at

https://limesurvey.science.ru.nl/index.php/118286/lang-en .

The following registration Fees are applied.

                                Normal     Late
Both MFPS and Calco		
  Non-Students        €230	€250
  Students	          €160	   €180
MFPS only or Calco only		
  Non-Students        €160	€180
  Students	          €100	   €120

SIGLOG members attending MFPS and/or Calco receive a discount on the registration fee: 
€20 for student members, and €30 for professional members. The yearly rate for SIGLOG 
membership is $15 for students, and $25 for professionals.

The deadline for normal registration is Sunday, June 14. After this date, the
 late registration fee will be applied. The registration fee can be paid by bank
 transfer or by credit card (Visa or Mastercard). Payment by bank transfer is 
strongly encouraged. Within the SEPA area, bank transfers are free of change. 

We will be sponsoring 5 free student registrations. Anyone interested please 
contact alexandra <at> cs.ru.nl. 
We are also proud to be a family-friendly conference: any participant who requires
 support for childcare to be able to attend the conference should contact us. 

Additional information on registration and hotel information can be found at

http://mfpscalco2015.cs.ru.nl/ .

-- LOCATION --

Nijmegen is the oldest city in the Netherlands and celebrated its
2,000th year of existence in 2005. It is situated in the eastern
province of Gelderland, quite near to the German border. The latin
name for Nijmegen, `Noviomagus´, is a reminder of its Roman past.
`Noviomagus´ means `new market´ and refers to the right to hold a
market as granted by the Romans. In the days of Charlemagne, the
city was called `Numaga´; later on, this became `Nieumeghen´ and
`Nimmegen´. However, citizens born and bred in Nijmegen speak
affectionately of `Nimwegen´.

Nijmegen is one of the warmest cities of the Netherlands, especially
during summer, when the highest temperatures in the country are
usually measured in the triangle Roermond – Nijmegen – Eindhoven.
The lack of north-south oriented mountain ranges in Europe make this
area prone to sudden shifts in weather, giving the region a
semi-continental climate.

Conference venue for MFPS/CALCO is the majestic *Art Cinema Lux* 
(http://lux-nijmegen.nl/), located in the city center of Nijmegen.

-- SIGLOG Anti-harassment Policy --

The open exchange of ideas and the freedom of thought and expression
are central to the values and goals of SIGLOG. They require an
environment that recognizes the inherent worth of every person and
group. They flourish in communities that foster mutual understanding
and embrace diversity. For these reasons, SIGLOG is committed to
providing a harassment-free conference experience, and implements the ACM
policy against harassment (see http://www.acm.org/sigs/volunteer_resources/officers_manual/anti-harassment-policy).

Conference participants violating these standards may be sanctioned or
expelled from the meeting, at the discretion of the conference
organizers. Conference organizers are requested to report serious
incidents to the SIGLOG Chair.

=========================================================

------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Clark Barrett | 20 May 21:03 2015
Picon

Deadline extended: 2015 SAT/SMT Summer School

Our apologies if you receive multiple copies of this email. We kindly ask you
to forward this email to interested students and postdoctoral researchers.

========================================================

                     SECOND CALL FOR PARTICIPATION

                 Fifth International SAT/SMT Summer School

                         Stanford, CA, July 15-17, 2015

                        http://smt2015.csl.sri.com/school

========================================================

APPLICATION:

The application deadline for the summer school has been extended to
May 26, 2015.  Full details
of the application procedure are available on the summer school website
(http://smt2015.csl.sri.com/school).

ABOUT:

Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers have
become the engines powering numerous applications in computer science and
beyond, including automated verification, artificial intelligence, program
synthesis, security, product configuration, and many more. The summer school
covers the foundational and practical aspects of SAT and SMT technologies and
their applications.

Besides providing a well-structured introduction to SAT and SMT, this year’s
edition of the SAT/SMT Summer School covers timely topics and novel
applications such as

- MaxSAT
- solvers for floating point arithmetic,
- optimization modulo theories,
- symbolic execution
- proofs and interpolation,
- synthesis

The fifth edition follows the schools that took place at MIT (2011), at
Fondazione Bruno Kessler in Trento, Italy (2012), at Aalto University in Espoo,
Finland (2013), and in Semmering, Austria (2014).  The school location and
schedule has been chosen to conveniently allow participants to also attend the
2015 SMT Workshop and CAV conference:

- SMT Workshop: http://smt2015.csl.sri.com/
- CAV Conference: http://i-cav.org/2015/

The Summer School program will feature four lectures per day including an
introductory lecture on day one by Donald Knuth.

Wednesday, July 15, 2015

  9:00 - 10:30 Donald Knuth
 10:30 - 11:00 Break
 11:00 - 12:00 Nina Narodystka
 12:00 -  1:00 Lunch
  1:00 -  2:30 Alberto Griggio
  2:30 -  3:00 Break
  3:00 -  4:00 Dejan Jovanović

Thursday, July 16, 2015

  9:00 - 10:30 Mate Soos
 10:30 - 11:00 Break
 11:00 - 12:00 Christoph Wintersteiger
 12:00 -  1:00 Lunch
  1:00 -  2:30 Roberto Sebastiani
  2:30 -  3:00 Break
  3:00 -  4:00 Joe Hendrix

Friday, July 17, 2015

  9:00 - 10:30 Pascal Fontaine
 10:30 - 11:00 Break
 11:00 - 12:00 Stefano Ermon
 12:00 -  1:00 Lunch
  1:00 -  2:30 Sanjit Seshia
  2:30 -  3:00 Break
  3:00 -  4:00 Vijay D'Silva

Organizers:

Clark Barrett (New York University)
David Dill (Stanford University)
Bruno Dutertre (SRI International)

------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Geoff Sutcliffe | 19 May 15:58 2015
Picon

LPAR-20 in Fiji - Call for Papers and Workshops


                The 20th International Conference on
    Logic for Programming, Artificial Intelligence and Reasoning
                             LPAR-20

               University of the Pacific, Suva, Fiji
                       http://www.LPAR-20.org

                    CALL FOR PAPERS AND WORKSHOPS

The series of International Conferences on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR) is a forum where, year after year, some of
the most renowned researchers in the areas of logic, automated reasoning,
computational logic, programming languages and their applications come to
present cutting-edge results, to discuss advances in these fields, and to
exchange ideas in a scientifically emerging part of the world. The 20th LPAR
will be held at the University of the South Pacific, Suva, Fiji in 2015
(see dates below).

== Topics

New results in the fields of computational logic and applications are welcome.
Also welcome are more exploratory presentations, which may examine open
questions and raise fundamental concerns about existing theories and practices.

Topics of interest include, but are not limited to:
+ Abduction and interpolation methods
+ Automated reasoning
+ Constraint programming
+ Decision procedures
+ Description logics
+ Foundations of security
+ Hardware verification
+ Implementations of logic
+ Interactive theorem proving
+ Knowledge representation and reasoning
+ Logic and computational complexity
+ Logic and databases
+ Logic and games
+ Logic and machine learning
+ Logic and the web
+ Logic and types
+ Logic in artificial intelligence
+ Logic of distributed systems
+ Logic programming
+ Logical aspects of concurrency
+ Logical foundations of programming
+ Modal and temporal logics
+ Model checking
+ Non-monotonic reasoning
+ Ontologies and large knowledge bases
+ Probabilistic and fuzzy reasoning
+ Program analysis
+ Rewriting
+ Satisfiability checking
+ Satisfiability modulo theories
+ Software verification
+ Specification using logic
+ Unification theory

== Submission Details

Submissions of two kinds are welcome:

- Regular papers  that describe solid new research results. They can be up to
  15 pages long in LNCS style, including figures and references, but excluding
  appendices (that reviewers are not required to read).

- Experimental and tool papers that describe implementations of systems, report
  experiments with implemented systems, or compare implemented systems. They
  can be up to 8 pages long in the LNCS style.

Both types of papers must be electronically submitted in PDF via EasyChair:
https://easychair.org/conferences/?conf=lpar20

== Participation

Prospective authors are required to register a title and an abstract a week
before the paper submission deadline (see below). Authors of accepted papers 
are required to ensure that at least one of them will be present at the 
conference. More details about the venue and organisation can be found on the
conference website.

== Important Dates

Abstract Submission: 30 June
Paper Submission: 7 July
Notification: 23 August
Workshops: 23 November
Conference: 24-28 November

== Programme Committee

Cyrille Valentin 	Artho 	AIST, Japan
Franz Baader 		TU Dresden, Germany
Christel Baier 		TU Dresden, Germany
Peter Baumgartner 	NICTA, Australia
Armin Biere 		Johannes Kepler University, Austria
Nikolaj Bjorner 	Microsoft Research, USA
Lei Bu 	Nanjing 	University, China
Franck Cassez 		Macquarie University, Australia
Ansgar Fehnker 		University of the South Pacific
Rajeev Gore 		Australian National University, Australia
Tim Griffin 	 	University of Cambridge, UK
Ralf Huuck 			NICTA and UNSW, Australia
Kim Guldstrand Larsen 	Aalborg University, Denmark
Dejan Jovanovic 	SRI International, USA
Gerwin Klein 		NICTA and UNSW, Australia
Dexter Kozen 		Cornell University, USA
Rustan Leino 		Microsoft Research, USA
Joe Leslie-Hurd 	Intel Corporation, USA
Annabelle McIver 	Macquarie University, USA
Kenneth McMillan 	Microsoft Research, USA
Marius Minea 		Politehnica University of Timisoara, Romania
Matteo Mio 			CNRS, ENS Lyon, France
Prakash Panangaden 	McGill University, Canada
Christine Paulin-Mohring 	Universit=C3=A9 Paris-Sud, France
Andreas Podelski 	University of Freiburg, Germany
Geoff Sutcliffe 	University of Miami, USA
Gancho Vachkov 		The University of the south Pacific (USP), Fiji
Ron Van Der Meyden 	UNSW, Australia
Tomas Vojnar 		Brno University of Technology, Czech Republic
Andrei Voronkov 	University of Manchester, UK
Toby Walsh 			NICTA and UNSW, Australia
More to be announced ...

                          CALL FOR WORKSHOPS

LPAR-20 workshops will be held either as one-day or half-day events. If you
would like to propose a workshop for LPAR-20, please contact the workshop
chair via email (Peter.Baumgartner <at> nicta.com.au), by the proposal deadline.

== Proposals

To help planning, workshop proposals should contain the following data:

- Name of the workshop.
- Brief description of the workshop, including workshop topics.
- Valid web address of the workshop.
- Contact information of the workshop organizers.
- An estimate of the audience size.
- Proposed format of the workshop (for example, regular talks, tool demos,
  poster presentations, etc.).
- Duration of the workshop (one-day or half-day).
- Potential invited speakers (if any).
- Procedures for selecting papers and participants.
- Special technical or AV needs.

== Important dates

Workshop proposals submission deadline:     May 15, 2015
Notification of acceptance:                June  1, 2015
Workshops:                             November 23, 2015

------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
Ramana Kumar | 19 May 16:09 2015
Picon
Picon

HOL Workshop 2015

                  SECOND CALL FOR ABSTRACTS

             2015 International Workshop on HOL4
               The HOL Theorem Proving System
                         (HOL'15)
                     hosted by CADE-25
               August 2-3, 2015, Berlin, Germany

            https://www.cl.cam.ac.uk/~rk436/hol15/

The deadline for expressions of interest to present an idea at the workshop is
next month! I encourage and welcome anyone who has any interest in HOL4 to
submit something. The original call for abstract follows.

IMPORTANT DATES

Abstract Submission     15th June 2015
Author Notification      1st July 2015

INVITED SPEAKER

HOL4's lead developer, Michael Norrish, will speak at the workshop.

THEME

The theme of the workshop is "the development agenda". We hope to gather
both users and developers of HOL4 to brainstorm and decide:
  - What tasks or projects (from small to large scale) should we prioritise
    for HOL4's continued development?
  - How can we apply the latest developments in the fields of automated and
    interactive theorem proving back to HOL4, and is it worth it?
  - Should HOL4 merge with or evolve into another system?
  - How might we increase the amount of developer time put into the system
    (e.g., attracting new users, holding more workshops)?

Being co-located with CADE, we also intend the workshop to be
beginner-friendly with the possibility of some tutorial introductions, and
we hope to focus some of the time on integrating ATP with ITP.

Specific development ideas can be found on the workshop website:
  https://www.cl.cam.ac.uk/~rk436/hol15/

ABSTRACT SUBMISSION

To register your interest in discussing the development agenda, please
submit a short abstract describing what you want to do and how long you
would like to have the floor (from 5 through 30 minutes). There will be
flexibility for impromptu talks and discussion, but we highly encourage
early submissions to give priority to better-prepared work.

Submission is via EasyChair:
  https://easychair.org/conferences/?conf=hol15

ABOUT

HOL4 is the latest incarnation of the original theorem prover for
Higher-Order Logic, and is still a popular choice for programming
tactics and proof automation, and developing formal theories.
Continuing the workshop series started last year, we invite everyone
interested in the use and development of HOL4 to participate in this
year's workshop dedicated to improving both the tool itself and the
breadth of knowledge spread across its community of users.
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
fghassemi | 17 May 08:34 2015
Picon

Call for papers - The First IFIP International Conference on Topics in Theoretical Computer Science (TTCS 2015)

  *** Apologies for multiple copies ***

Call for paper

 

Topics in Theoretical Computer Science (TTCS 2015)
http://www.ttcs.ir/

Institute for Research in Fundamental Sciences (IPM), Tehran, Iran
August 26-28, 2015

 



*Extended Submission Deadline:* May 22, 2015

 


========================================

Scope
------------------------------

TTCS is a new bi-annual conference series, intending to serve as a forum for novel and high-quality research in all areas of theoretical computer science, foundations of software engineering and programming languages. The conference is held in cooperation with the European Association for Theoretical Computer Science.

There will be a number of satellite events at TTCS, These will feature
presentation of early research results, and position papers. There will
also be a forum for Ph.D. students to receive comments about their ongoing
research projects.

Topics of interest include but are not limited to:

   - algebra and co-algebra in computer science,
   - algorithms and data structures,
   - algorithmic coding theory,
   - algorithmic graph theory and combinatorics,
   - approximation algorithms,
   - computational complexity,
   - computational geometry,
   - computational learning theory,
   - concurrency theory,
   - coordination languages,
   - economics and algorithmic game theory,
   - fixed parameter algorithms,
   - formal verification and model-based testing,
   - logic in computer science,
   - machine learning
   - methods, models of computation and reasoning for embedded, hybrid, and
   cyber-physical systems,
   - optimization,
   - parallel and distributed algorithms,
   - quantum computing,
   - randomness in computing,
   - stochastic and probabilistic specification and reasoning
   - theoretical aspects of other CS-related research areas, e.g.,
   computational science, databases, information retrieval, and networking,
   - theoretical cryptography,
   - theory of programming languages, and
   - type theory and its application in program verification.

Keynote Speakers
------------------------------

Anuj Dawar, Cambridge University, UK
Michael Fellows, Charles Darwin University, Australia
Mehrnoosh Sadrezadeh, Queen Mary University of London, UK

Submission
------------------------------

For the main conference, we solicit research papers in all areas of
theoretical computer science. All papers will undergo a rigorous review
process and will be judged based on their originality, soundness,
significance of the results, and relevance to the theme of the conference.

Papers should be written in English. Research papers should not exceed 15
pages in the LNCS style format. Multiple and/or concurrent submission to
other scientific venues is not allowed and will result in rejection as well
as notification to the other venue. Any case of plagiarism (including
self-plagiarism from earlier publications) will result in rejection as well
as notification to the the authors' institutions.

Papers should be submitted through our EasyChair submission website:
https://www.easychair.org/conferences/?conf=ttcs2015 . The web site is open
for submissions.

Important Dates
------------------------------

   - *Paper Submission:* May 22, 2015 (Extended, Anywhwere on Earth)
   - *Author notification:* June 26, 2015
   - *Camera ready paper due:* July 10, 2015
   - *Conference:* August 26-28, 2015

Program Committee
------------------------------
*Track A: Algorithms and Complexity*

   - Mohammad Ali Abam, Sharif University of Technology, Iran
   - Saeed Akbari, Sharif University of Technology, Iran
   - Saeed Alaei, Cornell University, USA
   - Mohammad Hossein Bateni, Google Research, USA
   - Salman Beigi, IPM, Iran
   - Amir Daneshgar, Sharif University of Technology, Iran
   - Fedor Fomin, University of Bergen, Norway
   - Ali Ghodsi, University of Waterloo, Canada
   - Mohammad Ghodsi, Sharif University of Technology, Iran
   - Mohammad T. Hajiaghayi, University of Maryland, USA (Chair)
   - Amin Karbasi, Yale University, USA
   - Nicole Immorlica, Microsoft Research, USA
   - Amit Kumar, IIT Delhi, India
   - Mohammad Mahdian, Google Research, USA
   - Hamid Mahini, University of Maryland, USA
   - Bojan Mohar, Simon Fraser University, Canada
   - Mohammad Mahmoody, University of Virginia, USA
   - Vahab Mirrokni, Google Research, USA
   - Morteza Monemizadeh, Frankfurt University, Germany
   - Shayan Oveisgharan, UC Berkeley and University of Washington, USA
   - Debmalya Panigrahi, Duke University, USA
   - Jorg Sack, Carleton University, Canada
   - Mohit Singh, Microsoft Research, USA
   - Dimitrios M. Thilikos, CNRS, France and University of Athens, Greece
   - Suresh Venkatasubramanian, University of Utah, USA
   - Jan Vondrak, IBM Almaden Research Center, USA

*Track B: Logic, Semantics, and Programming Theory*

   - Farhad Arbab, CWI and Leiden University, The Netherlands
   - S. Arun-Kumar, IIT Delhi, India
   - Ilaria Castellani, INRIA Sophia Antipolis, France
   - Dave Clarke, Uppsala University, Sweden and KU Leuven, Belgium
   - Pieter Cuijpers, Eindhoven University of Technology, The Netherlands
   - Fatemeh Ghassemi, Tehran University, Iran
   - Matthew Hennessy, Trinity College Dublin, Ireland
   - Ichiro Hasuo, University of Tokyo, Japan
   - Mahdi Jaghoori, AMC University of Amsterdam, The Netherlands
   - Jeroen Keiren, Vrije Universiteit Amsterdam, The Netherlands
   - Bas Luttik, Eindhoven University of Technology, The Netherlands
   - Jose Meseguer, University of Illinois at Urbana, USA
   - Lary Moss, Indiana University, USA
   - Mohammad Mousavi, Halmstad University, Sweden (Chair)
   - Jun Pang, University of Luxembourg, Luxembourg
   - Gerardo Schneider, Gothenburg University and Chalmers, Sweden
   - Marjan Sirjani, Reykjavik University, Iceland
   - Walter Vogler, Augsburg University, Germany
   - Tim Willemse, Eindhoven University of Technology, The Netherlands

 
 
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
"Mark" | 18 May 17:06 2015

Re: Question about proof of law of excluded middle.

Hello Robert,

If you're interested in the proof itself, rather than how in how the HOL
Light one works, then there's also a proof in HOL Zero which could help.
This follows the same idea but is a "forwards proof" in terms of basic
inference rule steps rather than tactics, but might (or might not..) be more
understandable.  Download the HOL Zero source distribution from:
    http://www.proof-technologies.com/holzero/

Best,
Mark.

on 15/5/15 11:22 PM, Robert White <ai.robert.wangshuai <at> gmail.com> wrote:

> Dear Sir/Madam,
>
> I wonder if you could explain a bit of the last step of the proof of law
of
> excluded middle (in the file class.ml). I am not sure how the rewriting
> magically converted
>
> 0 [`F <=> ( <at> x. (x <=> F) \/ t)`]
> 1 [`T <=> ( <at> x. (x <=> T) \/ t)`]
> 2 [`t`]
>
> `~(( <at> x. (x <=> T) \/ t) <=> ( <at> x. (x <=> F) \/ t)) ==> ( <at> x. (x <=> F) \/
t)`
>
> to `t \/ ~t`
>
> The proof is as follows:
>
> let EXCLUDED_MIDDLE = prove
> (`!t. t \/ ~t`,
> GEN_TAC THEN SUBGOAL_THEN
> `((( <at> x. (x <=> F) \/ t) <=> F) \/ t) /\ ((( <at> x. (x <=> T) \/ t) <=> T) \/
> t)`
> MP_TAC THENL
> [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL
> [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN
> DISJ1_TAC THEN REFL_TAC;
> DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
> TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN
> DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN
> PURE_ONCE_ASM_REWRITE_TAC[] THEN
> *    ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;*
>
> PS: Is there a way I can print out how it is done step by step form OCaml
> Toplevel?
>
> Thanks very much!
> --
>
> Regards,
> Robert
>
>
>
> ----------------------------------------
>
>
----------------------------------------------------------------------------
> --
> One dashboard for servers and applications across Physical-Virtual-Cloud
> Widest out-of-the-box monitoring support with 50+ applications
> Performance metrics, stats and reports that give you Actionable Insights
> Deep dive visibility with transaction tracing using APM Insight.
> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
>
>
> ----------------------------------------
> _______________________________________________
> hol-info mailing list
> hol-info <at> lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>

------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
Robert White | 15 May 18:58 2015
Picon

Question about proof of law of excluded middle.


Dear Sir/Madam,

I wonder if you could explain a bit of the last step of the proof of law of excluded middle (in the file class.ml). I am not sure how the rewriting magically converted

 0 [`F <=> ( <at> x. (x <=> F) \/ t)`]
 1 [`T <=> ( <at> x. (x <=> T) \/ t)`]
 2 [`t`]


`~(( <at> x. (x <=> T) \/ t) <=> ( <at> x. (x <=> F) \/ t)) ==> ( <at> x. (x <=> F) \/ t)`

to `t \/ ~t`

The proof is as follows:


let EXCLUDED_MIDDLE = prove
 (`!t. t \/ ~t`,
  GEN_TAC THEN SUBGOAL_THEN
   `((( <at> x. (x <=> F) \/ t) <=> F) \/ t) /\ ((( <at> x. (x <=> T) \/ t) <=> T) \/ t)`
  MP_TAC THENL
   [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL
     [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN
    DISJ1_TAC THEN REFL_TAC;
    DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
    TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN
    DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN
    PURE_ONCE_ASM_REWRITE_TAC[] THEN
    ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;

PS: Is there a way I can print out how it is done step by step form OCaml Toplevel?

Thanks very much!
--

Regards,
Robert
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane