As I promised, I now offer more challenges from algebra. You may especially enjoy these challenges because I have tried, and failed, to meet them. I thank Sherman Stein for bringing the theorem in focus, as well as others, to my attention.
In group theory, many of you are familiar with the theorem that says commutativity can be proved for groups in which the square of x, for every x, is the identity, xx = e. Well, other identities permit the deduction of commutativity. For example, so I am told, for any combination of positive integers a, p, and q, commutativity can be deduced from the following:
T31: yx = xayxpyq
For convenience, note that a group admits a two-sided identity, e, and, with respect to e, a two-sided inverse exists, a y for each x with xy = yx = e.
Your first challenge is to prove that commutativity holds in groups satisfying T31. You might, as a hint, turn to a Knuth-Bendix approach. If so, your second challenge is to find a demodulation-free proof, either by converting a Knuth proof or by directly turning to paramodulation. Your third challenge is to prove commutativity from T31 for monoids, no inverse is allowed. Finally, your fourth and last challenge is to prove commutativity for semigroups from T31. For that challenge, note that you can only rely on T31 and on associativity.
Now, for any and all challenges, you might resort to induction. Implicitly, each challenge asks for a first-order proof. For the curious, I am not in any way alone in my interest in first-order proofs. Many mathematicians and logicians seek first-order proofs, as was the case (implied) in an earlier newsletter in which a theorem of Hiz was the focus. If you succeed, especially if your result is demodulation-free, but not exclusively, I would enjoy seeing your proof.
An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:
The terms of Rajeev Goré, Renate Schmidt, and Christoph Weidenbach expire. There are thus three positions of elected trustees to fill.
The ex-officio position of Bernhard Gramlich as IJCAR 2012 program co-chair ends, and Maria Paola Bonacina has joined the board as CADE-24 program chair.
The following candidates (listed in alphabetical order) were nominated and their statements are below:
My research spans sequent calculi (AiML) and tableau methods for non-classical logics (TABLEAUX); complexity-optimal methods for automated reasoning in description logics with inverse roles (DL), fixpoint logics like CTL (LPAR), PDL (M4M, CADE) and CPDL (IJCAR); termination of term rewriting (CSL); reasoning about intruder theories in security (RTA); machine-checking proofs of cut-elimination using Isabelle (TPHOLs); using BDDs for automated reasoning in non-classical logics (IJCAR, PAAR); and automated reasoning in business process modelling (CAiSE). Thus I have a broad background in automated reasoning, in both theory and practice.
I think that holding IJCAR every second year is a “good thing” as it allows the constituent communities to retain a forum for their non-AR related interests in alternate years. I think that IJCAR@FLoC is also an excellent way to keep us in touch with other areas of logics in computer science. I think that having multiple co-chairs for IJCAR reflects the many diverse sub-themes of our area, and I see no need to try to “unify” these sub-themes into an annual IJCAR with only one PC chair.
I am the outgoing two-time president of the TABLEAUX Steering Committee (so I cannot serve again), and I have been a CADE Trustee twice. Why do I want to stand again? Because I believe that my broad background allows me to understand and represent the views of the many different communities that make up CADE, both from a theoretical and a practical perspective.
I have a broad view of automated deduction concerning “automated” as well as “deduction.” Automated may be fully automated, automatically supported, interactive, strategy-guided…, deduction may be first- or higher-order, involve general or inductive theorem proving, rely on classical or non-classical logic… For CADE as the major forum in the field implementations, tools and competitions are vital to reflect and measure practical progress. Theoretical fundamental research is equally important and indispensible, being the basis of the former. In addition, applications provide benchmarks and test cases and thus feedback whether the theory and the tools are successful in practice.
My own main research area is rewriting, the automatically supported analysis of properties of rewrite systems as well as the application of rewriting techniques for programming, automated deduction and more generally reasoning. More concretely, I've been working on topics like inductive theorem proving, proof engineering, rewriting and deduction strategies, and automated modular termination proofs. A more recent focus is the analysis of conditional rewriting, computation and deduction. Since rewriting is the technical basis of many computational mechanisms in automated deduction like simplification or redundancy elimination, there is a close connection between rewriting and (automated) deduction for which I would like to raise awareness. I was IJCAR PC-Co-Chair in 2012 and FroCoS PC and Conference Chair in 2005, and have often served as PC-member of e.g. IJCAR, CADE, FroCoS and RTA.
Concerning CADE Inc. and the position of the Trustees, I think that CADE should stay with IJCAR bi-annually (but not more often) and be open for new events to join. And having a FLoC (with IJCAR) every 4 years makes sense, but should not happen more often. The selection/appointment policy concerning venue, Conference and Program Chair should continue to keep a reasonable geographical balance. Also the support for young researchers (e.g. via travel grants to CADE/IJCAR conferences) should be continued. CADE could, in my opinion even should, try to attract authors/speakers/papers from neighbouring or separate fields and communities (e.g. CAV, ITP, SMT, automated SW-engineering/specification/verification/testing) and concerning emerging trends (e.g. computational biology) in the form of a “friendly competition.” Finally, I see the CADE Board of Trustees also as the right forum for strategic discussions and initiatives, for instance, concerning funding policies, political initiative(s) or summer/winter schools for young researchers.
My research focuses on theoretical, implementation and application aspects of automated reasoning. I have been working on instantiation-based methods, linear arithmetic, integration of theory reasoning, ordering constraints, orientability and AC-orderings. I have been developing and implementing iProver – an instantiation-based theorem prover for first-order logic, which won the EPR division at the recent five CASC competitions and the FNT division at CASC@Turing in 2012. I gave an invited talk on instantiation-based reasoning at CADE-22.
I was a conference co-chair and co-organiser of IJCAR 2012, held at the University of Manchester. As such, I played an active role in attracting and supporting a large number of workshops (12), an unprecedented number of system competitions (4) and Woody Bledsoe Student Travel Awards (27).
CADE excels in combining diverse research communities and fosters rapidly growing and exciting areas. I believe this tradition is vital for the success of CADE. Therefore I strongly support the participation of CADE within IJCAR and FLoC; the collocating with other large research meetings, such as the Turing Centenary Conference in 2012, which help to achieve the goal of bringing together wider research communities. Likewise, I strongly support the organisation of workshops, tutorials and competitions co-located with CADE. I believe it is important to support not only well-established workshops but also smaller workshops/competitions promoting novel topics in the area. Attracting and supporting students and young researchers is vital for the future development of automated reasoning and CADE. For this it is important to have low student conference fees, secure funding for student travel awards and to involve students in on-site conference organisation. We had a rewarding experience at IJCAR 2012 with students supported by the Woody Bledsoe Awards.
CADE maintains a good balance between theoretical work, implementation and applications. I believe CADE can further strengthen interactions between the research community and real-world applications. I thoroughly support the development of new systems and competitions such as CASC/SMT-COMP/SAT Competition/Termination/OWL Reasoner Evaluation and many others, which demonstrate the possibilities of state-of-the-art reasoning systems to a wide range of users and conversely, propagate problems from real-world applications to the research community.
As a CADE trustee, I will be devoted in supporting and promoting high quality theoretical research, development of reasoning systems and interaction between theory and applications. I will do my best in attracting and supporting young researches in the area.
I have been attending CADE since 1992. Since then, I have attended most CADEs and IJCARs. I have served on many program committees and presented many papers. I am co-organizer of CADE in 2013. 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.
I am excited about the direction the field is moving recently. 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. I believe we need to make workshops as informal as possible, with more discussion, and encourage people to submit unfinished work.
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 resolution and tableaux. The current focus of my research is tableau synthesis, minimal model generation and second-order quantifier elimination. I am an implementer of several automated reasoning tools for various non-classical logics and description logics and have contributed to the first-order theorem prover SPASS.
I was Programme Chair of CADE-22. I have (co-)chaired and (co-)organised 9 other international conferences and workshops. I have (co-)edited 16 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 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 will use every opportunity to promote especially practical and application-oriented research.
Personal:
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, trustee (2009–2012) and sponsor ( 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. End of 2011 I started a company that sells theorem proving technology to industry.
Nominee Statement:
CADE is the 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.
We see now that more and more of our technologies find their way from academia to industry, in particular through systems. 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 papers” at CADE. A well-developed system culture will further strengthen the impact of our methods and our community.
The Steering Committee of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods currently has three elected members whose terms expire in 2012:
The current Steering Committee rules and current membership can be found on the Tableaux conference series web page.
The ex-officio membership of George Metcalfe (University of Bern) as the representative of TABLEAUX 2011 ends in 2012. George will be replaced by one of the Co-Chairs of TABLEAUX 2013 (TBA). Rajeev Gore is ineligible to stand again as he has served two consecutive terms. Martin Giese and Valentin Goranko are eligible to be nominated for a second term
The Steering Committee is therefore calling for nominations of candidates who wish to contest an election for three positions which will be held in October 2012. Voting will be via mail, fax or email using a single transferable voting system. Eligible voters are those who are deemed to be members of the Tableaux community as defined below.
The Tableaux community consists of all people who have been registered participants in at least one of the 3 most recent Tableaux Conferences including IJCAR (i.e. IJCAR 2010, TABLEAUX 2011 and IJCAR 2012) and all members of the current Program Committee (i.e. IJCAR 2012 PC). Only members of the tableaux community may act as nominators.
To nominate please send an email to Rajeev.Gore (at) anu.edu.au
containing:
Closing date for nominations is 30 September 2012.
The 3rd International Conference on Interactive Theorem Proving will take place at Princeton, NJ, USA, on 13–15 August 2012 with colocated workshops on Coq and Isabelle on August 12th.
Registration is now open and the technical program is now available via the conference web site.
Highlights of the conference:
The Software Testing, Verification & Reliability (STVR) journal invites authors to submit papers to a Special Issue on Tests and Proofs.
The increasing use of software and the growing system complexity make focused software testing a challenging task. Recent years have seen an increasing industrial and academic interest in the use of static and dynamic analysis techniques together. Success has been reported combining different test techniques such as model-based testing, structural testing, or concolic testing with static techniques such as program slicing, dependencies analysis, model-checking, abstract interpretation, predicate abstraction, or verification. This special issue serves as a platform for researchers and practitioners to present theory, results, experience and advances in Tests and Proofs (TAP).
Topics of interest include, but are not limited to:
The deadline for submissions is 17 December 2012. Notification of decisions will be given by 15 April 2013.
For further information and submission details, see here.
The summer school on verification technology, systems and applications happens this year at the Max Planck Institute for Informatics. The school will take place from 3–7 September, 2012.
The following speakers have accepted to give courses:
Participation is free (except for travel and accommodation costs) and open to anybody holding at least a Bachelor degree (or equivalent) in computer science. The number of participants is limited. Please apply electronically by 1 August, 2012 by sending
to lamotte (at) mpi-inf.mpg.de
For details please see the Web page of the school.
A tenure track research position is available at the Embedded System Research Unit of the Center for Information and Communication Technology, Fondazione Bruno Kessler in Trento, Italy.
The FBK center for ICT is looking for a candidate to carry out research activities in the field of Automated Reasoning for the Design of Embedded and Cyber-physical systems. The successful candidate will primarily work on the development of efficient algorithms and tools for the design and verification of complex embedded systems.
The research activity focuses on the development of symbolic methods for the automated analysis, in particular methods based on model checking and Satisfiability Modulo Theories. The candidate is expected to carry out research activities in the context of critical application domains, including but not limited to the aerospace, railways, automotive, and factory automation sectors. The selected candidate will join the Embedded Systems research unit in the FBK center for ICT.
For further details, including the application procedure, please refer to the job openings page of FBK by 19 August 2012.
A 3 year postdoctoral research position is available at the University of Oslo, Norway, Dept. of Informatics, in the research group “Logic and Intelligent Data”.
The candidate will contribute to a newly established large-scale Integrating Project funded under European Commission FP7. The project is centered on ontology-based data access and query rewriting, applied to large-scale industrial data repositories. The project combines cutting edge database technology, semantic technologies, and human interface aspects. Relevant topics for the candidate's work include in particular
Applicants should have a strong background in either database technology, semantic technologies or applied logic.
Please refer to the vacancy web page for details about the position. You will find a link "Send application" on that page which leads you to a web portal where you can submit your application.
Queries about the position can be sent to both Martin Giese (martingi (at) ifi.uio.no) and Arild Waaler (arild (at) ifi.uio.no).
Application deadline 15 August 2012. Starting date: no later than 1 October 2012.