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,

2nd announcement: 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

       Early registration before *** 29 January 2012 ***

Though proof assistants such as Agda, Coq, Isabelle, Matita, Mizar,
Twelf, but also ACL2, HOL-Light, HOL4, PVS and many others are
characterized as interactive theorem provers, automation is largely
present under different forms in them, and at the same time probably
not as present as what one would like. The purpose of this workshop is
to gather people working on all different aspects of automation
relevant for interactive theorem proving, starting with the following
topics:

* decision procedures on specific domains
* connecting interactive and automated theorem provers
* combination of decision procedures
* reflection techniques
* unification techniques and heuristics
* rewriting techniques and heuristics
* automatic termination checking
* program synthesis

At least the first day of the workshop (Saturday 31 March) is
organized in coordination with the COST Action IC0901 Rich-Model

reductions in Mizar

Hello,

in Mizar version 7.12.02, which will be issued officially soon,
a new mechanism, called reductions, has been implemented.

Reductions are an attempt to increase power of the Mizar checker.

Syntax is:

registration
   let x_1,...,x_n;
   reduce term1(x_1,...,x_n) to term2(x_1,...,x_n);
   reducibility
   proof
     thus term1(x_1,...,x_n) = term2(x_1,...,x_n);
   end;
end;

where term2 has to be a _subterm_ of term1. This restriction is a result 
of a Mizar principle, that the system does not generate new terms itself 
(with very few exceptions).

Correctness condition to be proved is "reducibility".

Examples of reductions are:

reduce X \/ {} to X

reduce union {} to {}

MML Query and cscope

Dear all,

time ago when I programmed I used a tool called cscope. I basically used
just two functions: the first was to 'jump' to the text defining a function
of a given name, the second was to get all the definitions of the functions
that used a given function.
Now, in mathematics, I still want to do these two base operations: 1.
jumping, which is already available from the html interface of a Mizar
article, and 2. the inverse of jump. (you could call them 'zooming in' and
'zooming out')

Then the MML Query question is: given a constructor/substring/theorem X how
can I get the list of all theorems that 'use' X?

For example, I have the notion of simple group, how can I get the list of
all theorems in the library regarding simple groups?

I read the MML Query examples documentation, but it is really too abstruse
(I am not a real mizar user, but I have seen that MML is quite readable if
you already know what you are reading).

So, could you give me some MML Query expressions to solve the matter?

Many thanks.

Best regards,
Andrea
--

-- 
View this message in context: http://old.nabble.com/MML-Query-and-cscope-tp32998572p32998572.html

Invitation to connect on LinkedIn

Announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)

     ** Workshop on Automation in Proof Assistants 2012 **
              a satellite workshop of ETAPS 2012
         Sat 31 March - Sun 1 April, Tallinn, Estonia
         http://pauillac.inria.fr/~herbelin/aipa2012

Though proof assistants such as Agda, Coq, Isabelle, Matita, Mizar,
Twelf, but also ACL2, HOL-Light, HOL4, PVS and many others are
characterized as interactive theorem provers, automation is largely
present under different forms in them, and at the same time probably
not as present as what one would like. The purpose of this workshop is
to gather people working on all different aspects of automation
relevant for interactive theorem proving, starting with the following
topics:

* decision procedures on specific domains
* connecting interactive and automated theorem provers
* combination of decision procedures
* reflection techniques
* unification techniques and heuristics
* rewriting techniques and heuristics
* automatic termination checking
* program synthesis

The first day of the workshop (Saturday 31 March) is organized in
coordination with the COST Action IC0901 Rich-Model Toolkit
(http://richmodels.org) which explores how to make automated reasoning
applicable to a wider range of problems.

** 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
by ** March 5, 2012 **.

** Post-workshop proceedings **

It is planned to edit afterward a special journal issue collecting
selected papers on the topic of the workshop.

** 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)

2011 - Mizar Prize for Young Researchers

I have the pleasure to announce that the winner of the
"Mizar Prize for Young Researchers" in 2011
is Marco Caminati from Italy, for his Mizar article
"Sequent calculus, derivability, provability.
  Goedel's completeness theorem" (MML identifier: FOMODEL4).

Value of Prize:  1.000 Euro.

The prize was founded in 2009 by Prof. Krystyna Kuperberg
(Auburn University).

dr Roman Matuszewski
http://mizar.org/people/romat/

Chairman of the Prize
ASSOCIATION OF MIZAR USERS

Error No 9

Dear All,
I have suddenly met such an error message:

environ
  vocabularies ZFMISC_1, PRE_TOPC, EUCLID;
  constructors ZFMISC_1, PRE_TOPC, EUCLID;
  notations ZFMISC_1, PRE_TOPC, EUCLID;
  theorems ZFMISC_1;
  registrations MEMBERED;
  requirements SUBSET, NUMERALS;
begin
  reserve A, B, C for Point of (TOP-REAL 2), x, y, z for set;

  A, B, C are_mutually_different implies C, B, A are_mutually_different
  by ZFMISC_1:def 5;
::>,9,9
  A, B, C are_mutually_different implies C, B, A are_mutually_different
  proof
    assume A, B, C are_mutually_different;
    then A <> B & A <> C & B <> C by ZFMISC_1:def 5;
    hence C, B, A are_mutually_different by ZFMISC_1:def 5;
  end;
  x, y, z are_mutually_different implies z, y, x are_mutually_different
  by ZFMISC_1:def 5;
::>,4
::> 4: This inference is not accepted
::> 9: Too many instantiations

From the last line of this article it's obvious that even without
error No9 the first statement won't be accepted by checker. But I'm
curious about the nature of this error. How instantiations are counted
and what is their maximal number?

--
Yours,
Boris.

What does this 'attr c1 is strict' convention mean?

proof objects for mizar: already available?

There are two senses in which mizar already has proof objects, despite
appearances to the contrary.  However, both senses are unsatisfactory.

(a) One could argue that there's no difference between "proof object"
     and "mizar article", because the proof is contained right there in
     a mizar text.  That is, of course, correct.  But this is
     unsatisfactory because one must have the mizar infrastructure to
     work with the proof object.  Of course, with some mathematical and
     logical background one can read a mizar text in the same sense
     that one reads a book, but doing anything interesting requires the
     mizar tools.  (Moreover, as we all know, in general, owing to the
     evolving syntax and library, an article might even require a
     specific *version* of the mizar toolset.)  But proof objects
     shouldn't really depend on the version of mizar that was used to
     generate them.  They shouldn't even depend on mizar itself.  One
     should be able to inspect and work with a mizar object, in
     principle, independently of mizar.

(b) Proofs objects are already available, in some sense, for mizar
     proofs.  They do not give precisely what is wanted from the
     concept of proof object, though:

     * They are not always available.  With the current transformation
       into a vanilla first-order format, and with current ATPs, for
       less than half of mizar theorems from the library do we have
       deductions.  This is clearly an important result for the
       community, but not having deductions is a serious shortcoming.
       We want proof objects for all mizar proofs.

     * The calculi of the proofs that are found this way depend on the
       theorem prover employed.  One finds proofs in the superposition
       calculi, resolution calculi... The plurality of proof calculi is
       welcome -- we want to view mizar proof objects through various
       formal lenses -- but none of these is satisfactory because none
       is a natural deduction proof in the style of mizar.  (To some
       extent this problem can be overcome: an ATP could either do
       search in a natural deduction setting, or emit natural
       deductions by translating whatever calculus it uses into natural
       deduction.  But proof search in natural deduction is generally
       not as efficient as search in other calculi.  And the
       translation from other calculi to a natural deduction is not
       always clear.)  What is wanted from proof objects for mizar is a
       sort of natural deduction proof that adheres more or less to the
       mizar format, but which brings out all logical details.  It is
       unpleasant and awkward to switch from natural deduction-style
       mizar proofs to unnatural resolution deductions.

     * There is no assurance that the proofs discovered by an ATP
       thanks to Josef's translations are the same as the mizar proofs
       with which one started.  Genuinely new proofs can be (and are)
       discovered.  An ATP might exploit a premise or combination of
       premises in an unusual way that diverges from the input mizar
       proof.  An even when the ATP-discovered proof is more or less
       congruent to the mizar proof from which it came, because it is
       expressed in a different formal calculus there might be some
       uncertainty about whether we are looking at the same proof.

     * By diverging from mizar's natural deduction format, one loses
       the ability to carry out experiments and investigations that
       require that one works with natural deductions.  Thus, one might
       wish to investigate the notion of obviousness.  One might ask,
       for example, what instances of which universal formulas were
       used to carry out a particular by step.  One might wish to carry
       out certain transformations of the the deduction (e.g., rewrite
       a natural deduction by represent applications of definitions as
       rules of inference, rather than as applications of the rule of
       modus ponens).

--

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/

New Mizar articles

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

1113. MAZURULM
      Mazur-Ulam Theorem
       by Artur Korni{\l}owicz
      Received December 21, 2010
1114. EC_PF_1
      Set of Points on Elliptic Curve in Projective Coordinates
       by Yuichi Futa, Hiroyuki Okazaki and Yasunari Shidama
      Received December 21, 2010
1115. RLAFFIN3
      Continuity of Barycentric Coordinates in Euclidean Topological Spaces
       by Karol P\kak
      Received December 21, 2010
1116. SIMPLEX2
      Brouwer Fixed Point Theorem for Simplexes
       by Karol P\kak
      Received December 21, 2010
1117. BROUWER2
      Brouwer Fixed Point Theorem in the General Case
       by Karol P\kak
      Received December 21, 2010
1118. FOMODEL0
      Preliminaries to Classical First-order Model Theory
       by Marco B. Caminati
      Received December 29, 2010
1119. FOMODEL1
      Definition of first order language with arbitrary alphabet. Syntax of
      terms, atomic formulas and their subterms.
       by Marco B. Caminati
      Received December 29, 2010
1120. FOMODEL2
      First order languages: syntax, part two; semantics.
       by Marco B. Caminati
      Received December 29, 2010
1121. FOMODEL3
      Free interpretation, quotient interpretation and substitution of a letter
      with a term for first order languages.
       by Marco B. Caminati
      Received December 29, 2010
1122. FOMODEL4
      Sequent calculus, derivability, provability. Goedel's completeness theorem.
       by Marco B. Caminati
      Received December 29, 2010
1123. CAYLEY
      Cayley's Theorem
       by Artur Korni{\l}owicz
      Received December 29, 2010
1124. BOR_CANT
      Borel-Cantelli Lemma
       by Peter Jaeger
      Received January 31, 2011
1125. NFCONT_4
      More on the Continuity of Real Functions
       by Keiko Narita, Artur Kornilowicz and Yasunari Shidama
      Received February 22, 2011
1126. STACKS_1
      Representation Theorem for Stacks
       by Grzegorz Bancerek
      Received February 22, 2011
1127. FINANCE1
      Elementary Introduction to Stochastic Finance in Discrete Time
       by Peter Jaeger
      Received March 22, 2011
1128. FVALUAT1
      Valuation Theory, Part {I}
       by Grzegorz Bancerek, Hidetsune Kobayashi and Artur Korni{\l}owicz
      Received April 7, 2011
1129. CC0SP2
      Banach Algebra of Complex-Valued Continuous Functionals and Space of
      Complex-valued Continuous Functionals with Bounded Support
       by Katuhiko Kanazashi, Hiroyuki Okazaki and Yasunari Shidama
      Received May 30, 2011
1130. MATRTOP3
      The Rotation Group
       by Karol P\kak
      Received May 30, 2011
1131. NDIFF_5
      Differentiable Functions on Normed Linear Spaces
       by Yasunari Shidama
      Received June 2, 2011
1132. MFOLD_2
      Planes and Spheres as Topological Manifolds. Stereographic Projection
       by Marco Riccardi
      Received June 6, 2011

   Regards,
   Adam Grabowski
   Library Committee of the Association of Mizar Users