A charming set of mathematical varieties move from the more familiar to the less familiar: Boolean algebra (BA), modular ortholattices (MOL), orthomodular lattices (OML), ortholattices (OL), complemented lattices (CL), lattice (L), and quasilattice (QL). Each variety (class of objects) is a proper subset of its successor, except of course the last, which has none–as far as I know. In the September and December 2014 columns of the AAR Newsletter, I discussed BA and MOL, respectively. After more than a year's hiatus, I turn now to OML and offer you several challenges and an open question.
As in those earlier columns, I rely here on the Sheffer stroke, the nand (logical not), as the sole function. Equality plays the only role; and you are as usual advised to include reflexivity, x = x, in your attempts to meet one of the challenges I offer, if you plan to rely on the inference rule paramodulation.
I begin with the discovery by Bill McCune and Michael Rose of a 23-letter single axiom for OML, the following, where the function f denotes the Sheffer stroke.
f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x. % OML-singax
Your first challenge is to prove from this single axiom elements of the following 3-basis for OML. Each is presented in its negated form because I assume you will seek a proof by contradiction. (In OTTER, the ANSWER literal, which can be denoted by ANS, is used when a proof is complete to tell the researcher which proof has been found; OTTER allows the researcher to seek more than one proof at a time in a single run.)
f(f(a,a),f(a,b)) != a | $ANS(absorption).
f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))) | $ANS(associativity).
f(a,f(a,f(a,b))) != f(a,b) | $ANS(OML).
f(a,b) != f(a,f(a,f(a,b))) | $ANS(OML_flip).
You might naturally wonder about the inclusion of the so-called flip of the OML property. The reason is that I suspect that some of you will turn to Knuth-Bendix, which I think may benefit from having access to the flip of this property.
I also offer three additional challenges. In the first of these, you are asked to find a proof of each of the properties, and, of course, of their join, in which demodulation plays no role. In the second, you are asked to find a proof that is forward, neither bidirectional nor backward. And in the third, you are asked to find a proof that is both forward and free of demodulation. Will you be tempted to use some form of AC-unification?
I note that the three properties of the cited 3-basis are not equally difficult to prove. Indeed, as you might expect from other journeys into areas of algebra, associativity is harder to prove than are each of the other two; and the OML property is clearly harder to prove than is absorption.
Then, depending on your approach, you may find that your program can also prove the following two properties, each stated in negated form.
f(A,B) != f(B,A) | $ANS(commutativity).
f(A,f(A,A)) != f(B,f(B,B)) | $ANS(one).
The "one" property may be harder to prove than commutativity. Each of commutativity and the one property will most likely be proved, if at all, before a proof of associativity is offered by your program.
I also present later in this column hints about possible approaches–hints that I hope you will not read until you have attempted to meet the challenges given so far. As a reward for not looking at the hints, I make observations that might be especially interesting to those who enjoy the relation of one variety to another.
For the curious, especially those who accepted my challenges in late 2014 regarding MOL, I note that if you adjoin the following property to the three negated equations, each of course phrased in a positive form, you obtain MOL from OML.
f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). % modularity
And, for those who enjoy seeking models, finite or infinite, can you find a model of an OML that is not an MOL? As an aside, if you then adjoin distributivity to your amended axiom system for an MOL, you obtain Boolean algebra.
I promised an open question for consideration, and I now present more than one. Given the fact that mathematics now knows of a 23-letter single axiom for OML lattices, the question–still open from what I know–asks about the existence of a shorter single axiom in terms of the Sheffer stroke. If memory serves, Branden Fitelson and colleagues showed that none can exist of length strictly less than 21. Does there exist a second single axiom for OML of length 23? How long is the shortest single axiom for OML in terms of complement and join (union)? There does exist a single axiom in terms of complement and join, but no "nice" one is known (from what I recall).
And now, for your patience you merit a reward in terms of hints about meeting some of the earlier challenges. I begin with a reminder that paramodulation, being a term-oriented inference rule, can be fecund. Indeed, from but two parents, depending on their nature, you can obtain with paramodulation a number of conclusions. In contrast to, say, hyperresolution in the context of condensed detachment where at most two conclusions can be drawn from a pair of parents (two so-to-speak children can be found), with a moderately complicated equation as the sole initiator of the search, the program applying paramodulation applied to two copies of the equation can draw a surprising number of conclusions, sometimes more than fifty. In the context of OML, if you take two copies of the given 23-letter single axiom and apply paramodulation, you will obtain quite a few conclusions. In other words, from a level-saturation approach, there exist quite a few level-1 clauses (which I leave to you to produce, if desired). Among them is a so-called heavy clause, if measured solely in terms of symbols present. Therefore, if your program provides the capability, you may find it useful–or perhaps required–to permit heavy conclusions to be retained.
For a second hint, if your program offers a parameter that focuses on the number of distinct variables in a retained conclusion, you will almost certainly find your attempts to meet a challenge influenced by the value you assign to that parameter.
For a third hint, I note that in OTTER the default is to block paramodulation from and into a variable. After all, permitting either will always succeed; unification cannot fail. If you relax either constraint, a program applying paramodulation will yield even more conclusions. I have not investigated allowing paramodulation from or into a variable, and I have no idea what will occur. Would either action enable a program to meet one or more challenges more easily?
Possibly entertaining for you, and certainly a surprise for me, was what occurred when I was preparing this column. I had a 46-step proof that deduces the cited 3-basis from the 23-letter single axiom, a proof that includes a deduced step relying on five distinct variables. I conducted, as you might have predicted, experiments of the type I am suggesting here. Specifically, I relaxed certain constraints–the apparent keys being the relaxation of the number of distinct variables permitted in a deduced-and-retained conclusion and the assignment to max_weight (which measures the complexity of a statement). To my delight I found a 44-step proof, a proof new to me and one that McCune, were he still with us, would have enjoyed reading. McCune's interest in shorter proofs had, in fact, motivated my discovery of the 46-step proof in 2003.
Arguably, one might object that the proof is shorter but less elegant–that it has more variables. My main focus has been on proof lengths, but I acknowledge that various logicians and mathematicians are interested in diverse aspects of proof elegance–shortness of proof, size in total symbols of proof, so-called messiness, and the like.
It is with the deepest sadness that we announce Helmut Veith's passing on 12 March 2016. Helmut was a brilliant researcher, an inspiring collaborator, a stimulating teacher, a generous friend, and a wonderful father and husband. He leaves a void that will be impossible to fill. Our thoughts are with his family and friends. Obituaries remembering Helmut.
If you have photos of Helmut (or him together with his friends) which you would like to share with others, please send them to Katarina Singer at singer at forsyte dot at.
In memory of Helmut, we will institute an award to support promising students. We are asking for contributions. Contributions to the Helmut Veith Award can be made to
I am happy to announce that Zohar Manna and Richard Waldinger will jointly receive the Herbrand Award at IJCAR 2016, for their pioneering research and pedagogical contributions to automated reasoning, program synthesis, planning, and formal methods.
Nominations for four CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2016.
The current members of the board of trustees are (in alphabetical order):
The terms of Peter Baumgartner, Maria Paola Bonacina, Larry Paulson, and Brigitte Pientka expire. Larry Paulson and Brigitte Pientka have both served for two consecutive terms, and therefore cannot be nominated for a third term. Peter Baumgartner and Maria Paola Bonacina can be nominated for a second term.
The term of office of Ashish Tiwari as IJCAR 2016 program co-chair also ends; he is replaced by CADE-26 program chair Leonardo de Moura. As outgoing ex-officio trustee, Ashish Tiwari is eligible to be nominated as elected trustee.
In summary, we are seeking to elect four trustees.
Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at IJCAR 2016 in Coimbra. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be AAR members. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations are to be sent to Maria Paola Bonacina, CADE President (mariapaola (dot) bonacina (at) univr (dot) it), and Martin Giese, CADE Secretary (martingi (at) ifi (dot) uio (dot) no), up to the upcoming CADE business meeting.
Registration, accommodation, and travel information for IJCAR 2016 and all the affiliated events can be found at the conference website. The call for the Woody Bledsoe Student Travel Award is included below.
27 to 30 June 2016: IJCAR main conference
1 and 2 July 2016: Workshops
The Woody Bledsoe Student Travel Award was created to honour the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.
The winners of the IJCAR 2016 Woody Bledsoe Student Travel Award will be partially reimbursed (up to 750 EUR) for their conference registration, transportation, and accommodation expenses. Preference will be given to students who will play an active role in the conference (including satellite workshops, competitions, tutorials and poster events) and do not have alternative funding. However, also students in other situations are very much encouraged to apply.
A nomination consists of a recommendation letter of up to 300 words from the student's advisor. Nominations for IJCAR 2016 should be sent by e-mail to Conference Chair Pedro Quaresma at pedro@mat.uc.pt.
Nominations must arrive no later than 13 May 2016. The winners will be notified by 20 May 2016.
The awards will be presented at IJCAR 2016; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.
The awards are sponsored by CADE Inc.
The conference is aimed to serve as a forum for the effective exchange of novel results and the survey of works in the widely understood non-classical logics and their applications. Topics of either theoretical or applied interest include, but are not limited to: many-valued logics, modal logics, non-monotonic logics, paraconsistent logics, plausible reasoning, and substructural logics. Other fields of interest, related to cognitive science, computer science, formal ontology, foundations of mathematics, philosophy of language, and philosophy of mind are also welcome.
Participants are requested to submit extended abstracts of their talks of the length of 3 to 5 pages. The paper submission deadline is 30 May 2016. See the conference web site for details.
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress. Formal proceedings are produced only after the symposium so that authors can incorporate this feedback in the published papers.
Topics of interest cover all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large. Both full papers and extended abstracts describing applications in these areas are especially welcome. Contributions are welcome on all aspects of logic-based program development, including, but not limited to synthesis; transformation; specialization; composition; optimization; inversion; specification; analysis and verification; testing and certification; program and model manipulation; transformational techniques in SE; applications and tools.
The abstract submission deadline is 7 June 2016. See the conference web site for details.
FM 2016 is the latest in a series of symposia organized by Formal Methods Europe, an independent association that encourages the use of, and research on, formal methods for the engineering of computer-based systems and software. The symposia have been notably successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral work.
FM 2016 will highlight the development and application of formal methods in a wide range of domains including software, computer-based systems, systems-of-systems, human interaction, manufacturing, sustainability, power, transport, cities, healthcare, and biology. We also welcome papers on experiences of formal methods in industry, and on the design and validation of formal methods tools.
The abstract submission deadline is 16 May 2016. The full paper submission deadline is 30 May 2016. See the conference web site for details.
CPP is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. CPP 2017 is co-located with POPL 2017.
We welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interests to CPP:
Abstracts must be submitted by 5 October 2016. See the conference web site for details.
This workshop, affiliated with IJCAR 2016, is looking for positions statements of up to 500 words, which should be submitted by email by 1 June 2016. They should be in PDF format, and include your name, email address and affiliation, and a short paragraph describing your background or experience in machine proof. Please indicate whether you would be willing to have your statement posted online.
Position statements might address topics such as:
We do not plan to publish workshop proceedings, but will publish a report based on the discussions, co-authored by the participants. See the workshop web site for details.
Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete compared to NP-completeness of the decision problem of propositional logic (SAT). As the efforts of extending languages with quantifiers have not only been made for propositional logic in terms of QBFs, but in many other formalism like Constraint Satisfaction Problem (CSP) and Satisfiability Modulo Theories (SMT), QBF 2016 also targets researchers working in these related fields in order to exchange experiences and ideas.
The paper submission deadline is 8 May 2016 (with possible extension). See the workshop web site for details.
Human reasoning or the psychology of deduction is well researched in cognitive psychology and in cognitive science. There are a lot of findings which are based on experimental data about reasoning tasks, among others models for the selection task or the suppression task discussed by Byrne and others. Automated deduction, on the other hand, is mainly focusing on the automated proof search in logical calculi. Recently a coupling of the areas of cognitive science and automated reasoning is addressed in several approaches.
This workshop, co-located with IJCAI-16, intends to get an overview of existing approaches and make a step towards a cooperation between computational logic and cognitive science. See the workshop web site for details.
We are pleased to announce a workshop on Categorical Logic and Univalent Foundations, held at the University of Leeds preceeding the Logic Colloquium 2016. The workshop will be quite informal and include time for open discussions. Talks are invited concerning all aspects of homotopy type theory and univalent foundations, the scope of the workshop being very broad.
A limited amount of paid-for accomodation on campus is available for registrants. Preference will be given to participants who are also attending the Logic Colloquium 2016, graduate students, and recent graduates.
The deadline for registrations requesting accomodation support is 15 May 2016. The deadline for registration and abstract submission is 15 June 2016. See the workshop web site for details.
LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in: implicit computat= ional complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, b= ounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. The programme will consist of invited lectures as well as contributed talks selected by the Programme Committee.
The submission deadline is 17 June 2016. See the workshop web site for details.
The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends.
The scientific programme of the workshop will include presentations of recent results and ongoing research. The presentations will be selected by the Steering Committee on the basis of submitted abstracts according to originality, significance and general interest. The abstracts must be up to two pages long including references. If a longer version of the contribution is available, it can be made accessible on the web and referenced in the abstract.
The submission deadline for abstracts is 3 June 2016. See the workshop web site for details.
VeriFun is a reasoning system for verification of statements about programs written in a simple functional language. It was designed and developed as an easy to learn and easy to use system for teaching Automated Reasoning, Semantics, Verification and similar subjects and has been used in beginner courses about Formal Methods as well as in practical courses about Program Verification for about 15 years at the Technische Universität Darmstadt. VeriFun is implemented in Java and installers for running the new version 3.5 under Windows, Unix/Linux or Mac are now available for free download. This website also provides several case studies computed with the system.
Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR) continue to make rapid advances and find novel uses in a wide variety of applications, both in computer science and beyond. The SAT/SMT/AR Summer School aims to bring a select group of students up to speed quickly in this exciting research area. The school is the first SAT/SMT/AR Summer School, but continues the successful line of SAT/SMT Summer Schools, which have taken place annually since 2011.
The SAT/SMT/AR Summer School will take place in Lisbon, Portugal, in the week before the IJCAR conference in Coimbra (27 June to 2 July), which in turn is followed by the SAT conference in Bordeaux (5 to 8 July).
The extended application deadline is 15 May 2016. The programme and more information is available at summer school web site.
Our research laboratory, Mitsubishi Electric R&D Centre Europe in Rennes, France, has opened a permanent position of Formal Methods Research Engineer. We are looking for a young researcher knowing well one or more formal methods (and associated tools) to work on applying formal methods to industrial systems and software of Mitsubishi Electric group.
We are using various formalisms (Deductive Verification, Model Checking, Refinement, Abstract Interpretation, ...) applied to very diverse domains (Rail, Factory Automation, Automotive, ...). Mitsubishi Electric group has a lot of interesting cases to work on and where formal methods could make a real difference!
Our research is applied to concrete industrial case studies which have interesting research challenges. As we are part of corporate R&D, we have less constraints than business units and make publications and prototypes or participate to collaborative research projects like any academic research laboratory.
See the job announcement for details.
This is an announcement for several postdoctoral positions and a PhD grant at ENS de Lyon, France, in the area of verification and certification. These positions are funded by the ERC project CoVeCe.
This project covers fields such as automata theory, relation algebra, and proof assistants. Applicants should have a strong background in one of the above fields, and a desire to work at their frontier.
To apply, send an email to Damien Pous (Damien.Pous at ens-lyon.fr) with your motivations (which part(s) of the project you would like to be involved in, why...), a brief CV, and the names of two persons who could recommend you. Please feel free to engage a scientific discussion, or to ask him for more details about the project, the salaries, the surrounding team (Plume), the lab (LIP), or Lyon's city.
The project started on 1 April 2016 and should end in 2021. Successful applicants could start this spring, this autumn, or the following years.
We are seeking two outstanding postdocs (one theoretical, one more practical) with strong interests in the formal specification and verification of concurrent and distributed systems to join the Program Specification and Verification Group, led by Professor Philippa Gardner, at Imperial College London.
Two three-year positions will be funded as part of "REMS: Rigorous Engineering of Mainstream Systems", a 6-year EPSRC-funded programme grant for 5.6 million GBP between Cambridge, Edinburgh and Imperial, which finishes in 2019.
Please take a look at our Concurrency web page for more details and do not hesitate to contact Philippa if you are interested in one of these postdoc positions.
The University of Cambridge, led by Dr Mateja Jamnik, and the University of Brighton, led by Dr Gem Stapleton, are seeking to appoint two enthusiastic researchers, each for three years, to work collaboratively on the interdisciplinary Accessible Reasoning with Diagrams project funded by the Leverhulme Trust. In this project we want to devise and implement an accessible diagrammatic logic for modelling and reasoning in diverse domains.
Within the research unit Computation with Bounded Resources at the University of Innsbruck, Austria there is an opening for a 2 year position as postdoctoral researcher or a 3 year position as PhD student. The position is funded by the ANR-FWF project The fine structure of proof systems and their computational interpretations (FISP for short). The research unit is part of the Computational Logic Group of the Department of Computer Science.
The objective of FISP is to apply the powerful and promising techniques from structural proof theory to central problems in computer science for which they have not been used before, especially the understanding of the computational content of proofs, the extraction of programs from proofs and the logical control of refined computational operations. Its primary objective is to build new concrete computational interpretations of proof systems based on the techniques developed in the STRUCTURAL project (2011-2013).
A strong background in the themes of the FISP project is an asset. Candidates with a strong theoretical background in related areas are also encouraged to apply. Candidates for the postdoc position are required to hold a PhD degree; candidates for the PhD position must have a Master's or equivalent degree.
Candidates are expected to contribute to research within the project. Knowledge of German is not required. The annual gross salary is approximately EUR 50 200 for the postdoc position and EUR 28 600 for the PhD position.
Applications (including CV, publication list, and two references) may be sent by email, to the research unit leader Georg Moser no later than 31 May 2016. Informal inquiries are also welcome.
We are looking for a Ph.D. student or postdoctoral researcher to work on the analysis of randomized algorithms in the theorem prover Isabelle.
We shall be investigating programming logics for randomized algorithms, case studies, and the formalization of probability theory. We will build on the existing formalization of probability theory in Isabelle.
The successful candidate will have a strong background in verification or randomized algorithms and basic knowledge of the other area and will be keen to bridge the gap between them.
The position will be filled as soon as possible. Please send informal enquiries or formal applications (including the usual material and the names of two references) directly to Prof. Tobias Nipkow.
IRISA, the computer science laboratory of Rennes in France, seeks to hire an outstanding Ph.D. student to perform research in the field of formal modeling and analysis of security. The position is within the project entitled Attack-Defense Trees for Computer Security: Formal Modeling of Preventive and Reactive Countermeasures.
Attack-defense trees constitute a methodology to represent how an attacker may compromise a system and how a defender can protect it against potential attacks. The project's objective is to increase the expressive power of attack-defense trees by integrating reactive countermeasures into the formalism. A detailed description of the thesis topic is available online. For further inquiries please contact Dr. Barbara Kordy. See also the official job advert.
Our community has another tragic death to deplore: that of Helmut Veith, organizer of the highly successful Vienna Summer of Logic in 2014 (which included IJCAR 2014) and leading figure in logic and its applications to software engineering. The in memoriam above links to many testimonies and lists ways in which we can honor his memory.
Helmut's untimely departure is perhaps another reminder that we need to train a new generation of students to push automated reasoning further. Our community is in a strange situation: Although deduction is becoming increasingly relevant, with more and more tools based on automatic provers, model finders, or other logical engines as backends, our community is hardly growing; and we are still fighting just to keep existing projects alive, even the most successful ones.
In the past couple of years, quite a few large grants have been won for using proof assistants to formalize various aspects of programming (e.g., DeepSpec, RustBelt), but few to improve the automation of logic itself. A notable exception of which I am aware is Josef Urban's AI4REASON (Artificial Intelligence for Large-Scale Computer-Assisted Reasoning) ERC project, which aims at applying strong artificial intelligence techniques to automatic theorem proving.
One way to secure financing for automated reasoning is to connect it to security and privacy, which are timely topics. Another might be to ride the artificial intelligence wave. Thanks to an initiative by Christoph Benzmüller, the 2015 edition of CADE has been recognized as a sister conference of IJCAI (International Joint Conference on Artificial Intelligence), which means that a selection of the best CADE papers will be presented at IJCAI (along with hundreds of other papers from various tracks). This is good for the visibility of our field. There might also be lots of potential applications for our technology in the IJCAI community. Another positive sign for the integration of our field with artificial intelligence is the second edition of Bridging the Gap between Human and Automated Reasoning, this year as an IJCAI workshop.
Final exhortation: If you are an M.Sc. or Ph.D. student, or if you are supervising one, the deadline for the Woody Bledsoe Student Travel Awards for attending IJCAR 2016 and/or its workshops is 13 May 2016. So hurry up!