Next: About this document ...
From the AAR President, Larry Wos...
Education
is key, we are told, to keeping our society strong
and flourishing.
I am delighted, therefore, to see that several people have
recently received doctoral degrees in automated reasoning.
I hope they will in turn become guiding lights for the next
generation of researchers!
On a different note, let me point our readers to the call for papers for a special issue of the Journal of Automated Reasoning. Most attractive, to me, is the emphasis being placed on ``really working'' systems and applications. While theory is certainly important, I have--throughout my career--stressed the value of translating ideas into working software and then testing those ideas on real applications.
An election of CADE trustees will be held soon, and all AAR members will receive a ballot. The following people are currently serving as trustees of CADE Inc.:
The terms of Robert Nieuwenhuis, Andrei Voronkov, and Toby Walsh are expiring. The position of Robert Nieuwenhuis will be taken by Uli Furbach as IJCAR 2006 co-program chair. Thus, there are two positions to fill.
The following candidates were nominated, and their statements are below:
galmiche/)
reiner/)
stump/)
tinelli/)
tw/)
In addition, the CADE trustees and the business meeting at CADE-20 have decided to put the following amendment of the CADE bylaws regarding the election of the CADE president to the vote of the entire AAR membership:
In Article V (Officers), Section 2 (Election and Term of Office) replace
``The President and Vice President shall be elected by and from the Board of Trustees."
by
``The President and Vice President shall be elected by and from the Board of Trustees using the Single Transferrable Vote system."
Statement by Didier Galmiche
I have been working in automated deduction a long time in connection with type theories, substructural logics (intuitionistic logic, and linear logic) and with interests for both proof theory and semantics. My recent works focus on methods and tools for proof and countermodel construction in various resource and separation logics and their applications to distributed systems and semi-structured data analysis.
I have some experience (PC member of logic and AR events like CSL, CADE, IJCAR, Tableaux, Wollic, co-organizer of CADE Workshops on proof-search in type-theoretic languages, member of Tableaux Steering Committee) and an approach of automated reasoning in a broad perspective (theorem proving, semantic methods, proof theory, implementations).
Therefore, as CADE trustee I could help to keep its status and audience with high standards and an attracting scope. I think that we have to continue to attract new workshop proposals on related topics, to participate to FLOC and IJCAR, and also to strengthen the relationships with related communities like logic, proof-theory, verification, or security.
Statement by Reiner Hähnle
The first international scientific conference that I attended was CADE-8 in 1986. Ever since, the CADE community has been one of the major venues where my professional career took place. My most recent contribution to CADE was a tutorial (http://www.key-project.org/cade20-tutorial/) on verification of object-oriented software, presented at CADE-20 in Tallin this summer. In between, I participated in most CADEs, contributed numerous papers, served on several CADE PCs, and was conference chair of CADE-18 in Copenhagen.
I have worked on automated reasoning in non-classical and first-order logics in the past; my current research interests lie mainly within software verification (see the KeY project Web pages: http://www.key-project.org/). In order to keep automated deduction a dynamic and lively field of research, I believe it is very important that CADE tries to increase the participation of consumers of reasoning technology such as formal verification or Semantic Web reasoning. This means not merely a willingness to accept papers on applications, but ideally a more proactive approach, such as the organization of special tracks or co-location with suitable events. As CADE trustee I would use my influence to make applications of automated reasoning an integral part of the conference.
In the past five years I have been deeply involved in organizing FLoC
(http://research.microsoft.
com/floc06/)
(``hat king" of FloC 2002 - see http://floc02.diku.dk/misc/hatsself.html, trustee of FLoC Inc.) and starting up IJCAR
(founding member of steering committee). I also served on the steering
committees of Tableaux and FTP. From this experience I gained
considerable insight into the structure and current status of many
subcommunities of computational logic. I believe that the field needs
both: highly visible, comprehensive meetings (such as IJCAR, FLoC) as
well as more intimate and specialized ones, which subcommunities can
identify with. As a trustee I would work towards keeping both IJCAR
and CADE as alternating events.
Statement by Aaron Stump
As a younger researcher (I got my Ph.D. in computer science from Stanford in 2002), I am very excited about the possibility of serving the automated reasoning community as a CADE trustee. I have broad interests in automated reasoning, but I am probably best known for my work in decision procedures (I was the main implementor of the CVC cooperating validity checker). I also have ongoing projects in logical frameworks, type theory, and term rewriting theory. I am particularly interested in applications of automated reasoning to verification and programming languages theory.
To me, one of the best things about CADE is the diversity of its submissions. We regularly get talks covering the range from highly theoretical to engineering focused, as well as an exciting range of applications. I find such diversity intellectually very stimulating, and as a CADE trustee, I would work to support it, for example by personally encouraging colleagues in verification and programming languages to submit to CADE. I am also supportive of the current philosophy of having CADE meet either alone, with other meetings as IJCAR, or as part of FLoC, in different years.
Statement by Cesare Tinelli
My general research interests are automated reasoning, with a focus on reasoning modulo built-in theories--that is, theories implemented by means of specialized reasoners. I have been particularly active in the combination of decision procedures and their integration into general purpose calculi. My most recent research is on the DPLL(T) scheme, a general formal framework and architecture for ground satisfiability modulo theories (SMT), and on the Model Evolution calculus, a first-order version of the DPLL procedure, of both of which I am a co-author. I'm the co-founder of the PDPAR workshop (Pragmatics of Decision Procedures in Automated Reasoning), now at its 4th edition. I have served as a PC member or co-organizer for a number of AR related events (see my Web page for a complete list), and I am currently a steering committee member of FTP, FroCoS and IJCAR.
I'm also a coordinator of the SMT-LIB initiative, whose main goal is to establish a common standard and a library of benchmarks for satisfiability modulo theories. In that capacity, I maintain active contacts with a large number of computer-aided verification practitioners and researchers from industry and academia, who have many potential applications and a strong interest for provers for satisfiability/deduction modulo theories.
As a trustee I would push for CADE to continue its efforts in attracting papers over the whole spectrum of AR research, with a renewed emphasis of attracting more work on applications. One way to achieve this at the trustees level could be to establish a set of (non-strictly binding and renewable) guidelines for future CADE PC chairs on the composition of the PC, the selection of invited speakers, and the type of solicited submissions. On a personal level, I would use my ties to the growing community of SMT researchers--which sadly seem to gravitate more and more around forums such as CAV, CP and SAT--to help maintain a continued flow of CADE submissions from them. I would also work toward making the CADE community more aware of the sort of deduction problems faced in verification today, and the need in that field of a large spectrum of deduction tools, well beyond traditional stand-alone refutational theorem provers.
As a current member of the FTP and FroCoS SC's I strongly support the idea of having a larger comprehensive event like IJCAR on a regular basis, to avoid an excessive fragmentation of the AR community into several smaller events. Consistently with that, I also support the continuted participation of CADE to FLoC as IJCAR, not as a stand-alone conference. As a CADE trustee I would also push for a better interaction and coordination between CADE and other AR events such as TABLEAUX, FTP, FroCoS. In this respect, I am in favor of maintaining a permanent IJCAR SC, made of representatives from the various events, with the main goals of coordinating the organization of IJCAR and the interaction with FLoC.
Statement by Toby Walsh
The automated reasoning (AR) community faces a number of fundamental problems. First, there is increasing fragmentation. Events like IJCAR (which I chaired in Cork in 2004) are one solution to this problem. However, we cannot stop there but must embrace other closely related areas (for example, we need to join with the satisfiability research community, in which I am very active) that have common research problems. I was very happy therefore to help get SAT 06 into the FLOC conference next year. Second, there must be more fresh blood brought into the field. I introduced a doctoral programme for IJCAR 04 to engage Ph.D. students at an early stage in their studies. However, there are other initiatives to consider, like an AR summer school. Finally, we need to maintain our visibility in related areas like KR and AI where we have much to bring to the table.
Brief bio: Toby Walsh is leader of the Knolwedge Representation and Reasoning program at National ICT Australia and a professor at UNSW. He was previously SFI Research Professor at University College Cork and an EPSRC advanced research fellow at the University of York. He completed his Ph.D. in automated reasoning at the University of Edinburgh under the supervision of Profs. Alan Bundy and Fausto Giunchiglia.
AIESP 2006
The First International ICSC Symposium on Artificial Intelligence in Energy Systems and Power will be held on the island of Madeira, Portugal, February 7-10, 2006. For further information, see the website: http://www.icsc-naiso.org/conferences/aiesp2006/aiesp-cfp.html.
The organizing committee has extended the deadline for submission of papers to November 15, 2005. The conference will also accept a limited number of non-AI related poster papers.
Artificial intelligence is an advanced computer science that seeks to emulate some of the capabilities of the human brain, for example, to automate control of engineering systems and extend the skill of human operators. AIESP2006 is the first of a series of conferences on applications of AI in energy systems and power. It will provide a forum for discussing the latest developments in these subjects.
In energy systems the conference will cover topics such as alternative energy including renewable energy sources (biomass, hydro, solar, wind, geothermal, tidal and photovoltaic conversion systems), new transportation fuels (such as ethanol), and new applications of conventional energy sources (such as the use of propane and natural gas as automotive fuels, and batteries in electric vehicles), fuel cells, and gas hydrates
Examples of energy systems and power topics include dispersed generation and distribution planning, dynamic stability, load flow analysis, and power system equipment diagnosis.
Conference proceedings (including all accepted papers) will be published by ICSC Academic Press and be available for the delegates at the symposium on CD-ROM. Authors of a selected number of innovative papers will be invited to submit extended manuscripts for publication in prestigious international journals such as the International Journal of Energy Technology and Policy. For further information, please contact Ahmed Zobaa at editorial@eng.cu.edu.eg>editorial@eng.cu.edu.eg.
Natural Language and Knowledge Representation
FLAIRS 2006 will take place at Melbourne Beach, Florida May 11-13, 2006. A special track at FLAIRS 2006 will be devoted to natural language and representation (NL-KR). Submissions are invited for this track in the following and related areas:
Only electronic
submissions will be considered. Details about submission can be found on
http://users.ox.ac.uk/lady0641/Flairs06_NL_KR/submission_details.html
Selected papers will be considered for publication
in a special journal issue of Journal of Logic and Computation in the
second half of 2006.
Proceedings on CD will be provided to all.
Those interested in running a demo please contact Jana Sukkarieh J.Sukkarieh.94@cantab.net or Simon Dobnik Simon.Dobnik@clg.ox.ac.uk.
JAR Special Issue:
Empirically Successful Automated Reasoning
With improving technology, theorem proving and related methods are successfully being applied to larger problems and used in more domains. To further disseminate developments and results in this area, a special issue of the Journal of Automated Reasoning dedicated to empirically successful automated reasoning will be published.
We invite submission of articles describing work on the implementation
and deployment of working automated reasoning systems and applications.
Both participants of the successful ESCAR-workshop at CADE-20 (see
http://www.cs.miami.edu/geoff/Conferences/ESCAR/) and other authors
are invited to submit contributions. Submissions should be mature
journal articles. They may address any aspect of ``really working"
systems and applications and should not focus on theoretical ideas
that have not yet been translated into working software.
Similar to the ESCAR-workshop, this special issue will have two tracks: one for systems and one for applications. Suggested topics include the following:
Systems
Applications
Submissions should be formatted according to JAR's author guidelines (see the link on the home page below), and preferably be written in LaTeX. A LaTeX style file can be obtained from the Web: http://www.springeronline.com/authors/jrnlstylefiles. Submissions are due December 5, 2005, at esar-jar@eprover.org. The website for this special issue, containing more useful information, is
http://www.eprover.org/EVENTS/ESAR-JAR
FM'06
FM'06 will be held August 21-27, 2006, in Ontario, Canada. This is the fourteenth in a series of symposia on formal methods for software development. The symposia have been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development. Submissions are welcomed in the form of original papers on research and industrial experience, proposals for workshops and tutorials, entries for the exhibition of software tools and projects, and reports on ongoing doctoral work. We are particularly interested in the experience of applying formal methods in practice. The broad topics of interest of this conference are as follows:
Tools for formal methods: tool support and software engineering, environments for formal methods.
Formal methods in practice: experience with introducing formal methods in industry, case studies.
Role of formal methods: formal methods in hardware and system design, method integration, development process.
Full papers should be submitted via the website at http://fm06.mcmaster.ca/. Accepted papers (max. 16 pages) will be published in the symposium proceedings, to appear in Springer's Lecture Notes in Computer Science series. A prize for the best technical paper will be awarded at the symposium.
Industrial Usage Reports. One day will be dedicated to sharing the experience--both positive and negative--with using formal methods in industrial environments. This year's Industry Day investigates the use of formal methods in security and trust. Invited papers on organizational and technical issues will be presented. Inquiries should be directed to the Industry Day Chairs; see the Web site for details.
Workshops. We welcome proposals for one-day or one-and-a-half-day workshops related to FM'06. In particular, but not exclusively, we encourage proposals for workshops on various application domains.
Tutorials. We are soliciting proposals for full-day or half-day tutorials. The tutorial contents can be selected from a wide range of topics that reflect the conference themes and provide clear utility to practitioners. Each proposal will be evaluated on importance, relevance, timeliness, audience appeal and past experience and qualification of the instructors.
Poster and Tool Exhibition. An exhibition of both research projects and commercial tools will accompany the technical symposium, with the opportunity of holding scheduled presentations of commercial tools.
Doctoral Symposium. For the first time, FM'06 will feature a doctoral symposium. Students are invited to submit work in progress and to defend it in front of ``friendly examiners.'' Participation for students who are accepted will be subsidized.
Submission Info
M4M-4
The workshop ``Methods for Modalities" (M4M) will be held in Berlin December 1-2, 2005. M4M aims to bring together researchers interested in developing algorithms, verification methods and tools based on modal logics. Here the term ``modal logics" is conceived broadly, including description logic, guarded fragments, conditional logic, and temporal and hybrid logic.
To stimulate interaction and transfer of expertise, M4M will feature a number of invited talks by leading scientists, research presentations aimed at highlighting new developments, and submissions of system demonstrations. We strongly encourage young researchers and students to submit papers and posters, especially for experimental and prototypical software tools related to modal logics.
Regular papers should not exceed 12 pages; short papers, 6 pages; and posters and tools, 2 pages. Proceedings will appear online and as a Humboldt University report. Depending on the submissions, papers may be selected to appear in a special issue of an appropriate journal. Submission is by email; either Postscript or PDF files can be sent to m4m-4@first.fraunhofer.de.
For more information and registration information, see the M4M homepage at http://m4m.loria.fr/
We are pleased to present the abstracts of three recent theses in automated reasoning.
Author: Claudio Castellini
Title: Automated Reasoning in Quantified Modal and Temporal Logics
Supervisor: Alan Smaill
Date of Defense: June 6, 2005
Institution: University of Edinburgh (UK), School of Informatics
Abstract: Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account persistence through time. Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods.
The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of Feature Interactions in telecommunication systems.
These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency.
Author: Chad E. Brown
Title: Set Comprehension in Church's Type Theory
Supervisor: Peter B. Andrews
Date of Defense: June 29, 2005
Institution: Carnegie Mellon University
Abstract:
hurch's simple type theory allows quantification over sets and functions. This expressive power allows a natural formalization of many mathematical concepts. However, the process of automated theorem proving in Church's type theory is more difficult than in the first-order case. One problem in particular is the instantiation of set variables. Such instantiations can involve arbitrary logical constants. Searching for set instantiations has not yet been well understood. Here we study the role of set comprehension in higher-order automated theorem proving. In particular, we introduce formulations of fragments of Church's type theory which are restricted with respect to set comprehension. We then define corresponding semantics and show soundness and completeness. Using completeness, we show that some restrictions to set comprehension are complete with respect to the usual notion of Henkin models. That is, we can prove any theorem with restricted set comprehension that could be proven with unrestricted set comprehension. We also show some restrictions are incomplete. This methodology is used to study set comprehension both in the presence and absence of extensionality.
We also describe methods for automated theorem proving in extensional type theory with restricted set instantiations. The approach to automated proof search presented here extends mating search by including connections up to extensional and equational reasoning. Search procedures based on these ideas have been implemented as part of the TPS theorem prover. The procedures have also been augmented by including the ability to solve for certain sets using set constraints. We describe the implementation and include experimental results.
The thesis can be obtained from http://gtps.math.cmu.edu/cebrown/papers/thesis.ps.gz.
Author: Daniel Winterstein
Title: Using Diagrammatic Reasoning for Theorem Proving in a Continuous Domain
Supervisors: Alan Bundy, Corin Gurr, and Mateja Jamnik
Date of Graduation: January 2005
Institution: University of Edinburgh
Abstract: This project looks at using diagrammatic reasoning to prove mathematical theorems. The work is motivated by a need for theorem provers whose reasoning is readily intelligible to human beings. It should also have practical applications in mathematics teaching.
We focus on the continuous domain of analysis - a geometric subject, but one which is taught using a dry algebraic formalism which many students find hard. The geometric nature of the domain makes it suitable for a diagram-based approach. However it is a difficult domain, and there are several problems, including handling alternating quantifiers, sequences and generalisation. We developed representations and reasoning methods to solve these. Our diagram logic isn't complete, but does cover a reasonable range of theorems. It utilizes computers to extend diagrammatic reasoning in new directions, including using animation.
This work is tested for soundness, and evaluated empirically for ease of use. We demonstrate that computerised diagrammatic theorem proving is not only possible in the domain of real analysis, but that students perform better using it than with an equivalent algebraic computer system.
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 workforce, for teaching, or for higher degree by research study, in a two-week intensive summer school.
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.
Program Topics:
Modal and temporal logic
Automated reasoning
Formal methods
Knowledge representation and reasoning
Nonclassical logic
Computability and incompleteness
The Summer School 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.
Registrations after October 28, 2005, are subject to a 20% surcharge. To register or for more information visit our website 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
Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland have published a new book entitled Rippling: Meta-Level Guidance for Mathematical Reasoning. Rippling was developed for inductive proofs, and it has proved applicable in problems involving reasoning about repetition (e.g., the behavior of electronic circuits over time). This book introduces researchers and graduate students to rippling and to the wider subject of automated inductive theorem proof.
Cambridge University Press, 2005, ISBN 0-521-83449-X, 202 pages