gmane.science.mathematics.frogs

Avoiding Red Tape Frees Up Logic (ARTFUL)

Jon Awbrey — 2008-11-05T18:04:20

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o I was sampling the Frog List Archives and noticed a thread on "Bureaucracy and Identity" that seemed to ring a couple of bells. I can't say I grasped all the details of what was being proposed there, but the gist of it sounds very similar to design principles that I derive from the work of Charles Sanders Peirce. His attitude toward the design of formal languages for logical purposes appears to be that these are human artifacts crafted to an objective purpose, and so we are free to experiment with different ways of achieving the object of logic best, where logic is regarded in the traditional sense as one of the normative sciences. One of the consequences of this aesthetic is that we have no obligation to introduce artificial contraints and distinctions into our formal languages, unless those artifices serve logical purposes, and serve them better than alternative artifices. For example, it is an artifact of writing text in linear array that "

Correction

Alessio Guglielmi — 2008-11-02T10:11:10

Hi, I thought that it's not very clever to use the real list address, because if this one is spammed, we will have to moderate the list. So, I created a Google proxy. PLEASE USE THE ADDRESS ABOVE, i.e.: Frogs.List at GMail.com -Alessio

Change of address

Alessio Guglielmi — 2008-11-02T09:56:19

Hello, The address frogs-6f2JOXctL+67Jn3c8fOrWw< at >public.gmane.org has been collected by spammers, so I deactivated it. The new address to use is the one above, also indicated on the list web page. I'm going to take down prooftheory.org anyway, very soon, as it doesn't make sense any more. Frogs remains unmoderated (unless you ask me to do otherwise, of course). I think we all appreciate very low traffic. So, please, do not use the list address for conference announcements for the general community and such, especially because these announcements end up on the web and the addresses are harvested by spammers. Ciao, -Alessio

Gucci shoes LV shoes only $99

litcool — 2008-11-01T23:59:11

Gucci shoes LV shoes only $99 Gucci shoes Lacoste shoes LVshoes only $99 1800 styles Gucci shoes only $99 http://uspshoes.com Women shoes Highheel only $89 http://uspshoes.com/womenshoes.htm LV shoes: http://uspshoes.com/lv1.htm Gucci sneakers http://uspshoes.com/sneaker.htm Nike shoes only $69 http://uspshoes.com/nike.htm Lacoste shoes only $95 http://uspshoes.com/lacoste.htm D&G $95 http://uspshoes.com/dgsneaker.htm 180 styles,can't imagine! Only $99,can't cheaper! 1 day left,can't wait! Just 1 click. Post by litcool

self-introduction : jon awbrey

Jon Awbrey — 2008-10-30T14:22:12

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o i don't know if my interests fit in here, but i did see a few resonant themes in the archives, so what the heck ... my main directory page, where i collect links to papers (always in progress), projects, and vita info: http://www.mywikibiz.com/Directory:Jon_Awbrey focal interests: 1. graph-theoretic aspects of formal systems, e.g. formal languages that parse into nice families of graph-theoretic data structures like trees and cacti. some hint of this line of work is here: http://planetmath.org/encyclopedia/LogicalGraphFormalDevelopment.html 2. design of formal systems with attention to their conceptual elegance and computationsl efficiency. some design principles that appeal to me: a. i view deductive inference as factoring into information-preserving components (licensed by equational or reversible inference rules) and information-reducing components (licensed by "projections" like modus ponens, resolution

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

Re: Extension

Lutz Strassburger — 2008-06-23T13:07:45

On Fri, 20 Jun 2008, Alessio Guglielmi wrote: Hi Alessio, 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...) 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 and commutativity. Sometimes it is better to have them as equations, and sometimes it is better to make them into inference rules. Come on, this is a religious argument (the Holy Kai made it like this, we always did it like this, and therefore it is the o

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

Re:Meeting in Bath?

Alessio Guglielmi — 2008-04-03T12:40:09

Michel suggests Paris, Lutz suggests June, please indicate your preferences in your replies, I'll try and make a synthesis. Ciao, -Alessio

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