AAR is now entering a new exciting phase of its existence.
The plan is to expand the activities of AAR, to provide a focus point for the broad AR community, and
to provide services and support for research.
For one important item, we now have a new editor of the newsletter,
Martin Giese.
We in AAR are indeed fortunate to have him and his expertise.
I, for one, welcome him on board.
I eagerly await to witness his influence on the content of the newsletter.
Please transmit to Martin Giese items that might be of use to our membership.
His e-mail address is martingi (at) ifi.uio.no
I offer a challenge to students, professors, and others in general. For the first person, or group, that meets this challenge I shall give a prize of $100. The field in focus is called Lukasiewicz's infinite-valued sentential calculus. The following clauses provide an axiom system.
% Just the implicational Axioms: MV1 - MV3 P(i(x,i(y,x))). P(i(i(x,y),i(i(y,z),i(x,z)))). P(i(i(i(x,y),y),i(i(y,x),x))). % Following is MV4. P(i(i(n(x),n(y)),i(y,x))).
One additional axiom, the following, is sometimes given.
% Following is MV5. P(i(i(i(x,y),i(y,x)),i(y,x))).
As it turns out, MV5 is dependent on the other four formulas. I
have a number of 30-step proofs, each relying on condensed detachment.
The challenge is to find a proof relying strictly on condensed
detachment where the proof has length 29 or less (deduced steps). You
can have a reasoning program apply condensed detachment by using the
inference rule hyperresolution and the following clause,
where | denotes logical or and - denotes
logical not.
-P(i(x,y)) | -P(x) | P(y).
At this point in time, I have not included a 30-step proof in order to avoid biasing you. Good luck. Yes, I am indeed very interested in a proof sorter than length 30.
For many years, AAR has been more than fortunate to have Gail Pieper be editor of the newsletter. She has set a standard that we can ask future editors to follow. For those years of service, we thank you. Gail, from all of the members of AAR, we are indebted to you and know that, whatever activity you decide to pursue, you will succeed.
Larry Wos
on behalf of the board of the AAR
The AAR web pages have been ported to http://www.AARInc.org/. The pages include the names and contact information of the board members, the (soon to be updated) bylaws, the membership list, all newsletters, and information about the Herbrand Award. Visit http://www.AARInc.org/ now, if only to see the new AAR logo!
The board of the AAR has five members: president, vice president, secretary, and two CADE nominees. Until recently, CADE has been represented by Alan Bundy and Deepak Kapur. Both have stepped down, after many years of service. As successors, the CADE trustees elected Maria Paola Bonacina and Geoff Sutcliffe. The AAR board now has the following composition:
On the behalf of AAR and CADE, I thank Alan Bundy and Deepak Kapur for everything they did in service of both associations.
Wolfgang Ahrendt
Secretary of AAR and CADE
It is my distinct honor to announce on behalf of the Board of Trustees of CADE Inc. that Edmund M. Clarke is to receive the 2008 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades.
The award will be presented to Professor Clarke at the 4th International Joint Conference on Automated Reasoning (IJCAR 2008) in Sydney, Australia.
Franz Baader
President of CADE Inc.
The Woody Bledsoe Student Travel Award is intended to enable selected students to attend the the International Joint Conference on Automated Reasoning (IJCAR) by covering much of their expenses. The winners of the travel award will be (partially) reimbursed for their conference registration, transportation, and accomodation expenses (past awards have varied, but have typically been AU$250 to AU$1000). Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.
The awards are sponsored by CADE Inc.
See The IJCAR 2008 web pages for more information, including application details.
The University of Edinburgh School of Informatics is holding a symposium to celebrate Alan Bundy's 60th birthday on July 13th and 14th 2008.
The broad range of Alan's research interests will be reflected in the invited talks by top international researchers who have worked closely with Alan over the years: Jörg Siekmann, Fausto Giunchiglia, Frank van Harmelen, Luigia Aiello, Chris Mellish, Dave Robertson, Stan Wainer and Alan Smaill. There will be public lectures on the Future of AI and many opportunities for informal conversation as well as round table discussions. This will also be the first event showcasing the new University of Edinburgh Informatics Forum.
Attendance is free and there will be a celebratory dinner on July 13th and a ceilidh on July 14th. We have funding for PhD students from AISB and from EPSRC to cover accommodation and travel. Further information and registration is available online here.
Please register by the 24th of June!
Any questions concerning the event can be sent to Sofi Freijeiro-Mato (sfmato (at) inf.ed.ac.uk.
We would like to remind you that IJCAR 2008 will host a number of exciting workshops:
Note that the ESHOL workshop has been merged into PAAR 2008, and that the workshop on Combining Systems for Efficient and Scalable Reasoning (CoSyScaRe 08) has been cancelled.
See also the IJCAR Workshops web page.
The 8th International Workshop On User Interfaces for Theorem Provers will be held as a TPHOLS'08 Satellite Workshop in Montréal, Québec, Canada, on Friday, 22nd August 2008. The UITP workshop series brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulas. Topics covered include, but are not limited to:
Please visit the UITP web pages for more information.
The Workshop on Automated Deduction in Geometry (ADG) will be held at East China Normal University, Shanghai, China, on September 22–24, 2008.
The workshop is a leading international forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools on the intersection between geometry and automated deduction. The main objective of this workshop is to encourage/promote/guide research efforts in the area in an informal setting.
It is expected that the accepted full papers will be published as a special issue of some journal or in the Springer Lecture Notes in Artificial Intelligence (LNAI) series
Specific topics for ADG 2008 include (but are not limited to):
Visit the workshop web pages for detailed information.
The CICM 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics (ESARM) will be held as part of the Conferences on Intelligent Computer Mathematics, in Birmingham, UK, 26th July–2nd August, 2008.
This workshop will bring together practioners and researchers who are concerned with the development and application of automated reasoning for mathematics. The workshop will discuss only "really running" systems and applications, and not theoretical ideas that have not yet been translated into working software.
See the workshop web pagefor details.
The The 4th International Joint Conference on Automated Reasoning, IJCAR 2008, will be held in Sydney, Australia, 10th–15th August 2008. The conference is a merger of four leading conferences and workshops:
IJCAR is the premier international joint conference on all aspects of automated reasoning, including foundations, implementations, and applications. The IJCAR technical program will consist of presentations of high-quality original research papers and invited talks. There will be two days of workshops and tutorials, 10th and 11th August, and the conference 12th to 15th August.
See The IJCAR Web pages for detailed information, including 101 reasons to attend the conference!
The 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) will be held at Doha, Qatar, on November 23–27, 2008.
New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to:
|
|
More details can be found on the LPAR web pages.
The 21st International Conference on Theorem Proving in Higher Order Logics will be take place in Montéal, Québec, Canada, on 18th–21st August, 2008.
The conference covers all aspects of theorem proving in higher order logics, and related topics in theorem proving and verification. This includes, but is not limited to, the following topics:
See the TPHOLs 2008 web pages for more details.
The conference on integrated formal methods, iFM 2009, will take place in Düsseldorf, Germany, on 16th–19th February 2009.
The iFM conference series seeks to further research into the combination of different formal methods, both for modelling and analysis, covering all aspects from language design over verification techniques to tools and their integration into software engineering practice.
Areas of interest include but are not limited to:
More information can be found on the iFM 2009 web pages
There will be a special issue of the Journal of Automated Reasoning on Operating Systems Verification. The submission deadline is September 15, 2008.
Industrial-strength software analysis and verification has advanced in recent years through the introduction of model checking, automated and interactive theorem proving, static analysis techniques, as well as correctness by design. However, many techniques are working under restrictive assumptions which are invalidated by complex (embedded) system software such as operating system kernels, low-level device drivers or microcontroller code.
This special issue will be devoted to the formal verification of operating systems and similar low-level systems code. The emphasis is on techniques and methods that provide real solutions to real software problems. A real solution is one that is applicable to the problem in industry and not one that only applies to an abstract, academic toy version of it. Submissions are encouraged, but not limited to, the following topics and their application to operating systems or low-level systems code:
For more information, including submission instructions, see the Call for Papers.