May 2000 - Categories - categories.org.au

LINEAR Summer School (2nd call)
by Nuno Barreiro 08 Jun '00

08 Jun '00

Please forward. We apologize for any duplication of this message in your mailbox. Best regards, Nuno Barreiro ------------------------------------------------------------------ =================================== = SECOND CALL - EXTENDED DEADLINE = =================================== The LINEAR International Summer School (Linear Logic and Applications) August 30 to September 7, 2000 Hotel Terra Nostra, S.Miguel, Azores, Portugal The Linear TMR research network (http://iml.univ-mrs.fr/LINEAR) is proud to announce its first International Summer School on Linear Logic and Applications. The school is directed to everyone doing postgraduate work in Computer Science or Mathematics with an interest in the field of Formal Logic and its applications. The school lasts one week and comprises both lectures and thematic sessions. The lectures are in the tradition of summer schools and cover one topic, from basic material to more advanced issues. The topics and lecturers are the following: Samson Abramsky --- Game Semantics Jean-Yves Girard -- Linear Logic and Ludics Stefano Guerrini -- Proof-Nets and Lambda-Calculus Yves Lafont ------- Phase Semantics and Decision Problems Phil Scott -------- Category Theory and Concrete Models The thematic sessions will cover state-of-the-art research in Linear Logic. Each session has an organiser responsible for inviting speakers who will talk about their work. The themes and organisers are the following: Andrea Asperti ---- Applications Vincent Danos ----- Proof Theory Thomas Ehrhard ---- Semantics Glynn Winskel ----- Concurrency The school will be held in the island of S.Miguel, Azores, amid luxurious vegetation and hot water springs. The entrance to the mythic kingdom of the Atlantis is believed to be located near Hotel Terra Nostra, some say at the bottom of its famous red and hot water swimming pool... Detailed information and application forms are available at http://linear.di.fc.ul.pt Don't forget to check it!

1 2

FMCS2000
by John MacDonald 01 Jun '00

01 Jun '00

FMCS2000 Foundational Methods in Computer Science JUNE 1st - 4th, 2000 The Department of Mathematics at the University of British Columbia, in cooperation with the Pacific Institute of Mathematical Sciences, is hosting the Foundational Methods in Computer Science workshop from June 1 to June 4, 2000, on the University of British Columbia Campus in Vancouver, B.C., Canada. The workshop is an informal meeting to bring together researchers in mathematics and computer science with a focus on the applications of category theory in computer science. The reception in the evening of June 1, 2000, at Walter Gage Towers, is followed by a day of tutorials aimed at students and newcomers to category theory, followed by a day and a half of research talks. There will be a few invited presentations, but the majority of the talks are solicited from the participants. Student participation is particularly encouraged at FMCS. PARTICIPANT LIST (as of May 1, 2000) Jeremy Bem, University of California, Berkeley David Benson, Washington State University Robin Cockett, University of Calgary Adam Eppendahl, Queen Mary and Westfield College, London Hongge Gao, Northeastern University Michael Johnson, Macquarie University, Sydney John MacDonald, University of British Columbia Ernest Manes, University of Massachusetts at Amherst Stefan Milius, York University Philip Mulry, Colgate University Cristina Pedicchio, University of Trieste Vaughan Pratt, Stanford University Robert Schneck, University of California, Berkeley Robert Seely, McGill University Peter Selinger, University of Michigan Lebelo Serutla, National University of Lesotho Tim Sheard, Oregon Graduate Institute Manuela Sobral, University of Coimbra, Portugal Art Stone, Vancouver Walter Tholen, York University Varmo Vene, Estonia Richard Wood, Dalhousie University Please note that not all of the individuals on the participant list have been confirmed. There still are a few places on the program for research presentations of 20 to 30 minutes. Reduced accommodation and registration rates are available to graduate student participants. Further information about FMCS2000 may be obtained from the conference website at http://www.pims.math.ca/science/2000/fmcs . You may also obtain housing and registration forms by sending email to johnm(a)math.ubc.ca with subject heading FMCS2000. If you are planning to attend (or might attend) the conference and your name is not on the above list, then please let me know. That way I can keep track of how many people will be attending and also keep you updated. John MacDonald Local organizer, FMCS2000

1 1

Pataraia
by Martin Escardo 31 May '00

31 May '00

Thanks to all of you who replied to my query. Dito Pataraia has kindly sent me a copy of his manuscript. Here are the details of the short note I've written based on that. ---------------------------------------------------------------------- On the nuclear reflection of a prenucleus ---------------------------------------------------------------------- There are at least three ways of obtaining the nuclear reflection of a prenucleus. We describe a fourth, based on an intuitionistic version of Tarski's fixed-point theorem due to Pataraia. As an illustration of the technique, we offer a simple intuitionistic proof of Johnstone's localic version of the Hofmann-Mislove theorem, which says that the compact fitted sublocales of any locale are in order-reversing bijection with the Scott open filters of opens. ---------------------------------------------------------------------- Available as http://www.dcs.st-and.ac.uk/~mhe/papers/nuclei.ps (and also gzipped, dvi etc.)

1 0

announcement
by Chikoidze 31 May '00

31 May '00

To whom it may concern, Dear Sir, Please, be so kind as to include the Announcement of the Tbilisi Summer School in your e-mail list. I hope, you will find all necessary information in the Announcement itself. Best regards, George Chikoidze Contact Person of the Centre on Language, Logic, Speech at the Tbilisi State University Address: Dpt. of Language Modelling Inst. of Control Systems Georgian Academy of Sciences 34, Gamsakhurdia Av. 380060 Tbilisi Georgia Phone: + 995 32 38 21 36 Fax: + 995 32 94 23 91 E-mail: chiko(a)contsys.acnet.ge ANNOUNCEMENT Tbilisi Summer School in Language, Logic, and Computation 29th August - 8 September 2000 Tbilisi, Georgia The Georgian Centre for Language, Logic, and Speech, based at the Tbilisi State University, will host Tbilisi Summer School, the main purpose of which is to make the students and young scholars acquainted with the modern state of affairs in the mentioned fields of science, and - at the same time - to further contacts and scientific collaboration between Western and Eastern Scholars. LECTURERS Jurij Apresjan, Moscow Matthias Baaz, Vienna Pascal Boldini, Paris Marina Glavinskaja, Moscow Michel Parigot, Paris Carl Vogel,Dublin Andrej Voronkov, Manchester COURSES - Foundations of linguistic semantics (Ju.Apresjan) - On the generalisation of proofs and calculations (M.Baaz) - Type theories for semantics and cognition (P.Boldini) - Semantics of aspect (M.Glavinskaja) - Proofs as programs (M.Parigot) - Cognitive constraints on linguistic theory. (C.Vogel) - Logical foundations of deductive databases. (A.Voronkov). SCHEDULE Tuesday, August 29 12.00 - 13.00 Opening of the School 18.00 - Banquet Wednesday, August 30 10.00 - 13.00 M. Parigot. Proofs as programs 13.00 - 14.00 Lunch 14.00 - 17.00 Ju. Apresjan. Foundations of linguistic semantics Thursday, August 31 10.00 - 13.00 M. Parigot. Proofs as programs. 13.00 - 14.00 Lunch 14.00 - 17.00 Ju. Apresjan. Foundations of linguistic semantics. Friday, September 1 10.00 - 13.00 M. Glavinskaja. Semantics of aspect. 13.00 - 14.00 Lunch 14.00 - 17.00 C. Vogel. Cognitive constraints on linguistic theory. Saturday, September 2 Recreation (sight-seeing in Tbilisi and environs, Sunday, September 3 excursion). Monday, September 4 10.00 - 13.00 M. Glavinskaja. Semantics of aspect. 13.00 - 14.00 Lunch 14.00 - 16.00 C. Vogel. Cognitive constraints on linguistic theory. Tuesday, September 5 10.00 - 14.00 A. Voronkov. Logical foundations of deductive databases. 14.00 - 15.00 Lunch 15.00 - 17.00 C. Vogel. Cognitive constraints on linguistic theory. Wednesday, September 6 10.00 - 12.00 A. Voronkov. Logical foundations of deductive databases. 12.00 - 14.00 M. Baaz. On the generalization of proofs and calculations. 14.00 - 15.00 Lunch 15.00 - 17.00 P. Boldini. Type theories for semantics and cognition. Thursday, September 7 10.00 - 12.00 M. Baaz. On the generalisation of proofs and calculations. 12.00 - 14.00 P. Boldini. Type theories for semantics and cognition. 14.00 - 15.00 Lunch Friday, September 8 10.00 - 12.00 M. Baaz. On the generalization of proofs and calculations. 12.00 - 14.00 P. Boldini. Type theories for semantics and cognition. 14.00 - 15.00 Lunch 15.00 - 16.00 Closing of the School. 18.00 Banquet STUDENTS Besides local students, the School also welcomes students from abroad. The Participation fee for these students will be $120 (wich includes excursion, banquet, reprints, etc.).Foreign students will be comfortably accommodated with Georgian families (with two meals) for $40 per day. LOCATION AND SIGHTSEEING TOURS Georgia is the ancient country situated between Black and Caspian seas, the Caucasus and Turkey. It is the country of the Golden Fleece, the myth of Argonauts, Jason and Medea, and Prometheus, chained to the Caucasus mountains. Tbilisi - capital of Georgia - has more than 1 million in habitant. It is situated some 100-150 km to the south of main Caucasus ridge, in the beautiful valley of the river Mtkvari, surrounded by the green slopes of the Caucasus spurs. The city has a long (1500 year old) history and abounds in historical and cultural memorials. Georgia is famous for its high quality wines, exquisite cuisine and cordial hospitality. The main site of the Symposium, Tbilisi State University, is the chief centre of education in the country, and has several outstanding scholars in science, art and politics among its graduates. During the School there will be an excursion over the famous Georgian Military Road, which leads us through the ancient capital of Georgia - Mtskheta, with its abundant architectural and historical monuments - and which brings us across the main ridge of the Caucasus by the Cross Pass. The destination of the envisaged trip is the mountain resort Kazbegi with its Trinity Church situated on the top of high peak facing the second mountain (after Elbrus), the peak of the Caucasus - Mkinvarcveri (Glacier - mountain). TRAVEL INFORMATION Tbilisi can only be reached by air. If there are no direct trip between your point of departure and Tbilisi, the most convenient connections are via Istambul, Frankfurt or Moscow. ORGANISING COMMITTEE: T.Khurodze (Chair, Pro-rector of Tbilisi State University) R.Asatiani (Institute of Oriental Studies) N.Chanishvili (Tbilisi State University) G.Chikoidze (Institute of Control Systems) K.Pkhakadze (Institute of Applied Mathematics) Kh.Rukhaja (Institute of Applied Mathematics). For additional information, please, use the following address: George Chikoidze Dept. of Language Modelling Inst. of Control Systems Georgian Academy of Sciences 34, K. Gamsakhurdia 380060 Tbilisi Georgia Phone: +9 9532 382136 E- mail: chiko(a)contsys.acnet.ge

1 0

question
by adrian duma 31 May '00

31 May '00

Dear Experts in Category Theory, I am very interested in the following problem. Let us consider the category Cat of small categories. I need for a "topology" on Morph(Cat) (i.e., the functors between small categories), with the following property: For each u in Morph(Cat) and each D in Ob(Cat) there exist v C------------>D in Morph(Cat), a functor F:Cat----->Cat with F(u) = v, and two "open neighbourhoods" U and V of u and v, respectively, such that F (acting on Morph(Cat)) is a "homeomorphism" between U and V. I would be very grateful to you for any related comment. With my best regards, I remain Truly Yours Adrian Duma. ____________________________________________________________________ Get free email and a permanent address at http://www.netaddress.com/?N=1

1 0

Lectureships in Computer Science
by Roy L. Crole 31 May '00

31 May '00

Dear Colleagues, I would like to announce three Lectureships in Computer Science, which may be of interest to CATEGORIES and TYPES readers. Leicester has a research group working in Categories and Semantics which includes Simon Ambler, Neil Ghani, Vincent Schmitt, Nobuko Yoshida and myself. Current research areas include Operational Semantics, Mechanized Reasoning, Categorical Models of Programming Languages including Concurrency, Categorical Term Rewriting, and Enriched Category Theory. These areas are directly or indirectly connected with the theory and practice of categories and types. Roy Crole. --------------------- %< ---------------------------------------- UNIVERSITY OF LEICESTER DEPARTMENT OF MATHEMATICS & COMPUTER SCIENCE Lecturer A in Computer Science (3 posts) Available from 1 September 2000 Ref: A5365/GD Applications are invited for three open-ended Lectureships in Computer Science in the Department of Mathematics and Computer Science at the University of Leicester. There is no restriction regarding the area of research and applicants with expertise in any area of Computer Science are welcomed. All three lectureships are tenable from 1 September 2000 or as soon as possible thereafter. The Department of Mathematics and Computer Science is divided into three groups: Computer Science, Pure Mathematics and Applied Mathematics. The Computer Science Group is firmly research oriented and these lectureships are intended to strengthen the Group with regard to both teaching and research. The successful applicants will be ambitious, able to develop their own research within a multi-faceted environment, and have a strong research record and potential. The new lecturers will be required to teach at undergraduate and postgraduate level, and to perform administrative duties as directed by the Head of Department. This is a superb opportunity for persons of energy, drive and ambition to assume rewarding roles and to establish themselves in a young, dynamic and rapidly developing department. Initial salary, dependent upon qualifications and experience, will be on the Lecturer Grade A scale UKpounds 17,238 to UK pounds 22,579 p.a. Candidates who are interested in the lectureships are invited, if they so wish, to contact Professor Iain Stewart, Head of Department telephone (+44) (0)116 252 3885, e-mail i.a.stewart(a)mcs.le.ac.uk or Professor Rick Thomas, Deputy Head of Department telephone (+44) (0)116 252 3411, email rmt(a)mcs.le.ac.uk, who will be pleased to discuss the Lectureships further. Information about all aspects of the Department is available from its World Wide Web pages [http://www.mcs.le.ac.uk] Further particulars and application forms are available, by quoting the reference A5365/GD, from Personnel Office, University of Leicester, University Road, Leicester LE1 7RH, U.K telephone (+44) (0)116 252 2439 email jobs(a)le.ac.uk, or via http://www.le.ac.uk/personnel/jobs The closing date for applications is 16 June 2000.

1 0

Pataraia's fixed-point theorem
by Martin Escardo 27 May '00

27 May '00

An intuitionistic version (in the sense of topos logic) of Tarski's fixed-point theorem, by Dmitri Pataraia, was discussed in this list some years ago. (I think it was presented in the PSSL in November 1997, but I didn't attend that.) I've written a paper that uses this, and I would like to cite it appropriately. Does anyone know if it has been published? (I didn't find anything in MathSciNet or Zentralblatt MATH.) (Maybe someone knows his e-mail address? I failed to find his whereabouts using search engines.) Thanks.

1 0

CFP: LPAR'2000, Reunion Island, France
by Andrei Voronkov 27 May '00

27 May '00

Subject: CFP: LPAR'2000, Reunion Island, France X-Mailer: VM 6.71 under 21.1 (patch 7) "Biscayne" XEmacs Lucid Sender: pmaenpaa(a)mappi.helsinki.fi X-Originating-IP: 130.233.193.43 Subject: CFP: LPAR'2000, Reunion Island, France [Apologies for receiving multiple copies ] LPAR'2000 7th International Conference on LOGIC for PROGRAMMING and AUTOMATED REASONING Reunion Island, November 6-10, 2000 CALL FOR PAPERS http://www.cs.man.ac.uk/~voronkov/LPAR/2000/general.html Location: LPAR'2000 will be held November 6-10, 2000, on Reunion Island, a small french island in the Indian Ocean, to the east of Madagascar. It will be followed by a "Workshop on Implementations of Logic", November 11-12. Topics: * automated reasoning * lambda and combinatory calculi * interactive theorem proving * constructive logic and type theory * implementations of logic * computional interpretations of logic * design of logical frameworks * logical foundations of programming * program & system verification * logical aspects of concurrency * model checking * program extraction from proofs * rewriting * linear logic * logic programming * modal and temporal logics * constraints programming * knowledge representation & reasoning * logic and databases * reasoning about actions * logic & computational complexity * description logics * specification using logics * nonmonotonic reasoning Invited speakers: * BrunoCourcelle (Bordeaux-1 University) * Georg Gottlob (Technische Universitaet Wien) * Erich Graedel (RWTH Aachen) * Michael Rusinowitch (LORIA-INRIA-Lorraine) Programme Committee: * Stefano Berardi, Torino * Leonid Libkin, Bell Labs * Manfred Broy, Munich * Patrick Lincoln, SRI * Maurice Bruynooghe, Leuven * David McAllester, AT&T Labs * Hubert Comon, Cachan * Robert Nieuwenhuis, Barcelona * Gilles Dowek, INRIA * Mitsuhiro Okada, Tokyo * Harald Ganzinger, MPI * Catuscia Palamidessi, Penn State * Mike Gordon, Cambridge * Leszek Pacholski, Wroclaw * Yuri Gurevich, Microsoft Res. * Michel Parigot, Paris (co-chair) * Neil Jones, Copenhagen * Frank Pfenning, Pittsburgh * Teodor Knapik, Reunion * Helmut Schwichtenberg, Munich * Yves Lafont, Marseille * Jan Smith, Goteborg * Daniel Leivant, Bloomington * Wolfgang Thomas, Aachen * Maurizio Lenzerini, Roma * Pascal van Hentenryck, Providence * Giorgio Levi, Pisa * Andrei Voronkov, Manchester (co-chair) Organizing Committee: * Teodor Knapik, University of Reunion * Pascal Manoury, University of Paris VI * Andrei Voronkov, University of Manchester Submission of papers: Submitted papers must be original and not submitted concurrently for publication to a journal or to another conference. Submission by members of the Program Committee is not allowed. The proceedings of LPAR'2000 will be published by Springer-Verlag in the LNAI series and available at the conference. Both "theoretical" papers and "experimental" papers are welcome. The first category is intended to contain new theoretical results, the second one to describe implementations of systems, to report experiments with implemented systems, or to compare implemented systems. Submitted "theoretical" papers should not be longer than 15 proceedings pages. Submitted "experimental" papers should not be longer than 10 proceedings pages. The proceedings of LPAR'2000 will be published by Springer-Verlag in the LNAI series. Papers in the postscript or PDF format, preferably uuencoded and zipped or gzipped, should be sent by email to lpar00-submission(a)cs.man.ac.uk. Title, abstract, and the list of authors with their email addresses should be sent to the same address in a separate message. --------------------------------------------- All questions related to submission should be sent to the program chairs: Michel Parigot <parigot(a)logique.jussieu.fr> and Andrei Voronkov <voronkov(a)cs.man.ac.uk> Important dates: Submission: June 1 Notification: July 15 Final version: August 10 Conference: November 6-10 Worskhop: November 11-12 More information: http://www.cs.man.ac.uk/~voronkov/LPAR/2000/general.html

1 0

FTP 2000 and TABLEAUX 2000 - Call for Participation
by Peter Baumgartner 22 May '00

22 May '00

------------------------------------------------------------------------- FTP 2000 and TABLEAUX 2000 Call for Participation University of St Andrews St Andrews, Scotland July 3-7, 2000 FTP 2000: http://www.uni-koblenz.de/ftp00/ TABLEAUX 2000: http://www-theory.dcs.st-and.ac.uk/~rd/tab2000/ --------------------------------------------------------------------- Contents: 1 - Scope 2 - Registration 3 - Contact 4 - Technical Program (including list of accepted contributions) --------------------------------------------------------------------- 1 - Scope FTP 2000 (First-Order Theorem Proving), July 3-5, is the third in a series of workshops intended to focus effort on First-Order Theorem Proving as a core theme of Automated Deduction, and to provide a forum for presentation of very recent work and discussion of research in progress. TABLEAUX 2000, July 4-7, is a continuation of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods held since 1992. The conference brings together researchers interested in all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods. FTP 2000 is held in conjunction with TABLEAUX 2000. The FTP 2000 and TABLEAUX 2000 sessions will be partly in series, partly shared and partly in parallel. --------------------------------------------------------------------- 2 - Registration To register for FTP 2000 and/or TABLEAUX 2000 please use the online registration form at http://www.dcs.st-and.ac.uk/~tab2000/register.html Joint registration at reduced rate is possible. Early registration ends at May, 31. --------------------------------------------------------------------- 3 - Contact FTP 2000 related: ftp00(a)cs.uiowa.edu TABLEAUX 2000 related: rd(a)dcs.st-and.ac.uk Local Organisation: rd(a)dcs.st-and.ac.uk --------------------------------------------------------------------- 4 - Technical Program FTP 2000 and TABLEAUX 2000 schedule: http://www.dcs.st-and.ac.uk/~tab2000/schedule.html Invited Talks ------------- FTP 2000 TABLEAUX 2000 -------- ------------- David Crocker Melvin Fitting (CUNY) (Intelligent Micro Modality and Databases Software Ltd) First Order Theorem Proving in Software Verification Deepak Kapur (New Mexico) Alasdair Urquhart (Toronto) 'Hardware Verification' Local Symmetries in (exact title to be announced) Propositional Logic Franz Baader (Aachen) (Joint invited speaker) Tableau Algorithms for Description Logics FTP 2000 accepted contributions: -------------------------------- J. Avenhaus, T. Hillenbrand, B. Loechner On Using Ground Joinable Equations in Equational Theorem Proving Johan Belinfante The Unifying Concept of Subvariance Domenico Cantone The decision problem in graph theory with reachability related constructs Michael Dierkes Defining a Unique Herbrand Model for Sets of Guarded Clauses Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt Hyperresolution for Guarded Formulae Martin Giese A First-Order Simplification Rule with Constraints Koji Iwanuma, Katsumi Inoue, Ken Satoh Completeness of Pruning Methods for Consequence Finding Procedure SOL James J. Lu, Jeffrey S. Rosenthal, Andrew Shaffer Crossword Puzzles: A Case Study in Compute-Intensive Meta-Reasoning Nicolas Peltier Combining Resolution and Enumeration for Finite Model Building Reinhard Pichler Equational Problems over a Finite Domain Regimantas Pliuskevicius On \omegaÂdecidability for a restricted FTL with Unless J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, F. Martin A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2) Nicolas Peltier Model Building with Ordered Resolution Cesare Tinelli Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing Bernhard Gramlich Extending First-Order Unification by Tractable Second-Order Features Kahlil Hodgson, John Slaney Semantic Guidance for SaturationÂBased Theorem Proving Bernhard Beckert DepthÂfirst Proof Search without Backtracking for Free Variable Clausal Tableaux Jens Otten, Wolfgang Bibel leanCoP: Lean ConnectionÂBased Theorem Proving (system description) Position Papers Chris Fermueller Automated Model Building for Non-Classical Logics Martin Giese Proof Search without Backtracking using Instance Streams Markus Moschner Towards Finite Model Building for Propositional GÃ¶del-Logics TABLEAUX 2000 accepted contributions ------------------------------------ Comparison of Theorem Provers for non-classical logics: Fabio Massacci and Francesco M. Donini Design and results of TANCS-2000 non-classical (modal) systems comparison Volker Haarslev and Ralf MÃ¶ller Consistency testing: the RACE experience Ian Horrocks Benchmark analysis with FaCT Ullrich Hustadt and Renate Schmidt MSPASS Modal reasoning by translation and first-order resolution Peter F. Patel-Schneider TANCS-2000 results for DLP Armando Tacchella Evaluating *SAT on TANCS 2000 benchmarks Research Papers: Alberto Artosi, Guido Governatori and Antonino Rotolo A labelled tableau calculus for nonmonotonic (cumulative) consequence relations Arnon Avron A tableau system for GÃ¶del-Dummett logic based on a hypersequent calculus Matthias Baaz, Christian FermÃ¼ller and Helmut Veith An analytic calculus for quantified propositional GÃ¶del logic Diderik Batens and Joke Meheus A tableau method for inconsistency-adaptive logics Domenico Cantone and Calogero G. Zarba A tableau calculus for integrating first-order reasoning with elementary set theory reasoning Agata Ciabattoni and Mauro Ferrari Hypertableau and path-hypertableau calculi for some families of intermediate logics Marta Cialdea Mayer and Serenella Cerrito Variants of first-order modal logics StÃ©phane Demri Complexity of simple dependent bimodal logics Uwe Egly Properties of Embeddings from Int to S4 Melvin Fitting, Lars Thalmann and Andrei Voronkov Term-modal logics Enrico Giunchiglia and Armando Tacchella A subset-matching size-bounded cache for satisfiability in modal logics Rajeev GorÃ© Dual intuitionistic logic revisited Ray Gumb Model sets in a nonconstructive logic of partial terms with definite descriptions Ortrun Ibens Search space compression in connection tableau calculi using disjunctive constraints Christoph Kreitz and Brigitte Pientka Matrix-based inductive theorem proving Pedro J. MartÃn and Antonio Gavilanes Monotonic preorders for free variable tableaux Maarten Marx, Szabolcs MikulÃ¡s and Mark Reynolds The mosaic method for temporal logics Linh Anh Nguyen Sequent-like tableau systems with the analytic superformula property for the modal logics KB, KDB, K5, KD5 David Pearce, Inmaculada P. de GuzmÃ¡n and AgustÃn Valverde A tableau calculus for equilibrium entailment Carla Piazza and Alberto Policriti Towards tableau-based decision procedures for non-well-founded fragments of set theory Riccardo Rosati Tableau calculus for only knowing and knowing at most Stephan Schmitt A tableau-like representation framework for efficient proof reconstruction Dan Willard The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic Q System Descriptions: Joachim Draeger Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO Gernot Stenz and Andreas Wolf E-SETHEO: An automated3 theorem prover --------------------------------------------------------------------- -- Peter Baumgartner phone: +49 261 287 2777 mail: peter(a)uni-koblenz.de fax: +49 261 287 2731 WWW: http://www.uni-koblenz.de/~peter/

1 0

FSTTCS 2000: revised Call for Papers
by Sanjiva Prasad 20 May '00

20 May '00

--text follows this line-- *********************************************************************** * * * FST TCS 2000 * * * * Foundations of Software Technology and Theoretical Computer Science * * December 13--15, 2000 * * New Delhi, India * * * *********************************************************************** * Call for Papers * *********************************************************************** New: Electronic Submission Guidelines Revised list of Invited Speakers ********************************************************************** IARCS, the Indian Association for Research in Computing Science, announces the 20th Annual FST TCS Conference in New Delhi. Tentatively planned satellite events include include two workshops: on Computational Geometry and on Advances in Programming Languages. Authors are invited to submit papers presenting original and unpublished research on **any** theoretical aspects of Computer Science. Papers in applied areas with a strong foundational emphasis are also welcome. The proceedings of the last six years' conferences (Springer-Verlag Lecture Notes in Computer Science volumes 880, 1026, 1180, 1346, 1530, 1738) give an idea of the kind of papers typically presented at FST TCS. Typical areas include (but are not restricted to): Automata, Languages and Computability Randomized and Approximation Algorithms Computational Geometry Computational Biology Combinatorial Optimization Graph and Network Algorithms Complexity Theory Parallel and Distributed Computing New Models of Computation Concurrent, Real-time and Hybrid Systems Logics of Programs and Modal Logics Database Theory and Information Retrieval Automated Reasoning, Rewrite Systems, and Applications Logic, Proof Theory, Model Theory and Applications Semantics of Programming Languages Static Analysis and Type Systems Theory of Functional and Constraint-based Programming Software Specification and Verification Cryptography and Security Protocols For an accepted paper to be included in the proceedings, one of the authors must commit to presenting the paper at the conference. Important Dates --------------- Deadline for Submission 31 May, 2000 Notification to Authors 15 August, 2000 Final Version of Accepted Papers due 15 September, 2000 Deadline for Early Registration 15 November, 2000 Submission Guidelines - --------------------- Authors may submit drafts of full papers or extended abstracts. Submissions are limited to 12 A4-size pages, with 1.5 inch top margin and other margins 1 inch wide with 11 point or larger font. Authors who feel that more details are necessary may include a clearly marked appendix which will be read at the discretion of the Programme Committee. Each paper should contain a short abstract. If available, e-mail addresses and fax numbers of the authors should be included. Electronic Submissions - -------------------- Electronic submission is very strongly encouraged. You may submit your paper using Rich Gerber's system START by visiting the URL for the conference and following the appropriate links. The URL for submissions is http://www.cse.iitd.ernet.in/~fsttcs20/START/www/submit.html In case you ar eunable to submit using START, self-contained uuencoded gzipped Postscript versions of the paper may be sent by e-mail to fsttcs20(a)cse.iitd.ernet.in In addition, the following information in ASCII format should be sent to this address in a **separate** e-mail: Title; authors; communicating author's name, address, and e-mail address and fax number if available; abstract of paper. Hard-Copy Submissions - --------------------- If electronic submission is not possible, authors may submit five (5) hard-copies of the paper by post to the following address: FST TCS 2000 Department of Computer Science and Engineering I.I.T., Delhi Hauz Khas New Delhi 110 016 INDIA Invited Speakers ---------------- Invited Speakers who have confirmed participation include: Peter Buneman (U Penn) Bernard Chazelle (Princeton) E. Allen Emerson (U Texas, Austin) Martin Groetschel (ZIB) Jose Meseguer (SRI) Philip Wadler (Bell Labs) Programme Committee ------------------- Pankaj Agarwal (Duke) Manindra Agrawal (IIT, Kanpur) Tetsuo Asano (JAIST) Vijay Chandru (IISc, Bangalore) Rance Cleaveland (Stony Brook) Anuj Dawar (Cambridge) Sampath Kannan (AT&T Research) Sanjiv Kapoor (IIT, Delhi) (Co-chair) Kamal Lodaya (IMSc, Chennai) Madhavan Mukund (CMI, Chennai) Gopalan Nadathur (Loyola) Seffi Naor (Bell Labs and Technion) Tobias Nipkow (TU Munich) Luke Ong (Oxford) C. Pandu Rangan (IIT, Chennai) Paritosh Pandya (TIFR) Benjamin Pierce (U Penn) Sanjiva Prasad (IIT, Delhi) (Co-chair) Sridhar Rajagopalan (IBM, Almaden) Abhiram Ranade (IIT, Mumbai) Dave Sands (Chalmers) A Prasad Sistla (U Illinois, Chicago) Michiel Smid (Magdeburg) Mandayam K. Srivas (SRI) Organized by ------------ Indian Institute of Technology, Delhi Hauz Khas, New Delhi 100 016. Organizing Committee ------------------- Sandeep Sen (chair) Naveen Garg (treasurer) S N Maheshwari Conference Site --------------- The Conference will take place at the India International Centre, 40 Lodhi Estate, Max Mueller Marg, New Delhi 110 003. Correspondence Address ---------------------- All correspondence regarding submissions may be addressed to FST TCS 2000 Department of Computer Science and Engineering I.I.T., Delhi Hauz Khas, New Delhi 110 016, INDIA Email: fsttcs20(a)cse.iitd.ernet.in Fax: +91 11 686 8765 Phone: +91 11 659 1294 / 659 1286 URL: http://www.cse.iitd.ernet.in/~fsttcs20 -- Sanjiva Prasad Associate Professor Department of Computer Science and Engineering sanjiva(a)cse.iitd.ernet.in Indian Institute of Technology, Delhi (Off) +91 11 659 1294 Hauz Khas, New Delhi 110016 (Res) +91 11 659 1684 INDIA (Fax) +91 11 686 8765 http://www.cse.iitd.ernet.in/~sanjiva

1 0