gmane.science.mathematics.frogs

Call For Papers: Analytic Proof Systems 4


                     Analytic Proof Systems 4
         (4th International Workshop on Analytic Proof Systems)
                22nd November @ LPAR 2008 Doha, Quatar
           http://www.logic.at/staff/chrisf/ws/LPAR-AS-4.html

                          Call for Papers

Analyticity is a topic that connects foundational issues in logic with
applications, mainly in automated deduction and analysis of proofs.
The workshop is primarily intended to enhance awareness for this topic
and to promote corresponding discussions and contacts between experienced
experts and younger colleagues.

TOPICS OF INTEREST include:

     * Old and new types of analytic calculi: sequent calculi,
       tableaux, connection method, hypersequents, deep inference
     * Cut elimination and Normalization: new methods, complexity,
       abstract approaches
     * Proof search: modeling proof search, streamlining calculi,
       model extraction
     * Relation to other methods: analytic systems and resolution,
       dialogue games, programming languages
     * Extracting information from analytic proofs: extraction of
       algorithms, constructivity, model construction, Herbrand's theorem

The workshop will be co-sponsered by the International Kurt G<F6>del Society 
(KGS) and will include a workshop dinner to which contributors are invited.

(Continue reading)

headers

Alessio Guglielmi | 13 Aug 17:13

Projects in France

Hi,

We have got the second big deep-inference grant approved in France. 
So, they might not be doing well in sports, but the French have good 
ideas about where to spend their research money (more than two 
million euros for the two projects).

This new project is called Demosthene (Francois's idea) and will 
involve Francois, Paola and myself for two years, on the problem of 
proof identity. We will start in the next few weeks.

So, young people on the list, if you like cheese, study deep inference!

-Alessio

headers

Berarducci Alessandro | 18 Jul 13:35

5 Year Research Position in Math. Logic in Lisbon

Da: "M. J. Edmundo" <<mailto:edmundo@...>edmundo@...>
Oggetto: 5 Year Research Position in Math. Logic in Lisbon

Dear colleagues,

Please announce everywhere, including Modnet mailling list, the following:

The Centre for Mathematics and Fundamental Applications (CMAF) at the 
University of Lisbon
invites applications for one 5-year research position in Mathematical Logic.
The successful applicant is expected to collaborate with the local 
team. Although there are no
teaching duties associated with this position, the candidate may be 
asked to collaborate in post-
graduate training. Deadline September 10, 2008. For details see 
<http://www.ciul.ul.pt/%7Elogicmat/index.html>http://www.ciul.ul.pt/~logicmat/index.html

Many thanks,

Mario

headers

Andreas Weierman | 16 Jul 10:36

3 years Postdoc position available in Ghent

To whom it may concern:

There is a three years postdoc position available at the department
of pure mathematics in Ghent. The candidate should have research experience
related to the existing expertise in the department. So in particular
candidates with research expertise in logic (e.g. proof theory, independence
results, phase transitions, subrecursive hierarchies, etc.)
are welcome.
The corresponding website is:
https://webster.ugent.be/vacatures/AAPWP/WE01d.html
This announcement is written in Dutch but
knowledge of Dutch is not required for the position.
(An English translation of the announcement can be provided on request.)
Salary ranges from min EUR 29069.79 to max EUR 45317.25
per year. Candidates should submit CV and copies of PhD diploma
via registered mail to the following address:
Directie Personeel en organisatie van de Universiteit Gent,
Sint-Pietersnieuwstraat 25, 9000 Ghent, Belgium.
The deadline is July 31st in 2008.

Best regards,
Andreas Weiermann

headers

Bertram FronhÃ¶fer | 11 Jul 15:15

JELIA - registration opened

Registeration for JELIA 2008 has opened.

(see www.jelia.eu/2008/).

headers

Bertram FronhÃ¶fer | 11 Jul 12:59

JOB OPPORTUNITY


 JOB OPPORTUNITY

 at the Knowledge Representation and Reasoning Group headed by Prof. 
 Hölldobler
 at the Faculty of Computer Science of the Technische Universität Dresden,
 Germany.

 The group  (www.wv.inf.tu-dresden.de/) coordinates the `European
 Master's 
 Program in Computational Logic'  (european.computational-logic.org/)  and
 manages the `International Center for Computational Logic'
 (www.computational-logic.org/index.php).
 The groups research orientation is strongly based on logic and formal 
 methods,
 while the focus lies on the development of methods for knowledge 
 representation
 and inference as well as on neural-symbolic integration.

 The open position is for a Ph.D. Student or Post-Doc. It is available from
 Aug. 1, 2008 with a duration of 3 years and the possibility of prolongation up
 to 2 years. The salary is based on E13 TV-L.

 The successful candidate is expected to do research in the area of 
 Computational
 Logic (leading to a doctoral thesis in case of candidates without
 Ph.D. respectivly leading to a `Habilitation' in case of Ph.D. 
 holders), to do
 four hours teaching per week during lecturing periods, to assist in 
 supervising

(Continue reading)

headers

Alessio Guglielmi | 8 Jul 14:30

Software update

Hello,

The Frogs list is now managed by a more modern software than the 
previous one. Hopefully, several of the glitches we noted in the past 
years will disappear. Please let me know if you find problems.

Ciao,

-Alessio

headers

Alessio Guglielmi | 8 Jul 13:48

Test

This is a test message intended to help the transition from Majordomo 
to Sympa.   -Alessio

headers

Lutz Strassburger | 23 Jun 15:07

Re: Extension

On Fri, 20 Jun 2008, Alessio Guglielmi wrote:

> Hi Lutz,
>
> I found your talk in Nancy very interesting, and I have some comments 
> that would have been impractical to discuss through Skype, so I'll do it 
> cc: to the list. We can refer to your paper 
> <http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf>.

Hi Alessio,

> I have two political concerns. It might very well be that I'm 
> missing quite a lot, so please correct me if I'm wrong.

Ok, let's discuss it. But you should know that I do not have strong 
opinions about "political" issues. I always try to present the stuff such 
that the technical issues become as simple as possible. (with a varying 
degree of success...)

> 1) I think that not using units complicates life.

I probably did not say that explicitly enough in the talk: I did not mean 
that omitting the units always simplifies life. Of course, your 
normalization on atomic flows would be a nightmare without units.
Similarly, when it comes to the algebra of proofs (i.e., categories), life 
is much easier with units.

But for the paper you are mentioning, I still think that the presentation 
is simpler without units. The situation is the same as with associativity

(Continue reading)

headers

"Kai =?iso | 23 Jun 15:02

Algorithmic Interpretation

Heihei!

Richard and I completed our first little attempt at interpreting deep
inference algorithmically. I talked about it in Nancy. If you're
interested, you can find the slides here:

http://kai.bruennler.googlepages.com/talks

and the paper here:

http://kai.bruennler.googlepages.com/unpublishednotes  .

Best wishes,

-Kai

headers

Alessio Guglielmi | 20 Jun 22:58

Extension

Hi Lutz,

I found your talk in Nancy very interesting, and I have some comments 
that would have been impractical to discuss through Skype, so I'll do 
it cc: to the list. We can refer to your paper 
<http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf>.

First of all, let me say that I find the simplified `Krajicek-Pudlak' 
theorem interesting, and I find QHQ fantastic. I also agree with all 
the technical matters (after a quick check).

That said, I have two political concerns. It might very well be that 
I'm missing quite a lot, so please correct me if I'm wrong.

1) I think that not using units complicates life. The amount of 
different systems is already daunting, and there really is no need to 
further complicate matters by adopting variants, like SKS- instead of 
SKS.

If I'm not mistaken, adopting units can have significant effects on 
p-simulations. For example, take eKS instead of eKS-, i.e., a cut 
free system with extension (your variant of it) and units instead of 
the same without units. Inside eKS, you can simulate an SKS cut like 
this:

        (a ^ -a)                    a         -a
    ai^ --------   becomes   (ext_ --- ^ ext_ ---).
           f                        f          t

This would give you that eKS p-simulates SKS (while it's not obvious

(Continue reading)

Mon	Tue	Wed	Thu	Fri	Sat	Sun

		1	2	3	4	5
6	7	8	9	10	11	12
13	14	15	16	17	18	19
20	21	22	23	24	25	26
27	28	29	30	31