I suspect that some of you might wish to return to logic, having tasted algebra and geometry recently. Therefore, a paper by John Kalman offers food for thought (Kalman, J. A., “Axiomatizations of logics with values in groups”, J. London Math. Society 2, no. 14 (1976) 193–199). In that paper, Kalman focused on the right group calculus. He relied on condensed detachment, an old friend (visited in earlier columns), the following.
% The following clause is condensed detachment. -P(d(x,y)) | -P(x) | P(y).
As discussed before, the symbol | denotes logical or, and the symbol -
denotes logical not. The expression d(x,y) can be interpreted as x times the inverse of y.
Kalman offered the following five axioms.
P(d(z,d(z,d(d(x,d(y,y)),x)))). % K1 P(d(u,d(u,d(d(z,y),d(d(z,x),d(y,x)))))). % K2 P(d(v,d(v,d(d(u,d(z,y)),d(u,d(d(z,x),d(y,x))))))). % K3 P(d(d(d(u,d(v,y)),d(z,d(v,x))),d(u,d(z,d(y,x))))). % K4 P(d(d(v,d(z,d(u,d(y,x)))),d(d(v,d(x,u)),d(d(z,d(x,y)),x)))). % K5
Yes, you have made the correct conjecture: not all of the axioms are needed. Phrased differently, one or more of the axioms can be deduced from the remaining set. In fact, a study of this five-axiom set, carried out fully, reveals that, among them, one or more can serve as a single axiom. In other words, among the five, there exists at least one with the property that the other four can be deduced from it by using condensed detachment.
The challenge for you is to find out which of the five can serve as a single axiom and, for those axioms that are too weak, find models establishing that weakness.
One of the finest researchers in automated reasoning, William McCune, made this discovery.
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 Franz Baader, Amy Felty, Larry Paulson, and Brigitte Pientka expire. There are thus four positions of elected trustees to fill.
The ex-officio position of Maria Paola Bonacina as CADE-24 program chair has also ended. Deepak Kapur has joined the board as IJCAR 2014 program co-chair.
The following candidates (listed in alphabetical order) were nominated and their statements are below:
My research area is automated deduction, with a focus on automated theorem proving in classical first-order logic and its applications. CADE is my main conference: I have been attending CADE regularly since 1990, co-authored 10 CADE papers, gave a tutorial, co-organized several workshops at CADE, and our systems participate(d) in CASC. I helped organizing CADE/IJCAR as publicity chair and workshop chair, and in 2008 I was the conference chair and PC co-chair of IJCAR in Sydney. I have regularly served on the program committee of CADE/IJCAR and I was elected CADE trustee twice, in 2003 and in 2006.
Should I be elected I would like to help making sure that CADE maintains its role as a premier conference on automated deduction. A concrete agenda item I have in mind concerns workshops. Quite frequently, proposed workshops are cancelled or need to be merged for lack of submissions these days. The steering committee could perhaps devise counteracting recommendations for future CADE workshops.
CADE is my home conference: I attended my first CADE right after finishing my undergraduate degree, and I contributed to CADE in many ways in the following years, most recently by serving as PC Chair of CADE-24. Automated deduction is at the heart of my research program, which spans many topics, including completion, distributed deduction, semantic resolution, strategy analysis, decision procedures, canonicity, integration of first-order inferences in SMT-solving, interpolation, and instance-based methods. I served as AAR secretary (1997-2004), CADE secretary (1999-2004), and CADE trustee (2004-2010), including one year as president. I was involved with the introduction of trustee elections, and with the start of IJCAR; I contributed to increase AAR membership, enhanced the AAR Newsletter, supported the growth of the Woody Blesdoe Student Travel Awards, promoted IJCAR systematically, and advocated geographical balance of conference locations.
The current rythm of having CADE in odd years, IJCAR in even years, and IJCAR at FLoC every fourth year, works very well and I support it. I am in favor of continuing with Best Paper Awards and starting test of time or most influential paper awards, for their practical utility in careers, and for historical memory, which is very important in research. My vision for our conferences is to strive for scientific excellence, nurturing creativity, cross-fertilization of ideas, openness to both new theoretical paradigms and new applications, preserving historical ties (e.g., FLoC, IFCoLoG), while being open to new ones. We need to keep working on our visibility, recognition, and attractiveness, in neighbor fields that apply our results, in the broader field of artificial intelligence, in computer science as a whole. Being a CADE trustee is about service and leadership, or leadership understood as service in the highest sense. It is about listening, remembering, foreseeing consequences, and taking responsibilities. If elected, I would bring to the board experience, institutional memory, and my unfaltering enthousiasm and energy for our ever fascinating research field.
More information on my record in research and professional service can be found on my homepage.
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 covers various areas of automated theorem proving, including interactive theorem proving (Isabelle), applications of resolution theorem proving (sledgehammer, MetiTarski), foundations of computer security, the mechanisation of mathematics, etc. I have often taken advantage of ideas shared by researchers outside my area. This is surely the best way to make progress while keeping our community together. Accordingly, I prefer broadly-based conferences that bring together researchers working in many different specialities. I would like to see CADE continue to participate in the IJCAR and FLoC meetings, where the various specialist workshops and conferences are co-located or integrated. The current pattern of holding IJCAR every two years seems to work well.
I would also like to encourage the distinction between conferences (which are ideal for the exchange of ideas) and journal publication (where definitive results appear). We should encourage a flow of publications from CADE to journals such as JAR, recognising life cycle of research findings from preliminary to definitive and comprehensive. CADE should be open to inspired student work, even if it is unpolished. At the same time, I would oppose attempts to make CADE more like a journal, in particular by having a second round of refereeing even occasionally. I’d also encourage the organisation of informal workshops with no printed proceedings, where preliminary work can be exposed to criticism and published later in a more formal venue.
I have been attending CADE, circumstances permitting, since Oxford in 1986.
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, mechanization of programming languages, and reasoning about programs. Joint events such as IJCAR and co-locating with FLOC are of vital importance. They give our area increased visibility 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, TPHOLs, ITP and more recently at POPL and ICFP. I also have served regularly on the program committee of these conferences.
Over the last few years, I have been actively involved in promoting our field. Over the previous years I was publicity chair for CADE 2005 and I currently serve on the steering committee of LFMTP (Logical Frameworks and Meta-languages: Theory and Practice). In 2009, I was conference chair of CADE. As a current CADE trustee, I have recently proposed to establish a ‘Most influential paper award’ following the model of other organizations such as ACM SIGPLAN. Such an award would recognize papers which appeared 10 years (and 15/20 years) prior and would be administered by a working group which includes some of the trustees, the PC chairs of CADE (N-10) and CADE N. If elected for a 2nd term, I aim to work with the CADE trustees and the CADE community to set up such an award. I also intend to work towards establishing a similar award for IJCAR. My general motivation and aim is to ensure that automated reasoning receives the attention it deserves.
The constant stream of technical innovations, driving the fields of social networks, mobile communication, geographic information systems, big data, embedded systems etc, is creating new complexities, new challenges and new opportunities for the automated reasoning community. Advances in modeling, logic engineering, and software verification requires research on faster automated reasoning algorithms, more powerful sovers, novel decision procedures, and innovative reasoning tools in the pioneering spirit of the CADE research tradition.
If elected a CADE trustee, I will work towards the following goals:
I have been a member of the CADE community for nearly 20 years and have extensive experience in the fields of automated reasoning, programming languages, proof assistants, and applications. I am one of the principal authors of the Twelf system, the Delphin programming language, and the Celf system. Since 2011, I am leading an international and interdisciplinary research project on democracy and technology.
We invite proposals for sites around the world to host the Conference on Automated Deduction (CADE) to be held in summer 2015 as a stand-alone conference. In some other years, CADE is held as part of FLoC and sometimes merges with other automated reasoning conferences into IJCAR. CADE's/IJCAR's recent location history is as follows:
CADE's/IJCAR's near location future will be as follows:
The deadline for proposals is: September 30, 2013
In addition, we encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
Perspective organizers are encouraged to get in touch with the CADE secretary and president (see contact information below) for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.
Franz Baader, CADE President
baader (at) tcs.inf.tu-dresden.de
Martin Giese, CADE Secretary
martingi (at) ifi.uio.no
FroCoS 2013, the 9th International Symposium on Frontiers of Combining Systems will take place in Nancy, France, on 18–20 September 2013. FroCos will be co-located with TABLEAUX 2013, the 22nd conference on AR with Analytic Tableaux and Related methods.
In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation and automated reasoning, there is an obvious need for using specialised formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialised systems must be combined with each other, and they must be integrated into general purpose systems.
Like its predecessors, FroCoS 2013 seeks to offer a common forum for research in the general area of combination, modularization and integration of systems, with emphasis on logic-based ones, and of their practical use.
NOTE: Early registration is until 31 July 31. For online registration, visit this web page. Please note the reduced fees for the joint registration FroCoS+TABLEAUX.
The Sixth Federated Logic Conference (FLoC 2014) will be part of the Vienna Summer of Logic (VSL), the largest logic event in history, with over 2000 expected participants. FLoC 2014 will host eight conferences and many workshops. Each workshop will be affiliated with one of the eight conferences.
Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense. Each workshop proposal must indicate one hosting conference among the participating conferences.
It is suggested that prospective workshop organizers contact the relevant conference Workshop Chair before submitting a proposal.
For full details, please refer to the FLoC Workshop Guide.
The 10th International Workshop on the Implementation of Logics will be held on 14 December 2013, colocated with the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning in Stellenbosch, South Africa.
IWIL is looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. IWIL is particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice.
Submissions of in a variety of categories are accepted until 14 October 2013. For further details, please refer to the Workshop web page.
The Second International Workshop on Design and Implementation of Formal Tools and Systems (co-located with FMCAD and MEMOCODE 2013) will be held in Portland, OR, USA, on 19 Octobter 2013.
The DIFTS (Design and Implementation of Formal Tools and Systems) workshop emphasizes insightful experiences in formal tools and systems design. DIFTS takes a broad view of the formal tools/systems area, and solicits contributions from domains including, but not restricted to, decision procedures, verification, testing, validation, diagnosis, debugging, and synthesis.
The paper submission deadline is 24 July. See the DIFTS web page for further details.
PAS 2013, the Second International Seminar on Program Verification, Automated Debugging, and Symbolic Computation will be held in Beijing, China,on 23–25 October 2013.
PAS 2013 will provide a forum for foreign and Chinese researchers and software developers actively involved or interested in developing, using, and applying methods and software tools of symbolic computation for program verification and automated debugging to exchange ideas and views, to review the state of the art and discuss prospects, to present research results and experiments, and to build up contacts for future cooperation. The scientific program of the seminar will feature invited talks and short presentations.
Topics of interest include (but are not limited to):
If you are interested in attending this seminar and giving a 25-minute talk, please send the title and an abstract of your talk to the organizers by 10 September 2013.
Please refer to the seminar web page for further information.
Dear AAR members,
I am a (nearly graduate) CS student at University of Potsdam (Germany). Currently I am trying to focus my plans for my PhD. During the last years, I have been doing research in the field of theorem proving and attended the CADE ATP Systems Competition twice (CASC-J6 and CASC-24) .
In order to focus my plans for my PhD, I am trying to get some impressions about the experiences of implementers and users of theorem provers (interactive and automated) and theorem proving assistents (e.g. preprocessors for theorem proving). The scope is to collect some information about the use of theorem provers and the strengths and weaknesses which are seen by users. Also, usually missing functionality and gaps are in my scope.
Thus, I created a small survey which I would like to distribute.
I assure that all information given will be treated as confidential and no information about the people who filled in the survey will be disclosed.
The survey can be found on this web page.
Sincerly,
Mario Frank