gmane.science.mathematics.frogs

Call For Papers: Analytic Proof Systems 4

Agata Ciabattoni — 2008-09-18T08:32:55

Analytic Proof Systems 4 (4th International Workshop on Analytic Proof Systems) 22nd November < at > 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, pr

Projects in France

Alessio Guglielmi — 2008-08-13T15:16:19

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

5 Year Research Position in Math. Logic in Lisbon

Berarducci Alessandro — 2008-07-18T11:38:27

Da: "M. J. Edmundo" <public.gmane.org>edmundo-iPLCblZGu/b/EXfavOTA/A< at >public.gmane.org> 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/~logicmat/index.html Many thanks, Mario

3 years Postdoc position available in Ghent

Andreas Weierman — 2008-07-16T08:37:01

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

JELIA - registration opened

Bertram FronhÃ¶fer — 2008-07-11T13:16:44

Registeration for JELIA 2008 has opened. (see www.jelia.eu/2008/).

JOB OPPORTUNITY

Bertram FronhÃ¶fer — 2008-07-11T11:02:44

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

Software update

Alessio Guglielmi — 2008-07-08T12:35:10

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

Test

Alessio Guglielmi — 2008-07-08T11:51:09

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

Algorithmic Interpretation

Kai Brünnler — 2008-06-23T13:04:39

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

Extension

Alessio Guglielmi — 2008-06-20T20:59:12

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 . 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. In

Last Call, Nancy Workshop on Deep Inference

Francois Lamarche — 2008-06-11T16:21:27

(this looks better with a fixed width font) DEEP INFERENCE, ITS ALGEBRA, GEOMETRY AND SYNTAX June 18 Salle du conseil (C005, on the ground floor of Building C) at the Loria, Nancy. PRELIMINARY SCHEDULE (The talks are 45min + 5min question period) 10:00 - 10:30 Greetings and coffee 10:30 - 11:20 Lutz Strassburger Extension without cut 11:20 - 12:10 Bruno W. Paleo Algorithms for Herbrand Sequent Extraction 12:10 - 13:00 Tom Gundersen TBA 13:00 - 14:30 Lunch at the Loria Cafeteria 14:30 - 15:20 Jim Laird Games Semantics for deep inference 15:20 - 16:10 Kai Bruenller Towards Curry-Howard for deep inference 16:10 - 16:30 Coffe Break 16:30 - 17:20 Robert Hein The Conduche condition and dependent products 17:20 - 18:10 Paola Bruscoli TBA PRELIMINATY LIST OF PARTICIPANTS (you are welcome too) Paola Bruscoli University of Bath Guillaume Burel Loria Kai Bruenller Bern

Workshop on Deep Inference, Nancy

2008-05-25T19:27:51

(a reminder for many, an announcement for others, and perhaps something verging on spam for some, with apologies) The workshop Deep Inference, its Algebra, Geometry and Syntax Will be held in Nancy, France on June 18 2008. As the title implies the main theme of the workshop is deep inference, but talks on related subjects like the the improvement and abstract theory of proof formalisms are most welcome. The workshop will be held at the Loria computer science lab on Wednesday June 18 2008, starting at 10:30, so as to ensure an easy commute from Paris (there is a Paris-Nancy TGV that leaves Gare de l'Est at 8:12 and the last return train leaves Nancy at 20:15). The webpage http://www.loria.fr/~lamarche/deepinf.html contains a few more details, including suggestions for accomodation. Please contact me if you intend to attend and/or give a talk. François Lamarche

Workshop on Deep Inference in Nancy

Francois Lamarche — 2008-05-07T12:42:29

The workshop Deep Inference, its Algebra, Geometry and Syntax Will be held in Nancy, France on June 18 2008. As the title implies the main theme of the workshop is deep inference, but talks on related subjects like the the improvement and abstract theory of proof formalisms are most welcome. The workshop will be held at the Loria computer science lab on Wednesday June 18 2008, starting at 10:30, so as to ensure an easy commute from Paris (there is a Paris-Nancy TGV that leaves Gare de l'Est at 8:12 and the last return train leaves Nancy at 20:15). The webpage http://www.loria.fr/~lamarche/deepinf.html contains a few more details, including suggestions for accomodation. Please contact me if you intend to attend and/or give a talk. François Lamarche

Meeting in Bath?

Alessio Guglielmi — 2008-04-03T08:10:19

Hello, Who would be interested in a deep-inference meeting in Bath, in the second half of May? Ciao, -Alessio

Cirquent calculus deepened

Giorgi Japaridze — 2008-04-02T21:55:11

A new version of the paper is now available at http://arxiv.org/abs/0709.1308 A substantial change of perspective has taken place: classical logic can be seen as a natural conservative fragment of resource logics in the form of deep cirquent calculus. It is an extreme special case of cirquent-based resource logics where "everything is shared". And the approach of linear logic is another imperfect extreme where "nothing is shared". Cirquent calculus is thus a general unifying framework. Those who earlier took interest in this paper, might want to at least read the (totally new) introductory section of the new version. G.Japaridze Cirquent calculus deepened Abstract Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuit-style structures (called cirque

[SPAM] Poste Italiane News

Poste Italiane S.p.a — 2008-04-02T20:57:16

Atomic flows

Alessio Guglielmi — 2008-02-25T10:38:56

Hello, Tom and I rewrote the paper on atomic flows, which has been accepted by LMCS. Please, throw away the old version of that paper. There were no mistakes, but, thanks to the referees and those who read the old paper, especially Michel, this new version is much simpler and much better in almost every aspect. The only exception is that there is now a definition of atomic flow. We plan to follow up this paper with another one where we will explore in much more detail the global transformations based on atomic flows. In particular, we obtain very simple cut elimination and interpolation procedures, and the streamlining procedure will be much more tightly determined by the topological structure of atomic flows. I am now convinced of the truth and usefulness of the following slogan: bureaucracy-free proof system = CoS with inference rules on derivations = Formalism B = atomic flows + logical relations. So, I think that atomic flows give us yet another perspective on which to

LSFA 2008 - First call for papers

Elaine Pimentel — 2008-02-18T14:31:40

LSFA'08 - Third Workshop on Logical and Semantic Frameworks, with Applications August 26th, 2008 Salvador, Bahia, Brazil SCOPE Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for formal specification of systems and programming languages, supporting tool development and reasoning. The objective of this one-day workshop is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. Topics of interest to this forum include, but are not limited to: * Logical frameworks o Proof theory o Type theory o Automated deduction * Semantic frameworks o Specification languages and meta-languages o Formal semantics of languages and systems o

[CFP] Workshop on Symmetric calculi and Ludics for the semantic interpretation

Sylvain Pogodalla — 2008-02-08T09:56:38

[Apologies for multiple postings] SECOND CALL FOR PAPERS Workshop on Symmetric calculi and Ludics for the semantic interpretation (http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html) August 4-8, 2008 organized as part of the European Summer School on Logic, Language and Information ESSLLI 2008 (http://www.illc.uva.nl/ESSLLI2008/), 4-15 August, 2008 in Hamburg, Germany Workshop Organizers: Alain Lecomte (SFL - Paris 8), Alain.Lecomte-rI2LGqwzyoH82ACdesgHKQ< at >public.gmane.org Myriam Quatrini (IML Marseille), quatrini-YrJ6uwBEqj+NMqqgB3vDxg< at >public.gmane.org Workshop Purpose and topics: In recent years there have been some important new developments of methods of dealing with semantic and pragmatic phenomena in Linguistics, inspired by developments in Logic and Theoretical Computer Science. Among these developments, Continuation Theory, Symmetric calculi and Ludics play an important role. Continuation theory dates back from the early seventies (cf. Reynolds, 93) and was at the heart of Programming L

Happy new year!

Lutz Strassburger — 2008-01-03T22:03:48

Hello Frogs, What you all have been waiting for for five years is finally a reality: http://www.lix.polytechnique.fr/~lutz/papers/NELbig.pdf It is the first paper that contains a readable proof of the decomposition theorems and it is the first paper that contains a splitting proof involving exponentials. Any comments about this new version of an old paper are, of course, very welcome. Best wishes for the new year, Lutz ******************************************************* Title: "A System of Interaction and Structure IV: The Exponentials" Authors: Alessio Guglielmi and Lutz Straßburger Abstract: We study some normalisation properties of the deep-inference proof system NEL, which can be seen both as 1) an extension of multiplicative exponential linear logic (MELL) by a certain non-commutative self-dual logical operator; and 2) an extension of system BV by the exponentials of linear logic. The interest of NEL resides in: 1) its being Turing complete, while the same for MELL is not known, a

Workshop on "computational interpretations of proofs"

Michel Parigot — 2007-11-17T09:34:44

Dear Frogs, A workshop on "computational interpretations of proofs" will take place in Paris, November 29-30. http://www.pps.jussieu.fr/~cip/cip.html The workshop is open to everyone interested. If you intend to give a talk or simply participate, please let us know by sending an email to cip-klhGwnj84BVaYsKGlXaXRA< at >public.gmane.org The list of talks will be announced soon. Best wishes Michel