Finding first proofs, better proofs, or more elegant proofs and settling conjectures often are successful only through an iterative procedure. One takes the results of one experiment and uses them in some way in the next. Appealing is the prospect of replacing much of the iteration with a single run. With such, one could submit a job in the afternoon, go to a play, eat dinner, and find, upon returning, the sought-after result.
For example, in 2002, I found with iteration and the cramming strategy, a 50-step proof that derives, from the following William McCune single axiom for lattice theory, a 50-step proof. The target was a 4-base. You might enjoy the challenge of trying to find a proof, deriving the 4-base, or deriving a standard 6-base.
(((y v x)^x) v (((z^ (x v x)) v (u^x))^v))^ (w v ((v6 v x)^ (x v v7)))=x.
(The 50-step proof can be found in the book Automated Reasoning and the discovery of Missing and elegant Proofs.) In addition, you might see how short a proof you can find. I suspect you will also use an iterative approach. Quite recently, I found a 42-step proof. That proof will appear on my website in a notebook soon.
Here's an alternative challenge. Have your program seek the proof of various lemmas that might be useful in a proof of a particular theorem of your choice.
Some of the lemmas might not be true, so do not spend time considering their deducibility. Instead, simply try to prove a number of possible lemmas. Have your program pause every so often, and check to see which lemmas have been proved. If any have, then take the proof steps, or just the proved lemmas, and in either case adjoin them to the run in progress and resume. This idea is somewhat in the spirit of learning. You might, if using resonators or hints, have the proof steps adjoined to either class.
Let me know what happens.
Wolfgang Ahrendt
(Secretary of AAR and CADE)
E-mail: ahrendt@chalmers.se
The terms of Franz Baader, Peter Baumgartner, and Aaron Stump expire. The position of Renate Schmidt is taken by Jürgen Giesl as IJCAR-2010 program co-chair. Thus, there are three positions to fill.
The following candidates (listed in alphabetical order) were nominated and their statements are below:
Rajeev Goré
nominated by Peter Baumgartner and Neil Murray
Konstantin Korovin
nominated by Andrei Voronkov and Stefan Schulz
Christopher Lynch
nominated by Franz Baader and Jürgen Giesl
Brigitte Pientka
nominated by Amy Felty and Maria Paola Bonacina
Renate Schmidt
nominated by Reiner Hähnle and Martin Giese
Aaron Stump
nominated by Peter Dybier and Koen Claessen
Christoph Weidenbach
nominated by Geoff Sutcliffe and Renate Schmidt
By joining the Steering Committee of CADE, I wish to continue the recent trend which makes CADE attractive to researchers in non-first-order or non-resolution methods like tableaux, inverse calculi, rewriting, and automata-theoretic methods. I believe that it is extremely important to let other conferences like TABLEAUX, FTP, TPHOLs/ITP and RTA continue their individual traditions, but also that we should continue to encourage these conferences to co-locate as IJCAR. Of course, first-order logic and resolution calculi will still form a central part of CADE, but I think CADE will benefit greatly from its broader view. I have published papers in CADE, TABLEAUX, TPHOLs and RTA over the years. I was on the CADE PC in 2007 and 2009. I have been on the PC for IJCAR01, IJCAR04 and IJCAR08. I was on the CADE Steering Committee from 2004-2007 and am the current president of the TABLEAUX Steering Committee.
My research focuses on both theoretical and implementation aspects of first-order reasoning. I have been working on ordering constraint solving, orientability problems, AC-orderings and more recently, on instantiation based methods and integration of theory reasoning into first-order logic. I have been developing and implementing iProver -- an instantiation-based theorem prover for first-order logic, which won the EPR division in two recent CASC competitions. I gave an invited talk on instantiation-based reasoning at CADE-22.
CADE is the leading conference in automated reasoning and we have seen a number of success stories at CADE including: first-order and higher-order theorem proving, satisfiability modulo theories, software and hardware verification, reasoning with description and modal logics. CADE has excelled in combining diverse areas and I believe that CADE could further promote rapidly growing and exciting areas. I strongly support the organisation of workshops co-located with CADE, as this helps to attract research work from bordering areas, which are usually published in other conferences such as CAV, RTA, LICS, ICALP, TPHOL and IJCAI.
Another attractive aspect of CADE is that it keeps a good balance between theoretical work, implementation and applications. I believe that CADE can further strengthen interaction between the research community and real-world applications. I strongly support the development of new systems and the organisation of competitions such as CASC and SMT-COMP, which help to demonstrate the possibilities of state-of-the-art systems to industrial users and conversely, propagate problems from real-world applications to the research community.
To conclude, as a CADE trustee, I would be very keen in supporting and promoting high quality theoretical research, development of reasoning systems and applications of automated reasoning.
I have been attending CADE since 1992. Since then, I have attended 13 out of 16 CADEs and IJCARs. I have served on many program committees and presented many papers. I feel a part of the CADE community, as much as I feel part of the community where I live at home. I have enjoyed working on Automated Reasoning for my entire research career. I believe it is a fundamental topic in computer science, and I would like to help make it prosper.
Over the last few CADEs, I have been excited about the direction the field is moving. There has been progress in its use in applications, such as software verification. I think the progress of the field can be partially measured by its use in applications. We need to encourage this in any way we can. As a person who works on first order, mostly resolution based, theorem proving methods, I am concerned that other areas of automated reasoning may not feel welcome in our community. I will make every effort to include the wide community in CADE and IJCAR, in order to keep the community from fragmenting. I like the current system where CADE sometimes meets on its own and other times in a larger context. We also need to think about the place of workshops in CADE and IJCAR. This year there were many workshops and not so many submissions. I think that workshops have become too much like conferences. I believe we need to make workshops more informal, with more discussion, and heavily encourage people to submit unfinished work.
In my view, CADE is the major venue for all aspects of automated reasoning research, and I regard it as the driving force to promote our field. While we should continue our emphasis on theoretical work and system building, I believe we should also reach out and welcome applications of our work in areas such as computer algebra, constraint solving, knowledge representation, mechanization of programming languages, and reasoning about programs. To foster synergy with other related areas, I support collocating CADE with conferences on related areas. Joint events such as IJCAR and collocating with FLOC are also important ways to promote the visibility of our area and demonstrate the impact of our results to the general computer science community at large.
My own research interest is in the theory and practice of logical frameworks. This includes: designing and investigating type theories and logics, building efficient verification and programming tools, and demonstrating their effectiveness using realistic applications. Since 2001, I have regularly published at CADE/IJCAR, ICLP, and, most recently, TPHOLs, POPL and PPDP.
Over the past few years, I have been actively involved in promoting our field. I was the conference chair for CADE-22 in Montreal in 2009, and the publicity chair for CADE in 2005. I am also the area editor for theorem proving for the Association of Logic Programming Newsletter. As a CADE trustee, I intend to continue working toward ensuring that automated reasoning receives the attention it deserves.
My research involves the development and theoretical analysis of reasoning methodologies and automated reasoning tools for first-order logic, modal logics used in multi-agent systems and description logics used for ontology reasoning and the semantic web. I am particularly interested in decision problems and the development of practical methods based on general principles. The current focus of my research is model building, second-order quantifier elimination, the study of the relationship between different deduction approaches and the automated synthesis of deduction calculi. I am an implementer of several automated reasoning tools for various non-classical logics and description logics and have been involved with the implementation of the first-order theorem prover SPASS.
I was Programme Chair of CADE-22. I have (co-)chaired and (co-)organised 7 other international conferences and workshops. I have (co-)edited 11 books, conference/workshop proceedings, and special journal issues. I serve on the editorial board of the Journal of Applied Non-Classical Logic, and am on the steering/organisation committee of AiML, RelMiCS and ARW (UK).
If elected I will help the board of trustees to promote high quality research in all aspects of automated reasoning. It is my strong belief that practical experience provides crucial impetus for a lot of research in automated reasoning and logic, and I will use every opportunity to promote especially practical and application-oriented research.
>From its roots in pure logic to its many practical applications in Verification, Artificial Intelligence, Combinatorics, and their subfields, Automated Reasoning (AR) spans a rich and dynamic collection of subfields, with continuing significance for Computer Science. I believe CADE is a meeting where both the theory and practice of AR, from the most abstract to the most engineering-intensive, should be welcomed and fostered. While subfields like SMT, where I began my research career, have seen a lot of recent attention, CADE must continue to promote other traditional areas, such as first-order theorem proving, higher-order logic, non-classical and modal logics, and rewriting. And while Verification, my main research interest, also continues to attract a lot of attention as an application area, other application areas like Knowledge Representation and Computer-Assisted Mathematics must also be strongly promoted. If elected to a second term, I will work to meet these goals, in part by continuing to encourage connections between CADE generally and more specialized communities like the SMT community and the verified-programming languages (i.e., type theory and dependently typed programming) community. Only by combining the strengths of our different subfields and different application areas can we continue to develop Automated Reasoning to meet the future grand challenges of Computer Science, and beyond.
My first CADE was in 1984 when I started studying computer science at Kaiserslautern. Since then I have regularly contributed to CADE as a conference participant, author, PC member and sponsor (this year's CASC computers). I worked in industry for six years, from 1999 to 2005, before returning to the Max Planck Institute for Informatics and founding the automation of logic group.
Nominee Statement:
CADE is a major conference on the automation of deduction. I will commit myself to keeping CADE the place for people working on the automation of deduction including the variety of logics, methods, and applications. It is this great many-sidedness that makes CADE unique on the conference landscape.
Developing successful systems requires often more effort than developing theory. In addition to the impressive theory results presented at CADE I will encourage "system build descriptions" at CADE. A good system culture will further strengthen the impact of our methods and our community.
The 17th Workshop on Logic, Language, Information and Computation will be held in Brasília, Brazil, from July 6th to 9th, 2010. WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning.
A title and single-paragraph abstract should be submitted by February 28, and the full paper by March 7. The proceedings will be published in Springer's LNCS series.
Refer to the conference web site for full details, including submission instructions.
The nineteenth biennial European Conference on Artificial Intelligence (ECAI-2010) will take place on 16-10 August 2010 in Lisbon, Portugal. ECAI is Europe's premier archival venue for presenting scientific results in AI.
ECAI currently solicits workshop proposals. The organizers explicitly encourage proposals from the field of Automated Reasoning. The deadline for submissions is 11 Dec 2009, but early submissions are welcome. Submission details for workshop propoals are given here.
The deadline for regular paper submission is 22 February 2010, with abstract submission until 15 February 2010, see the conference web site.
The Journal of Symbolic Computation will publish a special issue on the Automated Specification and Verification of Web Systems, edited by Temur Kutsia and Demis Ballis.
This special issue is related to the topics of the workshop WWV'09: Automated Specification and Verification of Web Systems, which took place in Hagenberg, Austria, on July 17, 2009. Both participants of the workshop and other authors are invited to submit contributions.
The editors solicit original papers on symbolic methods and techniques applied to Web sites, Web services or Web-based applications, such as:
Submission details and requirements are available from the special issue's web page. The deadline for paper submission is November 23, 2009, notification of acceptance/rejection: March 22, 2010.