From robj@dcs.qmw.ac.uk Fri Mar 4 13:18:41 EST 1994 Article: 20955 of comp.ai Xref: glinda.oz.cs.cmu.edu comp.ai:20955 Newsgroups: comp.ai Path: honeydew.srv.cs.cmu.edu!rochester!udel!gatech!howland.reston.ans.net!EU.net!uknet!warwick!qmw-dcs!robj From: robj@dcs.qmw.ac.uk (Robert Johnson) Subject: TABLEAUX-94 (plain text) Message-ID: Sender: usenet@dcs.qmw.ac.uk (Usenet News System) Organization: Computer Science Dept, QMW, University of London Date: Fri, 4 Mar 1994 16:22:13 GMT Lines: 219 ============================================================================ T A B L E A U X - 9 4 ============================================================================ Call for participation and registration form for the Workshop on Theorem Proving with Tableaux and Related Methods. The workshop will take place on May 4-6, 1994 at Coseners House, Abingdon. TABLEAUX-94 is supported by the UK Science and Engineering Research Council (SERC). Abingdon is situated on the river Thames between London and Oxford. Travel details will be forwarded with a confirmation letter on receipt of completed applications. Program Committee ----------------- David Basin MPI Saarbr\"ucken, Germany Krysia Broda Imperial College, University of London, U.K. Marcello D'Agostino Imperial College, University of London,U.K. Melvin Fitting CUNY, U.S.A. Dov Gabbay Imperial College, University of London, U.K. Rajeev Gor\'e University of Manchester, U.K. Wilfrid Hodges QMW, University of London, U.K. Reiner H\"ahnle University of Karlsruhe, Germany Neil Murray Albany, U.S.A. Joachim Posegga University of Karlsruhe, Germany Steve Reeves QMW, University of London, U.K. Peter Schmitt University of Karlsruhe, Germany Camilla Schwind CNRS -- GIA, University of Marseille, France Lincoln Wallen University of Oxford, U.K. Graham Wrightson University of Newcastle, Australia Invited Speakers ---------------- Professors Jaakko Hintikka (Boston) and Robert Kowalski (Imperial) have been invited to speak at the workshop. Organising Committee -------------------- Rob Johnson Rajeev Gore Dept. of Computing Dept. of Computer Science Manchester Metropolitan University University of Manchester John Dalton Building Manchester, M13 9PL Manchester, M1 5GD, England England Fax: +44-61-247-1483 Fax: +44-61-275-6204 Tel: +44-61-247-1536 Tel: +44-61-275-6139 E-mail: robj@sun.com.mmu.ac.uk E-mail: rpg@cs.man.ac.uk Marcello D'Agostino Krysia Broda Department of Computing Department of Computing Imperial College Imperial College 180 Queen's Gate 180 Queen's Gate London London M13 9PL, UK M13 9PL, UK Fax: +44-71-581-8024 Fax: +44-71-581-8024 Tel: +44-71-589-5111 x4983 Tel: +44-71-589-5111 x7507 E-mail: mda@doc.ic.ac.uk E-mail: kb@doc.ic.ac.uk ========================================================================== Accepted papers --------------- Ulrich Assmann "Combining model elimination and resolution techniques" P. Baumgartner and U. Furbach "Model elimination without contrapositives and its application to ptt" Bernhard Beckert "Adding equality to semantic tableaux" Chaterine Belleann\'{e}e & Raoul Vorc'h "A linear tableau proof of the pigeon formulae using symmetry" Stefan Br\"{u}ning "Exploiting equivalences in connection calculi" Arthur Buchsbaum & Tarcisio Pequeno "Automated deduction with non-classical negation" Jean Goubault "A BDD-based skolemization procedure" Mark Grundy "A stepwise mapping from resolution to tableau calculi" J\'{o}rg Hudelmaier "On a contraction-free sequent calculus for the modal logic s4" Robert Johnson "Tableau structure prediction" Stefan Klingenbeck & Reiner Haehnle "Semantic Tableaux with ordering restrictions" Miyuki Koshimura & Ryuzo Hasegawa "Modal propositional tableaux in a model generation theorem-prover" Marta Cialdea Mayer & Fiora Pirri "Propositional abduction in modal logic" P. Miglioli, U. Moscato, M. Ornaghi "How to avoid duplications in refutation systems for intuitionistic and Kuroda logic" Marco Mondadori "Efficient inverse tableaux" Jeremy Pitt & Jim Cunningham "Logical animation with the system KE" Vincent Vialard "Handling models in propositional logic" Raoul Vorc'h "A connection-based point of view of propositional cut elimination" Kevin Wallace & Graham Wrightson "Regressive merging in model elimination tableau-based theorem provers" Cristoph Weidenbach "First order tableaux with sorts" All accepted papers will be published in the workshop proceedings which will be distributed at Abingdon. It is planned to publish a selection from the accepted papers in the Journal of Logic and Computation, and a further selection in the Bulletin of the Interest Group in Pure and Applied Logics. In addition to the presentation of the accepted papers there will be sessions set aside for topic-related discussions. If you have a topic that you would like to be discussed during one of these sessions then please send details to Rob Johnson (address above - email preferred). ========================================================================== The conference registration fee is 100 UKP (UK pounds sterling) payable in advance to the registration address below no later than *28th March*. A late registration fee supplement (40 UKP) will be payable if registering after the 15th of April. Registration cannot be considered finalised until receipt of the fee. Please return a cheque or money order drawn on a UK bank in UK pounds sterling, payable to Imperial College, to cover registration with the completed registration form. To help us to plan your stay please indicate the dates of your stay, and your accommodation preferences. Accommodation will be distributed on a first-come, first-served basis. It may not be possible to assign all attendees their first choice of room. Each price quoted is in UK pounds sterling and covers a 3 night stay (the 3rd, 4th and 5th of May) with all meals included. There are four types of room available: Single room without shower (SR) 218 UKP Single room with shower (SRS) 250 UKP Shared Double room per person without shower (DR) 190 UKP Shared Double room per person with shower (DRS) 213 UKP ************************************************************************* N.B. As a result of SERC sponsorship of this event we expect to be able to subsidise the accommodation rates by a further 60-85 UKP depending on numbers. ************************************************************************* If overnight accommodation is not required a day rate is payable of 24 UKP per day which covers the cost of the seminar room, tea/coffee and lunch. In the event of cancellation a proportional fee will be payable as determined by a sliding scale (based on the lateness of cancellation). An invoice for accommodation will be issued on receipt of the registration fee. Payment for accommodation is expected at the start of the workshop. Registration address: Hard copy: TABLEAUX-94, Krysia Broda, Department of Computing, Imperial College, 180 Queen's gate, London SW7 2BZ, U.K. ----------- cut here and return this form to registration address ------------ Registration form for T A B L E A U X - 9 4 Personal Information: Family name: ................................ First name: .............. Affiliation: ........................................................... ........................................................... Address: ........................................................... ........................................................... ........................................................... ........................................................... E-mail: ........................................................... Tel.: .......................... Fax.: .......................... Accompanying person(s): ................................................ My arrival date will be: ............................................. My departure date will be: ............................................. Special dietary requirements: .......................................... Overnight accommodation type: ___ OR Day accommodation for ___ days. Second choice accommodation type: ___ For any administrative queries regarding registration or bookings please contact Fatima Dargam, Email: fccd@doc.ic.ac.uk Tel: +44-(0)71-5895111 ext. 5023 Fax: +44-(0)71-5818024. -- Robert Johnson Applied Logic Group | email:robj@dcs.qmw.ac.uk Department of Computer Science | tel. : +44-71-975-5241 Queen Mary and Westfield College | fax : +44-81-980-6533 Article 20956 of comp.ai: Xref: glinda.oz.cs.cmu.edu comp.ai:20956 Newsgroups: comp.ai Path: honeydew.srv.cs.cmu.edu!rochester!udel!MathWorks.Com!europa.eng.gtefsd.com!howland.reston.ans.net!news.moneng.mei.com!uwm.edu!math.ohio-state.edu!jussieu.fr!univ-lyon1.fr!zaphod.crihan.fr!warwick!qmw-dcs!robj From: robj@dcs.qmw.ac.uk (Robert Johnson) Subject: TABLEAUX-94 (LaTeX) Message-ID: Sender: usenet@dcs.qmw.ac.uk (Usenet News System) Organization: Computer Science Dept, QMW, University of London Date: Fri, 4 Mar 1994 16:24:39 GMT Lines: 261 \documentstyle[10pt,fullpage]{article} \begin{document} \begin{center} {\LARGE \bf Call For Participation TABLEAUX-94\newline}\\ %\vspace{0.2in} \bf Call for participation and registration form for the Workshop on Theorem Proving with Tableaux and Related Methods.\rm\newline May 4-6, 1994, Coseners House, Abingdon, UK.\newline\newline TABLEAUX-94 is supported by the UK Science and Engineering Research Council (SERC).\newline \end{center} \noindent Abingdon is situated on the river Thames between London and Oxford. Travel details will be forwarded with a confirmation letter on receipt of completed applications. \newline\newline \noindent \underline{Program Committee}\\ \begin{center} \begin{tabular}{ll} David Basin &MPI Saarbr\"ucken, Germany\\ Krysia Broda &Imperial College, University of London, U.K.\\ Marcello D'Agostino &Imperial College, University of London, U.K.\\ Melvin Fitting &CUNY, U.S.A.\\ Dov Gabbay &Imperial College, University of London, U.K.\\ Rajeev Gor\'e &University of Manchester, U.K.\\ Wilfrid Hodges &QMW, University of London, U.K.\\ Reiner H\"ahnle &University of Karlsruhe, Germany\\ Neil Murray &Albany, U.S.A. \\ Joachim Posegga &University of Karlsruhe, Germany\\ Steve Reeves &QMW, University of London, U.K.\\ Peter Schmitt &University of Karlsruhe, Germany\\ Camilla Schwind &CNRS -- GIA, University of Marseille, France\\ Lincoln Wallen &University of Oxford, U.K.\\ Graham Wrightson &University of Newcastle, Australia \end{tabular}\newline\newline \end{center} \noindent \underline{Invited Speakers}\newline\newline Professors Jaakko Hintikka (Boston) and Robert Kowalski (Imperial) have been invited to speak at the workshop.\newline\newline \noindent \underline{Organising Committee}\newline\newline \begin{tabular}{ll} Krysia Broda & Dept. of Computing, Imperial College, 180 Queen's Gate, London, SW7 2BZ, UK\\ &Fax: +44-71-581-8024, Tel: +44-71-589-5111 x7507, E-mail: kb@doc.ic.ac.uk\\ Marcello D'Agostino & Dept. of Computing, Imperial College, 180 Queen's Gate, London, SW7 2BZ, UK\\ &Fax: +44-71-581-8024, Tel: +44-71-589-5111 x4983, E-mail: mda@doc.ic.ac.uk\\ Rajeev Gor\'{e} & Dept. of Computer Science, University of Manchester, Manchester, M13 9PL, UK\\ &Fax: +44-61-275-6204, Tel: +44-61-275-6139, E-mail: rpg@cs.man.ac.uk \\ Rob Johnson & Dept. of Computing, Manchester Metropolitan University, Manchester, M1 5GD, UK\\ &Fax: +44-61-247-1483, Tel: +44-61-247-1536, Email: robj@sun.com.mmu.ac.uk \end{tabular}\newline\newline \newpage \noindent \underline{Accepted papers}\newline \begin{tabular}{lp{3.in}} \noindent Ulrich Assmann &`Combining model elimination and resolution techniques' \\ \noindent P. Baumgartner and U. Furbach &`Model elimination without contrapositives and its \mbox{application} to ptt'\\ \noindent Bernhard Beckert &`Adding equality to semantic tableaux'\\ \noindent Chaterine Belleann\'{e}e and Raoul Vorc'h &`A linear tableau proof of the pigeon formulae \mbox{using} symmetry'\\ \noindent Stefan Br\"{u}ning &`Exploiting equivalences in connection calculi'\\ \noindent Arthur Buchsbaum and Tarcisio Pequeno &`Automated deduction with non-classical negation'\\ \noindent Jean Goubault &`A BDD-based skolemization procedure'\\ \noindent Mark Grundy &`A stepwise mapping from resolution to tableau calculi'\\ \noindent J\"{o}rg Hudelmaier &`On a contraction-free sequent calculus for the modal logic S4'\\ \noindent Robert Johnson &`Tableau structure prediction'\\ \noindent Stefan Klingenbeck and Reiner H\"{a}hnle &`Semantic Tableaux with ordering restrictions'\\ \noindent Miyuki Koshimura and Ryuzo Hasegawa &`Modal propositional tableaux in a model \mbox{generation} theorem-prover'\\ \noindent Marta Cialdea Mayer and Fiora Pirri &`Propositional abduction in modal logic'\\ \noindent P. Miglioli, U. Moscato, M. Ornaghi &`How to avoid duplications in refutation systems for \mbox{intuitionistic} and Kuroda logic'\\ \noindent Marco Mondadori &`Efficient inverse tableaux'\\ \noindent Jeremy Pitt and Jim Cunningham &`Logical animation with the system KE'\\ \noindent Vincent Vialard &`Handling models in propositional logic'\\ \noindent Raoul Vorc'h &`A connection-based point of view of propositional cut elimination'\\ \noindent Kevin Wallace and Graham Wrightson &`Regressive merging in model elimination tableau-based theorem provers' \\ \noindent Cristoph Weidenbach &`First order tableaux with sorts' \end{tabular}\newline\newline \normalsize \noindent All accepted papers will be published in the workshop proceedings which will be distributed at Abingdon. It is planned to publish a selection from the accepted papers in the Journal of Logic and Computation, and a further selection in the Bulletin of the Interest Group in Pure and Applied Logics. \newline \noindent In addition to the presentation of the accepted papers there will be sessions set aside for topic-related discussions. If you have a topic that you would like to be discussed during one of these sessions then please send details to Rob Johnson (address above - email preferred). \noindent If you have any queries of a technical nature please contact any member of the organising committee (addresses above) who will be happy to help you.\newline \newpage \noindent \underline{Registration Details}\newline\newline The conference registration fee is \pounds 100 (UK pounds sterling) payable in advance to the registration address below no later than \underline{\bf 28th March}. A late registration fee supplement (\pounds 40) will be payable if registering after the 15th of April. Registration cannot be considered finalised until receipt of the fee. Please return a cheque or money order drawn on a UK bank in UK pounds sterling, payable to Imperial College, to cover registration with the completed registration form. \noindent To help us to plan your stay please indicate the dates of your stay, and your accommodation preferences. Accommodation will be distributed on a first-come, first-served basis since it may not be possible to assign all attendees their first choice of room.\newline Each price quoted is in UK pounds sterling and covers a 3 night stay (the 3rd, 4th, and 5th of May) with all meals included.\newline There are four types of room available:\newline \begin{center} \begin{tabular}{lll} Single room without shower &(SR) &\pounds 218 \\ Single room with shower &(SRS) &\pounds 250 \\ Shared twin room without shower, per person &(DR) &\pounds 190 \\ Shared twin room with shower, per person &(DRS) &\pounds 213 \end{tabular}\newline\newline \end{center} \noindent \bf As a result of SERC sponsorship of this event we expect to be able to subsidise the accommodation rates by a further \pounds 60-\pounds 85 depending on numbers.\rm\newline If overnight accommodation is not required then a day rate of \pounds 24 is payable which covers the cost of the seminar room, tea/coffee and lunch. In the event of cancellation a proportional fee will be payable as determined by a sliding scale (based on the lateness of cancellation). \noindent An invoice will be sent for your accommodation, and payment is expected at the start of the workshop. \newline \begin{center} \begin{tabular}{lll} Registration address: &Hard copy: &TABLEAUX-94, Krysia Broda, Department of Computing,\\ & &Imperial College, 180 Queen's gate, London SW7 2BZ, U.K. \end{tabular} \end{center} \noindent \underline{\bf Registration form}\newline \vspace{-.4in} \begin{center} \begin{tabular}{c} \hspace*{\textwidth}\\ Family name: \hrulefill \\ First name: \hrulefill \\ Affiliation: \hrulefill \\ \hrulefill \\ Postal address: \hrulefill \\ \ \hrulefill\ \\ \ \hrulefill\ \\ \ \hrulefill\ \\ \noindent E-mail: \hrulefill \\ Tel.: \hrulefill \\ Fax.: \hrulefill \\ \noindent Accompanying person(s): \hrulefill \\ My arrival date will be: \hrulefill \\ My departure date will be: \hrulefill \\ Special dietary requirements: \hrulefill \\ \ \end{tabular} \end{center} Overnight accommodation type: $\ldots\ldots$ OR day accommodation rate for $\ldots\ldots$ days.\newline Second choice accommodation type: $\ldots\ldots$ \noindent For any administrative queries regarding registration or bookings please contact Fatima Dargam, Email: fccd@doc.ic.ac.uk Tel: +44-(0)71-5895111 ext. 5023 Fax: +44-(0)71-5818024. \end{document} -- Robert Johnson Applied Logic Group | email:robj@dcs.qmw.ac.uk Department of Computer Science | tel. : +44-71-975-5241 Queen Mary and Westfield College | fax : +44-81-980-6533 Article 21138 of comp.ai: Xref: glinda.oz.cs.cmu.edu comp.ai:21138 Newsgroups: comp.ai Path: honeydew.srv.cs.cmu.edu!rochester!udel!MathWorks.Com!europa.eng.gtefsd.com!howland.reston.ans.net!EU.net!uknet!qmw-dcs!robj From: robj@dcs.qmw.ac.uk (Robert Johnson) Subject: TABLEAUX-94 Message-ID: Sender: usenet@dcs.qmw.ac.uk (Usenet News System) Organization: Computer Science Dept, QMW, University of London Date: Wed, 16 Mar 1994 11:50:14 GMT Lines: 477 ============================================================================ T A B L E A U X - 9 4 ============================================================================ Call for participation and registration form for the Workshop on Theorem Proving with Tableaux and Related Methods. The workshop will take place on May 4-6, 1994 at Coseners House, Abingdon. (***LaTeX version appended to this message***) TABLEAUX-94 is supported by the UK Science and Engineering Research Council (SERC). Abingdon is situated on the river Thames between London and Oxford. Travel details will be forwarded with a confirmation letter on receipt of completed applications. Program Committee ----------------- David Basin MPI Saarbr\"ucken, Germany Krysia Broda Imperial College, University of London, U.K. Marcello D'Agostino Imperial College, University of London,U.K. Melvin Fitting CUNY, U.S.A. Dov Gabbay Imperial College, University of London, U.K. Rajeev Gor\'e University of Manchester, U.K. Wilfrid Hodges QMW, University of London, U.K. Reiner H\"ahnle University of Karlsruhe, Germany Neil Murray Albany, U.S.A. Joachim Posegga University of Karlsruhe, Germany Steve Reeves QMW, University of London, U.K. Peter Schmitt University of Karlsruhe, Germany Camilla Schwind CNRS -- GIA, University of Marseille, France Lincoln Wallen University of Oxford, U.K. Graham Wrightson University of Newcastle, Australia Invited Speakers ---------------- Professors Jaakko Hintikka (Boston) and Robert Kowalski (Imperial) have been invited to speak at the workshop. Organising Committee -------------------- Rob Johnson Rajeev Gore Dept. of Computing Dept. of Computer Science Manchester Metropolitan University University of Manchester John Dalton Building Manchester, M13 9PL Manchester, M1 5GD, England England Fax: +44-61-247-1483 Fax: +44-61-275-6204 Tel: +44-61-247-1536 Tel: +44-61-275-6139 E-mail: robj@sun.com.mmu.ac.uk E-mail: rpg@cs.man.ac.uk Marcello D'Agostino Krysia Broda Department of Computing Department of Computing Imperial College Imperial College 180 Queen's Gate 180 Queen's Gate London London M13 9PL, UK M13 9PL, UK Fax: +44-71-581-8024 Fax: +44-71-581-8024 Tel: +44-71-589-5111 x4983 Tel: +44-71-589-5111 x7507 E-mail: mda@doc.ic.ac.uk E-mail: kb@doc.ic.ac.uk ========================================================================== Accepted papers --------------- Ulrich Assmann "Combining model elimination and resolution techniques" P. Baumgartner and U. Furbach "Model elimination without contrapositives and its application to ptt" Bernhard Beckert "Adding equality to semantic tableaux" Chaterine Belleann\'{e}e & Raoul Vorc'h "A linear tableau proof of the pigeon formulae using symmetry" Stefan Br\"{u}ning "Exploiting equivalences in connection calculi" Arthur Buchsbaum & Tarcisio Pequeno "Automated deduction with non-classical negation" Jean Goubault "A BDD-based skolemization procedure" Mark Grundy "A stepwise mapping from resolution to tableau calculi" J\'{o}rg Hudelmaier "On a contraction-free sequent calculus for the modal logic s4" Robert Johnson "Tableau structure prediction" Stefan Klingenbeck & Reiner Haehnle "Semantic Tableaux with ordering restrictions" Miyuki Koshimura & Ryuzo Hasegawa "Modal propositional tableaux in a model generation theorem-prover" Marta Cialdea Mayer & Fiora Pirri "Propositional abduction in modal logic" P. Miglioli, U. Moscato, M. Ornaghi "How to avoid duplications in refutation systems for intuitionistic and Kuroda logic" Marco Mondadori "Efficient inverse tableaux" Jeremy Pitt & Jim Cunningham "Logical animation with the system KE" Vincent Vialard "Handling models in propositional logic" Raoul Vorc'h "A connection-based point of view of propositional cut elimination" Kevin Wallace & Graham Wrightson "Regressive merging in model elimination tableau-based theorem provers" Cristoph Weidenbach "First order tableaux with sorts" All accepted papers will be published in the workshop proceedings which will be distributed at Abingdon. It is planned to publish a selection from the accepted papers in the Journal of Logic and Computation, and a further selection in the Bulletin of the Interest Group in Pure and Applied Logics. In addition to the presentation of the accepted papers there will be sessions set aside for topic-related discussions. If you have a topic that you would like to be discussed during one of these sessions then please send details to Rob Johnson (address above - email preferred). ========================================================================== The conference registration fee is 100 UKP (UK pounds sterling) payable in advance to the registration address below no later than *28th March*. A late registration fee supplement (40 UKP) will be payable if registering after the 15th of April. Registration cannot be considered finalised until receipt of the fee. Please return a cheque or money order drawn on a UK bank in UK pounds sterling, payable to Imperial College, to cover registration with the completed registration form. To help us to plan your stay please indicate the dates of your stay, and your accommodation preferences. Accommodation will be distributed on a first-come, first-served basis. It may not be possible to assign all attendees their first choice of room. Each price quoted is in UK pounds sterling and covers a 3 night stay (the 3rd, 4th and 5th of May) with all meals included. There are four types of room available: Single room without shower (SR) 218 UKP Single room with shower (SRS) 250 UKP Shared Double room per person without shower (DR) 190 UKP Shared Double room per person with shower (DRS) 213 UKP ************************************************************************* N.B. As a result of SERC sponsorship of this event we expect to be able to subsidise the accommodation rates by a further 60-85 UKP depending on numbers. ************************************************************************* If overnight accommodation is not required a day rate is payable of 24 UKP per day which covers the cost of the seminar room, tea/coffee and lunch. In the event of cancellation a proportional fee will be payable as determined by a sliding scale (based on the lateness of cancellation). An invoice for accommodation will be issued on receipt of the registration fee. Payment for accommodation is expected at the start of the workshop. Registration address: Hard copy: TABLEAUX-94, Krysia Broda, Department of Computing, Imperial College, 180 Queen's gate, London SW7 2BZ, U.K. ----------- cut here and return this form to registration address ------------ Registration form for T A B L E A U X - 9 4 Personal Information: Family name: ................................ First name: .............. Affiliation: ........................................................... ........................................................... Address: ........................................................... ........................................................... ........................................................... ........................................................... E-mail: ........................................................... Tel.: .......................... Fax.: .......................... Accompanying person(s): ................................................ My arrival date will be: ............................................. My departure date will be: ............................................. Special dietary requirements: .......................................... Overnight accommodation type: ___ OR Day accommodation for ___ days. Second choice accommodation type: ___ For any administrative queries regarding registration or bookings please contact Fatima Dargam, Email: fccd@doc.ic.ac.uk Tel: +44-(0)71-5895111 ext. 5023 Fax: +44-(0)71-5818024. \documentstyle[10pt,fullpage]{article} \begin{document} \begin{center} {\LARGE \bf Call For Participation TABLEAUX-94\newline}\\ %\vspace{0.2in} \bf Call for participation and registration form for the Workshop on Theorem Proving with Tableaux and Related Methods.\rm\newline May 4-6, 1994, Coseners House, Abingdon, UK.\newline\newline TABLEAUX-94 is supported by the UK Science and Engineering Research Council (SERC).\newline \end{center} \noindent Abingdon is situated on the river Thames between London and Oxford. Travel details will be forwarded with a confirmation letter on receipt of completed applications. \newline\newline \noindent \underline{Program Committee}\\ \begin{center} \begin{tabular}{ll} David Basin &MPI Saarbr\"ucken, Germany\\ Krysia Broda &Imperial College, University of London, U.K.\\ Marcello D'Agostino &Imperial College, University of London, U.K.\\ Melvin Fitting &CUNY, U.S.A.\\ Dov Gabbay &Imperial College, University of London, U.K.\\ Rajeev Gor\'e &University of Manchester, U.K.\\ Wilfrid Hodges &QMW, University of London, U.K.\\ Reiner H\"ahnle &University of Karlsruhe, Germany\\ Neil Murray &Albany, U.S.A. \\ Joachim Posegga &University of Karlsruhe, Germany\\ Steve Reeves &QMW, University of London, U.K.\\ Peter Schmitt &University of Karlsruhe, Germany\\ Camilla Schwind &CNRS -- GIA, University of Marseille, France\\ Lincoln Wallen &University of Oxford, U.K.\\ Graham Wrightson &University of Newcastle, Australia \end{tabular}\newline\newline \end{center} \noindent \underline{Invited Speakers}\newline\newline Professors Jaakko Hintikka (Boston) and Robert Kowalski (Imperial) have been invited to speak at the workshop.\newline\newline \noindent \underline{Organising Committee}\newline\newline \begin{tabular}{ll} Krysia Broda & Dept. of Computing, Imperial College, 180 Queen's Gate, London, SW7 2BZ, UK\\ &Fax: +44-71-581-8024, Tel: +44-71-589-5111 x7507, E-mail: kb@doc.ic.ac.uk\\ Marcello D'Agostino & Dept. of Computing, Imperial College, 180 Queen's Gate, London, SW7 2BZ, UK\\ &Fax: +44-71-581-8024, Tel: +44-71-589-5111 x4983, E-mail: mda@doc.ic.ac.uk\\ Rajeev Gor\'{e} & Dept. of Computer Science, University of Manchester, Manchester, M13 9PL, UK\\ &Fax: +44-61-275-6204, Tel: +44-61-275-6139, E-mail: rpg@cs.man.ac.uk \\ Rob Johnson & Dept. of Computing, Manchester Metropolitan University, Manchester, M1 5GD, UK\\ &Fax: +44-61-247-1483, Tel: +44-61-247-1536, Email: robj@sun.com.mmu.ac.uk \end{tabular}\newline\newline \newpage \noindent \underline{Accepted papers}\newline \begin{tabular}{lp{3.in}} \noindent Ulrich Assmann &`Combining model elimination and resolution techniques' \\ \noindent P. Baumgartner and U. Furbach &`Model elimination without contrapositives and its \mbox{application} to ptt'\\ \noindent Bernhard Beckert &`Adding equality to semantic tableaux'\\ \noindent Chaterine Belleann\'{e}e and Raoul Vorc'h &`A linear tableau proof of the pigeon formulae \mbox{using} symmetry'\\ \noindent Stefan Br\"{u}ning &`Exploiting equivalences in connection calculi'\\ \noindent Arthur Buchsbaum and Tarcisio Pequeno &`Automated deduction with non-classical negation'\\ \noindent Jean Goubault &`A BDD-based skolemization procedure'\\ \noindent Mark Grundy &`A stepwise mapping from resolution to tableau calculi'\\ \noindent J\"{o}rg Hudelmaier &`On a contraction-free sequent calculus for the modal logic S4'\\ \noindent Robert Johnson &`Tableau structure prediction'\\ \noindent Stefan Klingenbeck and Reiner H\"{a}hnle &`Semantic Tableaux with ordering restrictions'\\ \noindent Miyuki Koshimura and Ryuzo Hasegawa &`Modal propositional tableaux in a model \mbox{generation} theorem-prover'\\ \noindent Marta Cialdea Mayer and Fiora Pirri &`Propositional abduction in modal logic'\\ \noindent P. Miglioli, U. Moscato, M. Ornaghi &`How to avoid duplications in refutation systems for \mbox{intuitionistic} and Kuroda logic'\\ \noindent Marco Mondadori &`Efficient inverse tableaux'\\ \noindent Jeremy Pitt and Jim Cunningham &`Logical animation with the system KE'\\ \noindent Vincent Vialard &`Handling models in propositional logic'\\ \noindent Raoul Vorc'h &`A connection-based point of view of propositional cut elimination'\\ \noindent Kevin Wallace and Graham Wrightson &`Regressive merging in model elimination tableau-based theorem provers' \\ \noindent Cristoph Weidenbach &`First order tableaux with sorts' \end{tabular}\newline\newline \normalsize \noindent All accepted papers will be published in the workshop proceedings which will be distributed at Abingdon. It is planned to publish a selection from the accepted papers in the Journal of Logic and Computation, and a further selection in the Bulletin of the Interest Group in Pure and Applied Logics. \newline \noindent In addition to the presentation of the accepted papers there will be sessions set aside for topic-related discussions. If you have a topic that you would like to be discussed during one of these sessions then please send details to Rob Johnson (address above - email preferred). \noindent If you have any queries of a technical nature please contact any member of the organising committee (addresses above) who will be happy to help you.\newline \newpage \noindent \underline{Registration Details}\newline\newline The conference registration fee is \pounds 100 (UK pounds sterling) payable in advance to the registration address below no later than \underline{\bf 28th March}. A late registration fee supplement (\pounds 40) will be payable if registering after the 15th of April. Registration cannot be considered finalised until receipt of the fee. Please return a cheque or money order drawn on a UK bank in UK pounds sterling, payable to Imperial College, to cover registration with the completed registration form. \noindent To help us to plan your stay please indicate the dates of your stay, and your accommodation preferences. Accommodation will be distributed on a first-come, first-served basis since it may not be possible to assign all attendees their first choice of room.\newline Each price quoted is in UK pounds sterling and covers a 3 night stay (the 3rd, 4th, and 5th of May) with all meals included.\newline There are four types of room available:\newline \begin{center} \begin{tabular}{lll} Single room without shower &(SR) &\pounds 218 \\ Single room with shower &(SRS) &\pounds 250 \\ Shared twin room without shower, per person &(DR) &\pounds 190 \\ Shared twin room with shower, per person &(DRS) &\pounds 213 \end{tabular}\newline\newline \end{center} \noindent \bf As a result of SERC sponsorship of this event we expect to be able to subsidise the accommodation rates by a further \pounds 60-\pounds 85 depending on numbers.\rm\newline If overnight accommodation is not required then a day rate of \pounds 24 is payable which covers the cost of the seminar room, tea/coffee and lunch. In the event of cancellation a proportional fee will be payable as determined by a sliding scale (based on the lateness of cancellation). \noindent An invoice will be sent for your accommodation, and payment is expected at the start of the workshop. \newline \begin{center} \begin{tabular}{lll} Registration address: &Hard copy: &TABLEAUX-94, Krysia Broda, Department of Computing,\\ & &Imperial College, 180 Queen's gate, London SW7 2BZ, U.K. \end{tabular} \end{center} \noindent \underline{\bf Registration form}\newline \vspace{-.4in} \begin{center} \begin{tabular}{c} \hspace*{\textwidth}\\ Family name: \hrulefill \\ First name: \hrulefill \\ Affiliation: \hrulefill \\ \hrulefill \\ Postal address: \hrulefill \\ \ \hrulefill\ \\ \ \hrulefill\ \\ \ \hrulefill\ \\ \noindent E-mail: \hrulefill \\ Tel.: \hrulefill \\ Fax.: \hrulefill \\ \noindent Accompanying person(s): \hrulefill \\ My arrival date will be: \hrulefill \\ My departure date will be: \hrulefill \\ Special dietary requirements: \hrulefill \\ \ \end{tabular} \end{center} Overnight accommodation type: $\ldots\ldots$ OR day accommodation rate for $\ldots\ldots$ days.\newline Second choice accommodation type: $\ldots\ldots$ \noindent For any administrative queries regarding registration or bookings please contact Fatima Dargam, Email: fccd@doc.ic.ac.uk Tel: +44-(0)71-5895111 ext. 5023 Fax: +44-(0)71-5818024. \end{document} -- Robert Johnson Applied Logic Group | email:robj@dcs.qmw.ac.uk Department of Computer Science | tel. : +44-71-975-5241 Queen Mary and Westfield College | fax : +44-81-980-6533