Is one of your goals to convey the excitement, intrigue, and--yes--beauty of mathematics to a relative, a friend, a spouse, or a student?
If it is, in the book “Automated Reasoning and the Discovery of Missing and Elegant Proofs” you will find a wealth of material—from problems that challenged experts for decades, to eureka moments of discovery, to open questions still remaining. Chapter 5 of that book presents numerous gemstones for you to share with a novice, gemstones involving a nested set of algebraic varieties that move from the more familiar to the less familiar: Boolean algebra, modular ortholattices, orthomodular lattices, ortholattices, complemented lattices, lattice theory, and quasilattice theory.
To help you begin your mining foray, and as a precursor to columns I suspect I shall write in the future, I now give you an independent axiomatization of quasilattices in terms of meet (intersection) and join (union).
% Quasilattice Theory (QLT) x ∨ y = y ∨ x. % commutativity of join (x ∨ y) ∨ z = x ∨ (y ∨ z). % associativity of join x ∨ x = x. % idempotence of join x ⋀ y = y ⋀ x. % commutativity of meet (x ⋀ y) ⋀ z = x ⋀ (y ⋀ z). % associativity of meet x ⋀ x = x. % idempotence of meet (x ⋀ (y ∨ z)) ∨ (x ⋀ y) = x ⋀ (y ∨ z). % first link law (x ∨ (y ⋀ z)) ⋀ (x ∨ y) = x ∨ (y ⋀ z). % second link law
Each variety is a proper subset of its successor, except of course the last, which has none—as far as I know.
For this column, I'll focus on the first of these varieties, Boolean algebra, presenting a set of challenges for you to address. In the following equation, the function f denotes the Sheffer stroke, the (logical) nand, the not of and.
f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y.
Your first challenge is to prove that this equation is a single axiom for Boolean algebra. Your second challenge, with my hint that you begin by relying on a Knuth-Bendix approach, is to find a proof that is free of demodulation. Your third challenge is to find a proof that is free of demodulation and that is a forward proof.
The following is a target denial as a possible goal.
f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))).
As a reminder, the vertical bar | denotes logical or.
To be honest, many years ago the automated reasoning group at Argonne successfully addressed all three challenges. Our exploration involved several people. Specifically, it began with an examination of 25 cases, presented by S. Wolfram, for Boolean algebra in terms of the Sheffer stroke. Robert Veroff proved that two candidate pairs are 2-bases for Boolean algebra in terms of the Sheffer stroke. Using Veroff's proof, Bill McCune then showed that two of the one-member candidates are each a single axiom. B. Fitelson and K. Harris showed that no shorter single axiom exists. And yes, using various methodologies, a demodulation-free forward-reasoning proof was found.
Why, then, do I present these challenges here? The answer is threefold. First, in a kind of pass-it-forward action, I hope to have you experience some of the excitement our group experienced, and perhaps to have you convey some of that excitement to a colleague or student who might then decide to tackle other problems with an automated reasoning program. Second, I hope that one (or more) of you will find a shorter proof than the 66-step proof I succeeded in finding (if you succeed, please let me know). And third, by mentioning some of the experts who helped produce these proofs, I hope to encourage you to browse on the Internet to sample the work of any of these individuals. With such browsing, you will begin profitable and enjoyable journeys.
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 Viorica Sofronie-Stokkermans and Geoff Sutcliffe expire. Both are eligible to be nominated for a second term. Bernhard Gramlich served as CADE trustee until his untimely passing earlier this year (cf. the obituary in the previous Newsletter), so one additional trustee needs to be elected. There are thus three positions of elected trustees to fill.
The term of office of Deepak Kapur as IJCAR 2014 program co-chair also ends. As outgoing ex-officio trustee, he is eligible to be nominated as elected trustee. Amy Felty has joined the board as CADE-25 program co-chair.
The following candidates were nominated and there statements are below
My research covers various aspects of Automated Deduction, both on the theoretical and practical side. I'm currently focused on the development of tools and techniques for SMT. Hence, my interests span many topics of CADE, and I particularly like the fact that the conference values both theoretical and practical works on automated deduction. CADE has a particular emphasis on tools: this has been (and remains) essential for the development of the field. I attend CADE and IJCAR whenever possible. My involvement in the organization of CADE is still young and modest, but I have recently been organizing FroCoS, the SMT workshop, the SAT/SMT summer school, and I have been an elected member of the SMT steering committee.
CADE has the crucial mission of cross fertilizing the various trends in automated deduction. I believe this mission is increasingly important especially now because we are seeing convergence, like with SMT and FOL provers. CADE should remain open to the various trends, and should be increasingly the home conference for them. The current cycle of conferences, CADE alternating with IJCAR, and IJCAR as a part of FLoC every four years, is, I believe, the right organization for the current situation, since it preserves the specificity of CADE and of the other compound conferences of IJCAR.
The future of the automated reasoning community relies on students. We have to find ways to attract the best students, provide a friendly atmosphere for them to discuss with other researchers, and organize events to ease learning of state-of-the-art knowledge. I believe we have to even further promote CADE to students, using financial incentives for their participation, as well as organizing tutorials and summer schools co-located with the conference. At the start of their career as researchers, it is important to provide visibility and recognition to excellent works conducted by students; when applicable, CADE should give best paper awards, and best student paper awards.
As a trustee, my goal would be to keep the scope of CADE as broad as possible. CADE should be open to any aspect of automated deduction and it should cover everything from theoretical results and practical contributions up to applications of automated reasoning. It is important to make clear that every sub-field of automated reasoning is highly welcome at CADE to ensure CADE's position as the leading main conference of the field.
I also think that it is very important to attract tool submissions, and to organize tool competitions co-located with CADE. (Since its foundation in 2004, I have been active in the termination competition, which took place during IJCAR/CADE several times.)
I think the current organization of CADE as a stand-alone event every second year, within IJCAR every other year, and within FLoC every four years is a very good solution to guarantee the visibility of CADE on its own, while keeping in close contact with neighboring meetings and fields.
To attract as many participants as possible and to allow students to attend the conference, I think CADE should aim at affordable conference fees and continue the very good tradition of Woody Bledsoe travel grants for students.
My own research is concerned with different aspects of automated deduction. Therefore, I have been attending and publishing papers at CADE since 1994. In particular, I am working on techniques and tools to analyze properties like termination or complexity of programs automatically.
I was one of the PC chairs of IJCAR 2010, PC chair of RTA 2005, steering committee chair of RTA (2005–2007), area editor of ACM TOCL (since 2013), and I served many times on the PCs of CADE, IJCAR, RTA, LPAR, and several other conferences in the field.
My research focuses on theoretical, implementation and application aspects of automated reasoning. I have been working on instantiation-based methods, EPR-based verification, linear arithmetic, 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 and the first-order satisfiability divisions (FNT) at recent CASC competitions. I gave invited talks at CADE-22, FroCos'13 and a number of workshops. 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), 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 which helps to achieve the goal of bringing together the wider research community. 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 a large number of 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, 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 researchers 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 was 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 centers around understanding proof search and efficient implementations of inference engines, much of it embodied in the theorem prover E. I've recently returned to academia as professor of computer science at Baden-Wuerttemberg Cooperative State University Stuttgart.
CADE is my main conference. I have been a regular attendee of CADE/IJCAR since 1996, and have presented several papers and tutorials. I have co-organized 8 workshops at CADE/IJCAR, including the on-going series on "Practical Aspects of Automated Reasoning".
CADE is a medium-sized conference. As such, it must tread a fine line between being open for new topics, and staying focused enough to work as a forum for Automated Reasoning research. In my opinion the interleaving of CADE and IJCAR contributes to striking this balance, and I support its continuation. Another balance close to my heart is the one between theory and implementation. CADE has always been a major forum for new theoretical results in the field. Support for practical results, especially full papers, has been less steady. I think CADE should welcome such results—the proof of the pudding is in the eating, and the proof of the calculus is in the ATP system.
CADE is the leading conference in automated reasoning, and the major forum for discussing all aspects of automated theorem proving, including theory, implementations and applications. I believe that progress in this field can only be achieved by supporting all these aspects: new theoretical results create the basis for new powerful implementations, which in turn allow to use automated reasoning techniques in wider areas of applications. It is also essential to attract high-quality papers from new or related fields (SAT, constraint solving, computer algebra, verification, knowledge representation, complexity) as well as papers which combine automated reasoning with results from other areas. It is equally important to create the possibility of meetings—such as IJCAR—where the entire automated reasoning community meets; and to ensure the participation of IJCAR within FLoC.
Over the years I worked in several areas of automated reasoning (including non-classical logics, first-order logic and, in the last years, reasoning in extensions and combinations of logical theories). The results of my research turned out to be very useful in applications—especially in verification. I frequently publish and participate in CADE and IJCAR. I was program co-chair of CADE-23, the conference chair of FroCoS 2011, program co-chair of FTP'2009 and am regularly on the PC on numerous automated reasoning conferences. I organized several workshops (affiliated with CADE, IJCAR and ACA) with the goal of creating synergies between various scientific communities (logic, deduction, complexity; resp. deduction, symbolic computation, verification).
If elected as a CADE trustee, my goals will be:
In addition, I will fully support CADE's efforts to provide financial assistance for young researchers for attending the conference.
I believe that the advancement and application of automated reasoning depends on recognizing and supporting the synergetic interaction of theoretical progress, high performance implementation (techniques), and application requirements. I strongly support research and development that leads to effective implemented systems that are deployed in research and industrial applications. I expect CADE/IJCAR to remain the major forums for the presentation of new research in all aspects of automated deduction. As such our conferences must reflect the depth, breadth, and interaction of all aspects of automated reasoning, to allow a broad automated reasoning community to use CADE (and IJCAR) as the preferred conference for the presentation of research results. I support efforts to provide financial assistance that enables young and poor researchers to attend the conferences. I endorse CADE's leading role in IJCAR and continued participation in FLoC.
I started my academic career at Edith Cowan University in 1986, taught at James Cook University from 1992 to 2001, and am now professor and chair of Computer Science at the University of Miami. I am probably best known in the automated reasoning community for the TPTP Problem Library and the CADE ATP System Competitions (CASC). I have been attending CADE since CADE-10 in 1990 and have hosted CADE twice—in Australia in 1997 and in Miami in 2003. I have been on the CADE/IJCAR program committee eleven times. I am responsible for the CADE and IJCAR web pages.
In August 2014 the CADE Board of Trustees established the Thoralf Skolem Award to reward a CADE paper that has passed the test of time by being a most influential paper in the field. Beginning with CADE-25 (2015), at every CADE the Skolem Award Committee selects a paper presented at the CADE held 10 years earlier to receive the Skolem award.
Every CADE has its own Skolem award committee, whose office terminates with the CADE for which it was appointed. The CADE board of trustees appoints the chair of the Skolem award committee, and the chair appoints the rest of the committee. The committee agrees on a proposal and its chair presents it to the CADE board. It is expected that in most cases the CADE board will simply approve the proposal of the Skolem award committee. Under exceptional circumstances, two awards (ex aequo) or no award may be given.
In order to cover the entire history of CADE, beginning with CADE-25 (2015), in addition to the Skolem award to a paper presented at the CADE held 10 years earlier, every CADE conference offers three additional Skolem awards for papers presented at CADE's held approximately 20, 30, and 40 years earlier. Whenever a CADE offers multiple Skolem awards, one single Skolem award committee is responsible for all of them. The Skolem award schedule follows. On the account of their workshop status, a few very early CADE's are combined under one Skolem award.
Steady state is reached in 2027 when CADE-32 offers only one Skolem award.
For further information about the Skolem Award, refer to the CADE Inc. Web Site.
The 25th International Conference on Automated Deduction will be held in Berlin, Germany, 1–7 August 2015.
CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference invites high-quality submissions on the general topic of automated reasoning, including foundations, applications, implementations and practical experiences.
The CADE program will include the annual CADE ATP System Competition (CASC), as well as various workshops and tutorials. Details will be published in separate calls and on the conference website.
CADE calls for regular papers of up to 15 pages and system descriptions of up to 10 pages.
Papers shall be submitted until 23 February 2013. An abstract must be submitted already on 16 January 2015. Accepted papers will be published in Springer's LNCS series.
Please refer to the conference web site for further information, including the full Call for Papers.
CADE-25 is soliciting proposals for workshops, tutorials, and system competitions to be held in conjunction with the conference.
Proposals should be submitted until 14 November 2014, and notifications are scheduled to be sent out on 28 November 2014.
The conference web site contains details about required information, submission procedure, etc.
LATA 2015, the 9th Intl. Conf. on Language and Automata Theory and Applications will be held in Nice, France, on 2–6 March 2015. Topics of interest include theoretical and applied aspects of connections between automata and logic, term rewriting, and others that may be of interest to the AAR community.
The paper submission deadline is 10 October 2014. Accepted papers will be published in a Springer LNCS volume. For details, please refer to the conference web site.
The seventh NASA Formal Methods Symposium will take place in Pasadena, California, USA, from 27 to 29 April 2015. NFM is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. Submissions on cross-cutting approaches are encouraged, marrying formal verification techniques with advances in safety-critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages carrying throughout system development.
Accepted papers will appear as a Springer LNCS volume. Full papers of up to 15 pages, or short papers of 6 pages, may be submitted until 10 November 2014. For full details, refer to the symposium web site.
John Harrison, Josef Urban and Freek Wiedijk are asking for contributions to a special issue of the Journal of Formalized Reasoning demonstrating the state of the art in formalization of mathematics 20 years after the QED Manifesto and the related 1994 and 1995 QED Workshops.
The purpose of this special issue is to demonstrate the state of the art in formalization of mathematics 20 years after the QED Manifesto and the related 1994 and 1995 QED Workshops, and to show how we are (not yet) achieving the QED goals. The topics of interest include:
The deadline for submissions is 1 December 2014, expected publication in JFR is April–May 2015.
See the QED+20 workshop page for further details, and the complete CfP for submission instructions.