in Prague
Miroslav Olsak, University of Cambridge
J.D. Phillips, Northern Michigan University
Michael Rawson, TU Wien, Austria
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Josef Urban, Czech Technical University in Prague
Adam Vandervorst, SingularityNET
Sean
of Cambridge
J.D. Phillips, Northern Michigan University
Michael Rawson, TU Wien, Austria
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Josef Urban, Czech Technical University in Prague
Adam Vandervorst, SingularityNET
Zsolt Zombori, Alfréd Rényi Institute
, Jan 31, 2024 at 12:24 PM Josef Urban wrote:
> [This is a very late call and we are hoping for at least an informal
> deadline extension; please advertise/send it to people who might be
> interested.]
>
> ==
>
> The Hausdorff Trimester "Prospects of Formalized Ma
[This is a very late call and we are hoping for at least an informal
deadline extension; please advertise/send it to people who might be
interested.]
==
The Hausdorff Trimester "Prospects of Formalized Mathematics" will organize
a "School of Formalized Mathematics" (May 13 - 17, 2024).
ido University)
Lutz Straßburger (Inria Saclay)
Thomas Studer (University of Bern)
Josef Urban (Czech Technical University in Prague)
Yoni Zohar (Bar-Ilan University)
Zsolt Zombori (Alfréd Rényi Institute of Mathematics)
Hans de Nivelle (Nazarbayev University)
PC CHAIRS
Revantha Ramanaya
, University Paris 1
Miroslav Olsak, IHES
J.D. Phillips, Northern Michigan University
Michael Rawson, TU Wien, Austria
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Christian Szegedy, Google Research
Josef Urban, Czech Technical University in Prague
Zsolt Zombori
ersity of Bern)
Josef Urban (Czech Technical University in Prague)
Yoni Zohar (Bar-Ilan University)
Zsolt Zombori (Alfréd Rényi Institute of Mathematics)
Hans de Nivelle (Nazarbayev University)
PC CHAIRS
Revantha Ramanayake (University of Groningen)
Josef Urban (Czech Technical University in
Szegedy, Google Research
Josef Urban, Czech Technical University in Prague
Zsolt Zombori, Alfréd Rényi Institute of Mathematics
CONTRIBUTED TALKS
We solicit contributed talks. Selection of those will be based on
extended abstracts/short papers of 2 pages formatted with easychair.cls.
Submission
COMMITTEE
To be announced.
PC CHAIRS
Revantha Ramanayake (University of Groningen, The Netherlands)
Josef Urban (Czech Technical University in Prague, Czech Republic)
LOCAL ORGANIZERS
Karel Chvalovsky (Czech Technical University in Prague, Czech Republic)
Jan Jakubuv (Czech Technical University
, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Josef Urban, Czech Technical University in Prague
Robert Veroff, University of New Mexico
Petr Vojtěchovský, University of Denver
Freek Wiedijk, Radboud University Nijmegen
Stephen Wolfram, Wolfram Research
CONTRIBUTED TALKS
We solicit
Michael Kinyon, University of Denver
Tomáš Mikolov, Czech Technical University in Prague
Alberto Naibo, University Paris 1
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Josef Urban, Czech Technical University in Prague
Petr Vojtěchovský, University of Denver
Freek
===
The 6th International Congress on Mathematical Software will be held from
July
24 to July 27, 2018 at the University of Notre Dame. The General Chair is
James
H. Davenport, the Program Chairs are Manuel Kauers, George Labahn and Josef
Urban, and the Local Chairs
of Mathematics, and related fields. The group has a large and
active network of collaborations around the world. The AI4REASON project
led by Josef Urban is funded by the European Research Council (ERC) which
targets highest-quality investigator-driven frontier research in Europe (
https://erc.europa.eu
Last year I wrote some functions for calling Hol(y)Hammer remotely:
https://github.com/JUrban/hol-advisor/blob/master/hol-advice.el
It was done on top of this HOL Light mode (used by Flyspeck I think):
https://github.com/JUrban/hol-advisor/blob/master/hol-light.el . I
think I changed that mode a
2nd Call for Papers
Conference on Intelligent Computer Mathematics
CICM 2015
13-17 July 2015
Washington DC, USA
Digital and computational solutions are
guidelines and the JFR latex style are
available at http://jfr.unibo.it/about/submissions#onlineSubmissions.
In the first step of the online submission process, authors should
select the section: QED 20th anniversary.
GUEST EDITORS
-
John Harrison (Intel Corporation)
Josef Urban (Radboud
http://www.bourbaki.ens.fr/TEXTES/1086.pdf
The whole session is here (with video links):
http://www.bourbaki.ens.fr/seminaires/2014/Prog_juin14.html
Josef
--
Open source business process management suite built on Java
mathematical texts
in controlled natural language
Geoff Sutcliffe: QED and the TPTP World
Michael Kohlhase: MathHub.info: Active Mathematics
Cezary Kaliszyk: Hammering towards QED
Panel Discussion
ORGANIZERS:
John Harrison, Josef Urban, Freek Wiedijk
http://vsl2014.at/meetings/QED-index.html
-- Forwarded message --
From: SYNASC 2014 synas...@synasc.ro
Date: Wed, Jun 11, 2014 at 9:43 AM
Subject: CFP Synasc 2014 (FIRM extended deadline)
To: idramnesc idramn...@info.uvt.ro
[Please post - apologies for multiple copies.]
Call for Papers
---
version control, and searchable through the GitWeb interface. If there is
sufficient demand, we can also implement project update on the server
through Git (upon git-push done by a registered user).
The service is described in http://arxiv.org/abs/1309.4962 .
Cezary Kaliszyk Josef Urban
On Fri
can you give me the FOL formula for (0 \in 0), and how your derived it?
This is explained in
http://en.wikipedia.org/wiki/Extension_by_definitions#Definition_of_function_symbols
.
The empty set is obtained by proving
?!y: !u : ~(u \in y)
so, to match their notation, \phi is then !u : ~(u \in
that it has the
same strength as the original).
Best,
Josef
[1] I once thought of some practical use for this in
http://ceur-ws.org/Vol-767/paper-09.pdf :-)
On Fri, Sep 7, 2012 at 5:13 PM, Gottfried Barrow
gottfried.bar...@gmx.com wrote:
On 9/7/2012 4:41 AM, Josef Urban wrote:
Hi,
just a quick
Hi Bill,
I've worked very hard to make my miz3 Hilbert axiomatic geometry code
readable, and taking huge leaps nobody could follow would be
counterproductive. But I'm against shackling the proof assistant, as we agree
Mizar does but miz3 does not:
Yes, Mizar is certainly shackled in
Hi Bill,
Josef, it sounds like you're saying that Mizar is intentionally weak, and
that the reason for weakness is to make it practical to make calls to the
huge Mizar library.
The reasoning is that speed implies easy refactoring, and that
facilitates optimization of the library. Making the
On Tue, Jul 24, 2012 at 6:41 AM, Bill Richter
rich...@math.northwestern.edu wrote:
But I do it now only for Mizar, and I told you the results (the
shortening would be about 1400 lines of your Mizar code to some 300,
if ATPs could prove everything).
Josef, that's great, and Mizar is
Hi Bill,
Josef, let me try again. I apologize for not knowing the terminology or
anything about Vampire. Would there be a way to turn my 971 lines of Tarski
code http://www.math.northwestern.edu/~richter/TarskiAxiomGeometryCurry.ml
(which for Freek I made all my predicates official
Hi Bill,
On Fri, Jul 20, 2012 at 9:00 PM, Bill Richter
rich...@math.northwestern.edu wrote:
I'm looking for some kind of upper bound on how astounding a result you
can prove with little work if we have no heuristics, e.g. no `limit on depth
of chaining.'
There is no established limit.
On Wed, May 30, 2012 at 8:19 AM, Bill Richter
rich...@math.northwestern.edu wrote:
BTW Makarius seemed to say on the Isabelle group that Mizar is exactly
FOL with some automation to relieve the tedious parts of FOL.
Mostly yes. It is (a bit strengthened) ZFC/FOL with small amount of
(Charles University, Czech Republic)
o Georg Struth (University of Sheffield, UK)
o Josef Urban (Radboud University, Netherlands)
WORKSHOP ORGANISERS
o Alan Smaill
o Annabelle McIver
o Peter Höfner
o Jacques Fleuriot
The information in this e-mail may
Aspinall
* Joe Corneli
* Cezary Kaliszyk
* Fairouz Kamareddine
* Michael Kohlhase
* Markus Krötzsch
* Christoph Lange (co-chair)
* Lionel Mamane
* James McKinna
* Piotr Rudnicki
* Carst Tankink
* Josef Urban (co-chair)
* Denny Vrandečić
30 matches
Mail list logo
