headers
Cezary Kaliszyk | 2 Feb 20:07
Picon

UITP'12: First Call for Papers

UITP'12: First Call for Papers

   [Apologies if you receive multiple copies]
   ------------------------------------------

         --- First  Call for Papers ---

         10th International Workshop on
 User Interfaces for Theorem Provers (UITP 2012)
 11.07.2012, Bremen, Germany, Part of CICM 2012

   http://www.informatik.uni-bremen.de/uitp12/

While interactive theorem provers have found many new application
areas in the last years, the system interfaces have often not
enjoyed the same attention as the proof engines themselves. In
many cases, interfaces remain relatively basic and
under-designed. More and more, this is becoming an obstacle for
the wider adoption of theorem proving technologies outside the
academic community.

The User Interfaces for Theorem Provers workshop series provides
a forum for researchers interested in improving human interaction
with interactive proof systems, be it theorem provers, formal
method tools, and other tools manipulating and presenting
mathematical formulas.

For the forthcoming 10th UITP workshop, we invite contributions
from the theorem proving, formal methods and tools, and HCI
communities, both to report on experience with existing systems,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Josef Urban | 21 Feb 19:13
Picon

FW: overlijden Dick de Bruijn

-------- Original Message --------
Subject: 	FW: overlijden Dick de Bruijn
Date: 	Mon, 20 Feb 2012 11:46:02 +0100
From: 	Geuvers, J.H. <J.H.Geuvers <at> tue.nl>
To: 	herman <at> cs.ru.nl <herman <at> cs.ru.nl>

-------------------------------------------
From: Secretariaat WIN
Sent: Monday, February 20, 2012 11:45:25 AM
To: Faculteit WIN
Subject: overlijden Dick de Bruijn
Importance: High
Auto forwarded by a Rule

/Dear colleagues,/

//

/On February 17, 2012, Prof.dr. N.G. de Bruijn passed away. /

/Dick de Bruijn was a full professor at our department from 1960 until
1984./

/His contributions to mathematics and computer science are among the
greatest of our department./

//

/More information about the cremation can be found in the attached
document./
(Continue reading)

Permalink | Reply | 0 comments |
headers
Adam Naumowicz | 22 Feb 06:34
Picon

CICM 2012 -- last call for papers (fwd)

---------- Forwarded message ----------
Date: Tue, 21 Feb 2012 21:47:05 +0100 (CET)
From: Makarius <makarius <at> sketis.net>
To: adamn <at> math.uwb.edu.pl
Subject: CICM 2012 -- last call for papers

    I am not sure if the subsequent CFP made it on the list as intended. The
    abstract deadline has passed already yesterday, but there is about one
    more week left for the main submission deadline.  Moreover, the PC
    chairs have agreed to be flexible to accomodate late submissions.

  	Makarius

---------- Forwarded message ----------
Date: Fri, 17 Feb 2012 11:15:14 +0100
From: Johan Jeuring <J.T.Jeuring <at> uu.nl>
To: om <at> openmath.org, om-announce <at> openmath.org, poplmark <at> lists.seas.upenn.edu,
      project-calculemus <at> lists.jacobs-university.de,
      project-latexml <at> lists.jacobs-university.de,
      projects-mkm-ig <at> jacobs-university.de,
      project-omdoc <at> lists.jacobs-university.de, proofpower <at> lemma-one.com,
      pvs <at> csl.sri.com
Subject: [MKM-IG] Conference on Intelligent Computer Mathematics,
      last call for papers

           CICM 2012 - Conference on Intelligent Computer Mathematics
             July 9-13, 2012 at Jacobs University, Bremen, Germany

                http://www.informatik.uni-bremen.de/cicm2012/
(Continue reading)

Permalink | Reply | 0 comments |
headers
Adam Grabowski | 22 Feb 09:13
Picon

New Mizar articles

   Dear All,
   together with the latest official version of the Mizar system
(7.13.01, MML version 4.181.1147) the following new Mizar articles
are available:

1133. ZMODUL01
      $\mathbb Z$-modules
       by Yuichi Futa, Hiroyuki Okazaki and Yasunari Shidama
      Received September 5, 2011
1134. MORPH_01
      Morphology for Image Processing, Part {I}
       by Hiroshi Yamazaki, Czes\l aw Byli\'nski and Katsumi Wasaki
      Received September 21, 2011
1135. NDIFF_4
      The Differentiable Functions from $\mathbbR$ into ${\mathbbR}^n$
       by Keiko Narita, Artur Korni\l owicz and Yasunari Shidama
      Received September 28, 2011
1136. MATRIX17
      Some Basic Properties of Some Special Matrices, Part {III}
       by Xiquan Liang and Tao Wang
      Received October 23, 2011
1137. INTEGR19
      Riemann Integral of Functions from $\mathbbbR$ into $n$-dimensional Real
      Normed Space
       by Keiichi Miyajima, Artur Korni{\l}owicz and Yasunari Shidama
      Received October 27, 2011
1138. EC_PF_2
      Operations of Points on Elliptic Curve in Projective Coordinates
       by Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima and Yasunari Shidama
      Received November 3, 2011
(Continue reading)

Permalink | Reply | 1 comment |
headers
Hugo Herbelin | 24 Feb 23:09
Picon
Picon
Favicon

ETAPS Workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)

     ** Workshop on Automation in Proof Assistants 2012 **

              a satellite workshop of ETAPS 2012
   jointly organized with the Rich-Model Toolkit COST action

         Sat 31 March - Sun 1 April, Tallinn, Estonia
         http://pauillac.inria.fr/~herbelin/aipa2012

       Regular registration fees end *** 26 February 2012 ***

** Invited speakers **

Jean-Christophe Filliâtre (U. Paris-Sud): Why3
Jasmin Blanchette (T.U. Munich): Sledgehammer, Quickcheck, and Nitpick
Chad E. Brown (U. Saarland): Satallax

** Contributing a talk **

The workshop will be informal. In addition to invited talks, the
workshop will be based on contributed talks and discussions. To
contribute a talk, send a title and abstract to aipa2012(at)inria.fr.

** Program committee **

Keijo Heljanko (Aalto University, IC0901 chair)
Hugo Herbelin (INRIA Paris-Rocquencourt, AIPA chair)
Viktor Kuncak (EPFL, Lausanne)
Adam Naumowicz (University of Białystok)
Claudio Sacerdoti (University of Bologna)
Makarius Wenzel (University Paris-Sud)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Makarius | 27 Feb 14:20

Call for papers: THedu'12

----------------------------------------------------------------------
                               CALL FOR PAPERS
----------------------------------------------------------------------
                                  THedu'12
                    TP components for educational software
                                 11 July 2012
                     http://www.uc.pt/en/congressos/thedu

                             Workshop at CICM 2012
                  Conferences on Intelligent Computer Mathematics
                                9-14. July 2012
                     Jacobs University, Bremen, Germany
              http://www.informatik.uni-bremen.de/cicm2012/cicm.php
----------------------------------------------------------------------

THedu'12 Scope
--------------

This workshop intends to gather the research communities for computer
Theorem proving (TP), Automated Theorem Proving (ATP), Interactive
Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS)
and Dynamic Geometry Systems (DGS). The workshop tries to combine and
focus systems of these areas to enhance existing educational software
as well as studying the design of the next generation of mechanised
mathematics assistants (MMA). Elements for next-generation MMA's
include:

    * Declarative Languages for Problem Solution: education in applied
      sciences and in engineering is mainly concerned with problems,
      which involve operations on elementary objects to be transformed
(Continue reading)

Permalink | Reply | 0 comments |
headers
Josef Urban | 27 Feb 17:20
Picon

lstlangmizar.sty

Hi,

at https://raw.github.com/JUrban/mizarmode/master/lstlangmizar.sty is
a basic LaTeX syntax highlighting mode for Mizar. Use it with Mizar
code in LaTeX like this:

\begin{lstlisting}[language=Mizar]
::$N Brouwer Fixed Point Theorem
theorem Th14:
  for r being non negative (real number), o being Point of TOP-REAL 2,
      f being continuous Function of Tdisk(o,r), Tdisk(o,r)
  holds f has_a_fixpoint
proof ...
\end{lstlisting}

Josef
Permalink | Reply | 0 comments |

Gmane