From the AAR President
Call for Papers

  f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z))))))) = y

            f(f(a,b),c) = f(a,f(b,c))
  f(a,f(a,f(a,f(a,a)))) = e
                 f(e,a) = a

Interested readers may examine the input file and proof , respectively.

The 12th International Symposium on Temporal Representation and Reasoning will take place in Burlington, Vermont, June 23-25, 2005. Of interest is research on time-related problems within areas such as artificial intelligence, databases, and logic and computer-aided verification. Special emphasis is on new directions in time research. All submissions must be done electronically through the symposium Web page. The submission deadline is January 22, 2005.

SPIN 2005

The 12th international SPIN Workshop on Model Checking of Software will be held in San Francisco on August 22-24, 2005. SPIN 2005 solicits previously unpublished, currently unsubmitted, original contributions addressing theoretical, experimental and applied problems in model checking of software artifacts. Although authors are encouraged to compare their work with existing model checkers such as SPIN, the scope of the workshop is not limited to topics directly related to the SPIN system. Accepted contributions will be included in the workshop proceedings which will be published by Springer Verlag in the Lecture Notes in Computer Science series. The submission deadline: April 1 (abstracts) and April 8, 2005 (papers). For further information, see the Web site.

FroCoS 2005

The 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005) will be held at Vienna, Austria, September 19-21, 2005. The general theme of FroCoS is the development of techniques and methods for the combination, modularization and integration of systems (with emphasis on logic-based ones), and of their practical use.

Topics of interest include the following:

• Combination of logics (e.g., modal logics, logics in AI)
• Combination of decision procedures, satisfiability procedures, and constraint solving techniques
• Combinations and modularity in term rewriting
• Integration of equational and other theories into deductive systems
• Combination of deduction systems and computer algebra
• Integration of data structures into CLP formalisms and deduction processes
• Model/problem analysis and decomposition
• Hybrid methods for deduction, resolution and constraint propagation
• Hybrid systems in computational linguistics, knowledge representation, natural language semantics, and human computer interaction
• Logical modeling of multi-agent systems
• Logical aspects of combining and modularizing programs and specifications

Submission categories include full papers, for work on foundations, applications, implementation techniques, and problem sets (up to 15 pages), as well as system descriptions (up to 8 pages), for describing publicly available systems. The submission deadline is May 2, 2005, for titles and abstracts, and May 9, 2005, for papers. For further information see the Web site.

PPDP 2005

The seventh ACM-SIGPLAN international symposium on Principles and Practice of Declarative Programming (PPDP 2005) will be held July 11-13, 2005, in Lisboa, Portugal.

PPDP 2005 aims to provide a forum that brings together those in the declarative programming communities, including those working in the logic, constraint and functional programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for specifying, performing, and analyzing computations, and to stimulate cross-fertilization by including work from one community that could be of particular interest and relevance to the others.

Topics include logic, constraint, and functional programming; applications of declarative programming; methodologies for program design and development; declarative aspects of object-oriented programming; concurrent extensions to declarative languages; declarative mobile computing; integration of paradigms; proof theoretic and semantic foundations; type and module systems; program analysis and verification; program transformation; abstract machines and compilation; and programming environments.

The submission deadline is Feb. 13, 2005. Consult the Web for further details:

LICS 2005

The twentieth annual IEEE symposium on Logic in Computer Science (LICS 2005) will take place June 26-29, 2005, in Chicago, Illinois.

The LICS symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic broadly construed. Submissions are invited on topics that fit under that rubric, including automated deduction, categorical models and logics, constraint programming, formal aspects of program analysis, formal methods, lambda and combinatory calculi, logics in artificial intelligence, modal and temporal logics, model checking, reasoning about security, rewriting, type systems and type theory, and verification. Also welcome are submissions in emergent areas, such as bioinformatics and quantum computation, if they have a substantial connection with logic.

Authors are required to submit a paper title and a short abstract of about 100 words before submitting the extended abstract of the paper. All submissions must be electronic. Titles and short abstracts are due Jan. 5, 2005; extended abstracts are due Jan. 10, 2005. Authors will be notified of acceptance by March 18, 2005. Detailed information about electronic paper submission will be posted at the LICS Web site.

Short Presentations: LICS 2005 will have a session of short (5-10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages long), should be entered at the LICS 2005 submission site March 19-25, 2005. Authors will be notified of acceptance or rejection by April 1, 2005.

Kleene Award for Best Student Paper: An award in honor of the late S. C. Kleene will be given for the best student paper, as judged by the program committee. Details concerning eligibility criteria and procedure for consideration for this award will be posted at the LICS website. The program committee may decline to make the award or may split it among several papers.

KI 2005

The 28th German conference on AI will take place in Koblenz, Germany, on September 11-14, 2005. This conference traditionally brings together academic and industrial researchers from all areas of AI. Researchers are invited to submit proposals for technical papers and workshops/tutorials. Workshop/tutorial proposals must be submitted by February 18, 2005. The deadline for submission of technical papers is April 15, 2005.

For detailed information see the Web site on workshops and on tutorials.

IWIL-2005

The fifth international workshop on the Implementation of Logics will be held in March 2005 in conjunction with the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning in Mondevideo, Uruguay.

Contributions are invited that describe implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include the following:

• Data structures and algorithms for the efficient representation of logical concepts
• Practical constraint handling
• Implementation of provers for different logics
• Efficient model generation
• Issues of reliability, witness generation, and witness verification
• Propositional logic (modulo theories) and decision procedures
• Implementation of higher-order logics and lambda-calculus
• Proof search organization and efficient heuristics for classical and inductive provers
• Experiences with new or unusual calculi
• Evaluation and benchmarking of provers and other logic-based systems
• System descriptions

For information, see the Web page.

ESSLLI'05 Student Session

The 17th European Summer School in Logic, Language and Information (ESSLLI'05) will be held August 8-19, 2005, in Edinburgh. Included will be a Student Session (StuS), and students (undergraduates as well as graduates) are invited to submit papers for oral and poster presentation from the areas of logic, language, and computation. Student authors are invited to submit a full paper, not to exceed 7 pages (exclusive of references). Papers are to be submitted with clear indications of the selected modality of presentation: oral or poster. The submissions will be reviewed by the student session program committee and selected reviewers. The preferred formats of submissions are PostScript, PDF, or plain text, although other formats will also be accepted. The paper and a separate identification page must be sent electronically to gervain@sissa.it by Feb. 15, 2005.

For more information and the technical details of the submission, see the Web page.

Authors are invited to submit electronically (in postscript or PDF) full papers for work on foundations, applications or implementation techniques (15 pages), as well as system descriptions (5 pages) for describing publicly available systems. For further information and submission instructions, see the CADE-20 Web page.

Deadlines:

E-submission of title and abstract: February 25, 2005 E-submission papers: March 4, 2005 Notification of acceptance: April 22, 2005 Final version due: May 20, 2005

Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles Dowek (Ecole Polytechnique) and by Frank Wolter (U. Liverpool).

An election was held from September 23 through October 13 to fill four positions on the board of trustees of CADE Inc. Maria Paola Bonacina, David Basin, Gilles Dowek, Juergen Giesl, Rajeev Goré, Hans de Nivelle, Geoff Sutcliffe, and Cesare Tinelli were nominated for these positions. (See AAR Newsletter No. 64, September 2004.)

Ballots were sent by electronic mail to all members of AAR on September 23rd, for a total of 630 ballots (up from 587 in 2003, 566 in 2002, 548 in 2001, 445 in 2000 and 396 in 1999). Of these, 125 were returned with a vote, representing a participation level of 19.8% (the same percentage exactly as in 2003, but down from 26.3% in 2002, 22.5% in 2001, 24.5% in 2000, and 30% in 1999). The majority is 50% of the votes plus 1, hence 63.

The following table reports the initial distribution of preferences among the candidates:

No candidate reaches a majority right away. G. Dowek and H. de Nivelle have the same number of first preference votes, but Dowek is higher in the ranking because of receiving more second preference votes. The redistribution of the votes of H. de Nivelle yields the following new distribution:

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of C. Tinelli, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of R. Goré, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of D. Basin, one gets the following table:

M. P. Bonacina is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

None of the candidates has a majority to be elected, so the votes of H. de Nivelle need to be redistributed again:

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of C. Tinelli, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of R. Goré, one gets the following table:

Thus, D. Basin is elected to the board of trustees. (Since 57 votes does not suffice for the majority, the STV algorithm executes another round distributing the votes of G. Sutcliffe, but this is not reported because the outcome is obvious.) The redistribution of the votes of the winner produces the following table:

Again, no candidate reaches a majority, and by redistributing the votes of H. de Nivelle, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of C. Tinelli, one gets the following table:

Thus, G. Sutcliffe is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

Again, no candidate reaches a majority, and by redistributing the votes of H. de Nivelle, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

Thus, R. Goré is elected to the board of trustees.

After this election, the following people are serving on the board of trustees of CADE Inc.:

Franz Baader (President, CADE-19 Program Chair, elected 10/2003)
David Basin (IJCAR 2004 Program Co-chair, elected 10/2004)
Peter Baumgartner (elected 10/2003)
Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004)
Amy Felty (Secretary, appointed 5/2004)
Rajeev Goré (elected 10/2004)
Michael Kohlhase (elected 10/2000, reelected 10/2003)
Neil Murray (Treasurer)
Robert Nieuwenhuis (CADE-20 Program Chair)
Geoff Sutcliffe (elected 10/2004)
Andrei Voronkov (Vice President, CADE-18 Program Chair, elected 10/2002)
Toby Walsh (elected 10/2002)

On behalf of the AAR and CADE Inc., I thank Frank Pfenning for his service as trustee and CADE Inc. president during the past 6 years, Gilles Dowek and John Harrison for their service as trustees during the past three years, all candidates for running in the election, all the members who voted; and offer congratulations to David Basin, Maria Paola Bonacina, Rajeev Goré, and Geoff Sutcliffe on being elected, and to Franz Baader on being elected president of CADE Inc.

TPTP v3.0.0 is now available on the Web. The TPTP-v3.0.0.tar.gz file contains the library, including utilities and basic documentation. Full documentation is online.

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.

What's New in TPTP v3.0.0

Changes from v2.7.0 to v3.0.0 for FOF problems

• new abstract problems
• new problems
• new generators
• 53 bugfixes done, in the domains AGT SYN
• ratings changed

Changes from v2.7.0 to v3.0.0 for CNF problems

• new abstract problems
• new problems
• new generators
• 1 bugfix done, in the domains SWC
• ratings changed

The library has been translated to the new TPTP syntax (aka the TSTP syntax).

• The BNF for the new TPTP syntax has been added to the Documents directory.
• Equality is now written in infix, using = and !=
• CNF ``conjecture"s have been changed to ``negated_conjecture"
• $true and $false are now reserved constants and have been used as expected.

Equality is now assumed to be built in, and all equality axioms have been removed from all problems.

Problem status values have been updated to the SZS problem status ontology:

• The ontology has been added to the Documents directory.
• FOF problems with conjectures are one of Theorem, CounterSatisfiable, Unknown, Open.
• FOF problems without conjectures are one of Unsatisfiable, Satisfiable, Unknown, Open.
• CNF problems are one of Unsatisfiable, Satisfiable, Unknown, Open.

tptp1T has been updated to understand the new status values.

No numbers appear in any problems--numbers are now reserved for future built-in treatment.

The tptp2X utility has been extended and improved:

• The new TPTP syntax (aka the TSTP syntax) is the default output format
• The old TPTP syntax is available as the oldtptp format
• rm_equality with no selection removes all
• add_equality has been parameterized like rm_equality
• New set_equality transform
• New prefix format
• FOF files with multiple conjecture formulae are expanded to multiple files each with a single conjecture and all the other formulae.
• Searches for include files:
  • No search for absolute names
  • Relative names are searched for under the $TPTP environment variable and if not found then under the current working directory
• Explicit support for YAP Prolog
• Installation is done by editing the *.uninstalled files and creating the final files. This solves some CVS problems.