Community News
List of News:


AAAI-05
Announcement about Alternative Programming

Communicated by Andrew Gleibman

 
To: ALP Newsletter readers
Gentlemen,

I would like to get your feedback about the perspectives of the "Alternative Programming" project, announced at the AAAI-05 Workshop on Inference for Textual Question Answering (see the links below).

The project is related to reasoning by analogy using natural language expressions in a Logic Programing framework. It suggests a specific way of exploiting the natural semantics of the existing words and phrases without writing the program code, via alignment and subsequent generalization of natural texts (which can be NL sentences, fragments of
biological sequences, or other texts of unrestricted nature; see Sections 4-6 in the paper [2]).

As the unusual (and innovative) feature of the project, it suggests to do first order logic without the concept of predicate and to do text analysis, interpretation and synthesis without the concept of formal grammar. (Special alignment and unification of the generalized texts are used instead). I believe the project can provide a more deep modeling of the text
meaning than what can be achieved using the handcrafted semantic formalisms applied today; also I hope it can be applied for a better understanding of the meaning and the interaction of genetic sequences.

Thank you in advance if you can provide some critiques, recommendations, or another feedback about the project.

Sincerely yours,
Dr. Andrew Gleibman
Sampletalk Technologies
Email address: admin@sampletalk.com
Phone: +972-4-9590758


Links and references:

[1] Brief presentation of the project:
      http://www.sampletalk.8m.com/AAAI05tlk.pps

[2] Detailed presentation of the project: A. Gleibman. Knowledge Representation via Verbal Description Generalization: Alternative Programming in Sampletalk Language. In: Workshop on Inference for Textual Question Answering. July 09, 2005 – Pittsburgh, Pennsylvania, pp. 59-68. AAAI-05 - the Twentieth National Conference on Artificial Intelligence. See this publication online at
http://www.hlt.utdallas.edu/workshop2005/papers/WS505GleibmanA.pdf


[3] Math formulation of the project ideas: A. Gleibman. First Order Text Calculus: Algorithmic Properties and Descriptive Power. (In publishers). See
http://sampletalk.8m.com/FOTC2_LNCS.doc

[4] More detailed description of the Sampletalk language and the Sampletalk compiler:
http://www.sampletalk.8m.com



SICStus Prolog in the International Space Station

Communicated by Vicki Carleson

 
Clarissa, a voice-enabled procedure browser developed at NASA Ames, was successfully tested for the first time today by astronaut John Phillips on the International Space Station. To the best of our knowledge, this is the first ever use of a spoken dialogue system in space. During the test, Phillips completed the interactive Clarissa training procedure, which exercises all the main system functionality.

For more information, including on-line conference papers and technical reports, see the Clarissa home page at http://www.ic.arc.nasa.gov/projects/clarissa/.

There is a short non-technical write-up in the current issue of New Scientist, at http://www.newscientist.com/article.ns?id=dn7584.
The current experimental version of Clarissa runs on a standard ISS laptop, and browses procedures written in an XML format. The markup language includes constructs for branch points, conditional steps, querying the user for numerical values, and linking to subprocedures. For our initial experiments, five procedures have been converted into Clarissa-compatible XML form: three for sample collection and testing of the Station's potable water supply, and two for space suit checkout.

The system has a vocabulary of about 260 words, and supports about 75 different commands. The user can scroll forwards or backwards, move to an arbitrary new step, preview or read out a non-current step without losing their place in the procedure, open a sub-procedure, and read safety-critical portions of the procedure in a mode which checks aggressively that steps have not been skipped. Other commands include support for recording, playing and deleting voice notes, setting timers and alarms, and querying status. Any misrecognition can be undone or corrected, using a command like "undo" or "no, I said go to step fourteen".

Speech recognition is in "open mic" mode. In the deployed system, the error rate for distinguishing between voice commands and non-system-directed speech is about 10%; together with Jean-Michel Renders from Xerox Research Center Europe, we have developed experimental methods using Support Vector Machines, which reduce the error rate to about 5%. This work may be integrated into a future version of Clarissa. Spoken output is performed using a recorded voice.

Clarissa has been implemented mainly using SICStus Prolog and a speech recognition toolkit provided by Nuance Communications. Application-specific spoken command grammars were constructed using the Regulus platform. Other programming languages and software packages used include Java, C, and SRI International's Gemini and Open Agent Architecture.


International Journal of Human-Computer Studies
Knowledge Representation with Ontologies: Present Challenges - Future Possibilities

 
Guest Editors: Christopher Brewster and Kieron O'Hara
http://www.dcs.shef.ac.uk/~kiffer/IJHCS.html

Recently, we have seen an explosion of interest in ontologies as artifacts to represent human knowledge and as critical components in knowledge management, the Semantic Web, business-to-business applications, and several other application areas. Various research communities commonly assume that ontologies are the appropriate modelling structure for representing knowledge. However, little discussion has occurred regarding the actual range of knowledge an ontology can successfully represent.

What are the limits of ontology-based representation? Some types of knowledge are extremely suited to ontological representation, such as taxonomic information, but clearly this isn't always the case. We can't always easily represent certain types of knowledge (for example, skills or distributed knowledge), nor easily transform types of representation into ontology-appropriate formats (for example, diagrammatic knowledge). And with the expanded recognition of multiple modalities, does our vision of an ontology change? Can we speak of multi-media ontologies? This is of even greater significance as Knowledge Management recognises more exactly the range of knowledge that is embodied in an organisation.

Most, but not all, definitions of "ontology" insist that an ontology specifically represents common, shared conceptual structures. Does this requirement for publicity help guarantee adequacy? And if so, can we talk of personal ontologies? If ontologies have to represent knowledge relatively coarsely or approximately, how much is this likely to matter in realistic contexts? Will scale be a problem?

This special issue seeks outstanding papers on the potential and the limits of ontologies in the broad range of fields in which they have come to play a major part. We wish to stimulate discussion so as to facilitate a vision of where ontologies and knowledge representations are heading.

Contributions should be original and unpublished studies. We are interested in both theoretical and practical research concerning the limits and value of ontologies, including: evaluations of the practical applicability of ontology based technologies; their limits and potentials; issues and solutions for problematic real-world applications; tools and techniques for ontology building and maintenance. Papers concerning the following topics will be particularly welcome, though any other topic relevant to the theme of the limits and value of ontological representations would be acceptable:
Important Dates
Paper submissions:        1 September, 2005 (negotiable)
Notification of acceptance:    1 November, 2005
Final versions due:        1 February, 2006
Journal publication:        Summer, 2006

Format for submissions
Paper should be formatted in accordance with IJHCS guidelines available in the journal, or at http://authors.elsevier.com/journal/ijhcs and should be between 6000-8000 words in length. Authors of submitted journals may be invited to take part in the review process.

Submission should be made in pdf or word format electronically to C.Brewster@dcs.shef.ac.uk.



Information and Computation
Open Access Experiment

Communicated by Moshe Vardi

The Publisher and Editorial Board of Information and Computation are pleased to announce that for one year, effective immediately, online access to all journal issues back to 1995 will be available without charge.  This includes unrestricted downloading of articles in pdf format. 
Journal articles may be obtained through the journal's web site http://theory.csail.mit.edu/~iandc or Elsevier's Sciencedirect at
http://www.sciencedirect.com/science/journal/08905401

At the end of the year, the retrieval traffic during the open access period will be evaluated as future subscription policies are considered.
Albert R. Meyer, Editor-in-Chief, MIT Computer Science & AI Lab
Chris Leonard, Publishing Editor, Elsevier
Moshe Y. vardi, Associate Editor, Rice University



Book Announcement
Advanced Topics in Types and Programming Languages
Edited by Benjamin C. Pierce

 Communicated by David Weininger
 
The study of type systems for programming languages now touches many areas of computer science, from language design and implementation to software engineering, network security, databases, and analysis of concurrent and distributed systems.  This book offers accessible introductions to key ideas in the field, with contributions by experts on each topic.

The topics covered include precise type analyses, which extend simple type systems to give them a better grip on the run time behavior of systems; type systems for low-level languages; applications of types to reasoning about computer programs; type theory as a framework for the design of sophisticated module systems; and advanced techniques in ML-style type inference.

Advanced Topics in Types and Programming Languages can be used in the classroom and as a resource for professionals. Most chapters include exercises, ranging in difficulty from quick comprehension checks to challenging extensions, many with solutions. Additional material can be found at <http://www.cis.upenn.edu/~bcpierce/attapl>.

Benjamin C. Pierce is Professor of Computer and Information Science at the University of Pennsylvania.

Contributors
David Aspinall, Karl Crary, Robert Harper, Fritz Henglein, Martin Hofmann, Henning Makholm, Greg Morrisett, George Necula, Henning Niss, Benjamin C. Pierce, Andrew Pitts, François Pottier,Didier Rémy, Christopher A  Stone, David Walker

8 x 9, 608 pp., 125 illus., ISBN 0-262-16228-8


The TPTP Library, Release v3.1.0

 Communicated by Geoff Sutcliffe
 
The TPTP  (Thousands  of Problems  for Theorem  Provers)  Problem Library  is a library of test problems for automated theorem proving (ATP) systems.  The TPTP supplies the ATP community with:
The principal motivation for the TPTP is to support the  testing and evaluation of ATP systems,  to help ensure that performance results accurately reflect the capabilities of the  ATP system being considered.  A common library of problems is necessary for meaningful system evaluations,  meaningful system comparisons, repeatability  of testing,  and the  production  of  statistically  significant results. The TPTP is such a library.

TPTP v3.1.0 is now available at:
    http://www.tptp.org
The TPTP-v3.1.0.tar.gz file contains the library, including utilities and basic documentation. Full documentation is online at:
    http://www.tptp.org/TPTP/TR/TPTPTR.shtml

The TPTP  is regularly updated with new problems,  additional information,  and enhanced utilities.  If you would like to register as a TPTP user,  and be kept informed of such developments, please email Geoff Sutcliffe.



Theoretical Computer Science
Special Issue on Automated Reasoning for Security Protocol Analysis
http://www.avispa-project.org/arspa

 Communicated by Luca Vigano'
 
BACKGROUND AND SCOPE
In connection with
           The Second Workshop on Automated Reasoning
             for Security Protocol Analysis
                   (ARSPA'05)

which took place as a satellite event of ICALP'05, we are guest-editing a Special Issue of Theoretical Computer Science devoted to original papers on formal security protocol specification, analysis and verification.

Contributions are welcomed on the following topics and related ones:
 SUBMISSION
Authors should submit their papers electronically, in portable document format (pdf) or postscript (ps), by sending an email with subject "TCS submission" to the address
                        arspa -at- avispa-project.org
with the file of the paper as an attachment, by November 13, 2005.
The following information should be included in the body of the email, in plain text:
 The cover page of the submission should also include this information.

Authors are strongly encouraged to use Elsevier Science's document class 'elsart', or alternatively the standard document class 'article'.  The Elsevier LaTeX package (including detailed instructions for LaTeX preparation) can be obtained from Elsevier's web site:
http://www.elsevier.com/locate/latex (see also http://www.elsevier.com/wps/find/journaldescription.cws_home/505625/description).

Submitted papers must be original and not submitted for publication elsewhere. The submitted papers will be subject to the standard journal refereeing process.
We kindly ask the authors to send us an abstract of their submission by November 6, 2005.

DEADLINES
Submission of abstract: November  6, 2005
Submission of paper:    November 13, 2005

EDITORS
Pierpaolo Degano (Universita` di Pisa, Italy)
Luca Vigano`     (ETH Zurich, Switzerland)

WEB-SITE
http://www.avispa-project.org/arspa


PhD Scholarships to Pursue PhD Studies in the CLIP Group at the
Technical University of Madrid, Spain
MOBIUS EU Project

 Communicated by German Puebla
 
The CLIP  group at  the Technical University  of Madrid  (UPM) invites applications for  up to three, fully funded,  4-year, PhD Scholarships for qualified graduate students.

Candidates  should  have   graduated  in  Computer  Science,  Computer Engineering, or  related fields prior to  the start of  their study at UPM. The Ph.D. work will center  around the research areas of the CLIP group  within  the  European  research  project  "MOBIUS",  under  the direction of German Puebla and Manuel Hermenegildo.

The general  aim of  "MOBIUS: Mobility, Ubiquity  and Security"  is to develop  a  framework for  establishing  trust  and  security of  Java programs,  using the Proof  Carrying Code  paradigm. The  project will start September 1, 2005 and will run for four years.

Within the MOBIUS  project, the research of the  CLIP group focuses on Abstraction Carrying  Code, an Abstract  Interpretation based approach to mobile code  safety. This involves the development  of new advanced program analysis  techniques for security  and verification, including resource consumption, both in terms of time and memory.

The   offered  scholarships   provide   excellent  opportunities   for international collaboration since MOBIUS is a European project with 16 partners  from  10 countries.  Also,  the  CLIP  group is  active  and international,  with  around 15  full-time  members  from 6  different countries.

The  grants  include  academic  fees,  medical  care, plus a  tax-free monthly  payment which  ranges from 1,100 to 1,600 euros, depending on experience.

The  following  qualifications are  not  mandatory,  but increase  the chances of success:
 Applications and information:
The  deadline for  applications is  September 26,  2005.  Applications received  after this deadline  may be  considered if  the scholarships have  not been filled  at the  time.  Applications  should be  sent to mobius-phd-grants@clip.dia.fi.upm.es and include a curriculum vitae, a listing  of  grades from  previous  studies,  a  brief description  of research interests with regards to  the CLIP group and MOBIUS, and, if at all  possible, letters of recommendation from  teachers or managers that  the student  has worked  with.   The latest  information on  the scholarships   and   the  application   process   can   be  found   at
http://www.clip.dia.fi.upm.es/Job_Openings/mobius-phd-grants.html


Research Associate Position
University of York

 Communicated by Colin Runciman
  
Applications are invited for a fixed-term research position at the Department of Computer Science, University of York, UK.  This position is for a post-doctoral researcher to investigate the use of functional programming systems in grid computing.  Specifically, the post is available in connection with a recently awarded EPSRC grant: "A Lazy Polytypic Grid: Generic Data Visualization Methods That Adapt to Resources Available".

The project is a collaboration between the University of Leeds (grant holder: David Duke) and the University of York (grant holder: Colin Runciman).  A post-doctoral researcher is being appointed at each site. The researcher at Leeds is expected to specialise in data visualisation and the researcher at York in functional programming systems, but the intention is that work will be genuinely collaborative. Both departments are active centres of research; for further information about them see http://www.cs.york.ac.uk/ and http://www.comp.leeds.ac.uk/.

The essential qualifications for the post are these:
Other desirable qualifications include:
Starting salary will be up to 27,116 pounds per annum and the position is available for up to 3 years.

For details of how to apply please email jobs@york.ac.uk quoting reference number CR05305 or see http://www.york.ac.uk/admin/persnl/jobs/. The closing date is 31 August 2005.

For informal enquiries, or more details of the technical aims of the project, you are welcome to contact me directly: e-mail Colin.Runciman at cs.york.ac.uk or telephone +44 1904 432740. Please note, however, that I am due to be away for the first 10 days and the last 10 days of August.



Ph.D. Studentship in Probabilistic Model Checking
University of Birmingham

 Communicated by Marta Kwiatkowska
  
One PhD studentship is available in the School of Computer Science at the University of Birmingham to work on probabilistic model checking under the supervision of Professor Marta Kwiatkowska.

Probabilistic model checking is an automatic verification method that can establish whether a given specification holds for a probabilistic system. For example, for the randomised Bluetooth protocol one might obtain quantitative answers to the expected time to device discovery and the probability of delivery by a deadline.  PRISM (http://www.cs.bham.ac.uk/~dxp/prism/), the leading and widely used probabilistic model checker developed at the University of Birmingham under Kwiatkowska's leadership, is an open source tool that has been used to model and analyse over 30 real-world protocols, with flaws discovered in six of those. PRISM is a symbolic model checker, and it combines numerical solution techniques, simulation-based methods (for approximate analysis) and parallelization.  This project is to contribute to the implementation of probabilistic model checking techniques within PRISM.  Possible topics include an extension of probabilistic model checking to real source code, statistical model checking, efficient algorithms and data structures, probabilistic real-time verification and online analysis methods.  More detail about this project is available at http://www.cs.bham.ac.uk/~mzk/research_probmc_stud.html

Applicants are encouraged to contact Marta Kwiatkowska directly (email: mzk@cs.bham.ac.uk) and refer to her group's work on probabilistic modelling and verification (http://www.cs.bham.ac.uk/research/systems/probabilistic/).

The studentship is available for UK and European applicants who want to work full time on their research degree and lasts for up to three years. Candidates should have, or be predicted to gain, a very good degree in computer science, mathematics or a relevant scientific discipline. Informal inquiries are welcome, preferably via e-mail. Information about admission for PhD in Computer Science at the University of Birmingham is available at http://www.cs.bham.ac.uk/study/postgraduate-research/. 

Professor Marta Kwiatkowska,
School of Computer Science,
University of Birmingham,
Edgbaston, Birmingham B15 2TT.
E-mail: mzk@cs.bham.ac.uk
URL: http://www.cs.bham.ac.uk/~mzk
Tel: +44 121 4147264
Fax: +44 121 4144281




Australian National University
Logic Summer School (12/5 - 12/16)

 Communicated by Diane Kossatz
 
As computers become more powerful, their ability to perform complicated reasoning tasks increases. In order to harness their power, we need to understand the reasoning they do, and how they may do it more efficiently.  This understanding begins with logic.

The Australian National University (ANU) has an exciting opportunity for IT professionals, senior educators and students to enhance their logic and reasoning skills for the work-force, for teaching, or for higher degree by research study, in a two-week intensive summer school at the ANU.

The Logic Summer School comprises a blend of practical and theoretical short courses on aspects of pure and applied logic taught by international and national experts. The school provides a unique learning experience for all participants, backed up with state-of-the-art computational science facilities at the ANU.

ANU Graduate Course Award
The Logic Summer School now offers graduate students the opportunity to complete part of the Summer School courses as an accredited ANU Course Award.  See our website for further details.

Program Topic:

Is It For You?
The Summer School is for you if you want to expand your knowledge and understanding of information technology for the workplace or classroom, or for your studies if you want to take the next step towards a research degree.  It is intended for:
Fees:
Professionals: $1,650 per person; discounts are available for multiple registrations from individual companies and institutions.  Students in full-time education: $120 per person; scholarships are available and are assessed on a  case-by-case basis. The web site has more details.
Registrations after Friday 28 October 2005, are subject to a 20% surcharge.

To register or for more information visit our web site at:  http://lss.rsise.anu.edu.au

If you would like to discuss this invitation in more detail, including advice on suitable candidacy, please contact Professor John Slaney by email: John Slaney@anu.edu.au

The Logic Summer School is supported by:
The Logic and Computation Program, National ICT Australia and
The Research School of Information Sciences and Engineering, ANU

General enquiries: lss@mail.rsise.anu.edu.au
Phone: +61 2 6125 8630
Fax: +61 2 6125 8651
http://lss.rsise.anu.edu.au

Professor John Slaney
Convenor
The Logic Summer School



Summer School Student Travel Grants
Second Latin-American Summer School on Computational Intelligence

 Communicated by Pablo Estevez
  
The IEEE Computational Intelligence Society is sponsoring 4 travel grants of US$500 each to help IEEE student members to attend the Second Latin-American Summer School on Computational Intelligence, EVIC2005, to be held in Santiago, Chile, on December 14-16.  Applicants must be IEEE and CIS student members. 

A poster competition will be held during the summer school. Applicants to the competition must be graduate or senior undergraduate students who present their own research/thesis work on Computational Intelligence. Posters to be presented will be selected based on an extended abstract, written in English. The student must be the first author and must present the poster orally to the jury. The First Prize will be a certificate and US$200. 

The deadline for application is October 15, 2005. For more information visit the web page 
http://www.die.uchile.cl/ieee-cis/evic2005/en/index.htm

Ph.D. Position
Monadic Computational Logics in HOL

 Communicated by Lutz Schroeder
  
A 3-year PhD-Position is available in the project

	"Monadic Computational Logics in HOL"

at the University of Bremen. The project is concerned with the implementation and further development of monadic computational logics, including monadic Hoare logic and monadic dynamic logic as well as extensions covering exception handling, as introduced by Till Mossakowski and myself. More detailed information can be found at

http://www.informatik.uni-bremen.de/~lschrode/research/projects/HOL-MDL_e.htm

Applications or further enquiries may be e-mailed to my address below.

-- Lutz


-- 
-----------------------------------------------------------------------------
Lutz Schroeder                  Phone +49-421-218-4683
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            lschrode@informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen
http://www.informatik.uni-bremen.de/~lschrode
-----------------------------------------------------------------------------





Book Announcement
Linear Logic in Computer Science
Ehrhard, Girard, Ruet, and Scott, eds.

 Communicated by Alex Simpson
  
  Linear Logic in Computer Science
  Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Philip Scott, editors
  Cambridge University Press, November 2004, ISBN 0-521-60857-0.  392 pages;
  75 exercises; 150 figures; 50 worked examples. $70.00

Linear Logic is a branch of proof theory which provides refined tools for the study of the computational aspects of proofs. These tools include a  duality-based categorical semantics, an intrinsic graphical representation  of proofs, the introduction of well-behaved non-commutative logical  connectives, and the concepts of polarity and focalization. These various  aspects are illustrated here through introductory tutorials as well as  more specialized contributions, with a particular emphasis on applications  to computer science: denotational semantics, lambda-calculus, logic  programming and concurrency theory. The volume is rounded-off by two  invited contributions on new topics rooted in recent developments of  linear logic. 

The book derives from a summer school that was the climax of  the EU Training and Mobility of Researchers project "Linear Logic in  Computer Science". It is an excellent introduction to some of the most  active research topics in the area.

Contents:  
Part I. Tutorials: 
1. Category theory for linear logicians R. Blute and Ph. Scott; 
2. Proof nets and the x-calculus S. Guerrini; 
3. An  overview of linear logic programming D. Miller; 
4. Linearity and  nonlinearity in distributed computation G. Winskel; 
5. An axiomatic  approach to structural rules for locative linear logic J. M. Andreoli; 
6. An introduction to uniformity in ludics C. Faggian, M. R. Fleury-Donnadieu and M. Quatrini;
7. Slicing polarized addictive normalization O. Laurent  and L. Toratora De Falco; 
8. A topological correctness criterion for  muliplicative noncommutative logic P.A. Mellies; 
9. Bicategories in  algebra and linguistics J. Lambek; 
10. Between logic and quantic: a tract J. Y. Girard.

For ordering information, please visit
  http://www.cambridge.org/0521608570.