Association for Automated Reasoning

Newsletter No. 114
February 2016

From the AAR President, Larry Wos

In my column in the previous issue of the AAR Newsletter, the focus was on intuitionism. The names Heyting and Horn appeared there. Indeed, I offered you a 10-axiom system for intuitionism authored by Horn. But before Horn entered the picture, Heyting, in 1930, provided the first axiomatization of intuitionistic propositional calculus, a system consisting of eleven formulas. Such a system is designed to allow only those theorems and rules that intuitionists find acceptable in proving (constructively) results in mathematics. I present here, in negated form, the 11-axiom system Heyting offered.

(In OTTER, developed by W. McCune, the ANSWER literal is used to show you which theorems have been proved. You can ask OTTER to prove one theorem, or many theorems, in a single run.) In the following, the function i denotes implication, n denotes negation, a denotes logical or, and k denotes logical and. (As a reminder, and to have this column more independent, I note that constants such as b, c, and the like that occur in the Heyting formulas negated I give shortly are just that; in contrast, x, y, and the like that occur in the Horn clauses are variables implicitly meaning for all.) 

% Following eleven are Heyting's axioms in negated form; his fifth,
% seventh, and tenth, as noted, are Horn's first, fifth, and tenth, respectively.
-P(i(b,k(b,b))) | $ANS(01).
-P(i(k(b,c),k(c,b))) | $ANS(02).
-P(i(i(b,c),i(k(b,d),k(c,d)))) | $ANS(03).
-P(i(k(i(b,c),i(c,d)),i(b,d))) | $ANS(04).
-P(i(b,i(c,b))) | $ANS(05).
-P(i(k(b,i(b,c)),c)) | $ANS(06).
-P(i(b,a(b,c)))  $ANS(07).
-P(i(a(b,c),a(c,b))) | $ANS(08).
-P(i(k(i(b,d),i(c,d)),i(a(b,c),d))) | $ANS(09).
-P(i(n(b),i(b,c))) | $ANS(10).
-P(i(k(i(b,c),i(b,n(c))),n(b))) | $ANS(11).

If you wish to consider the challenges, you use condensed detachment with a clause I give below, with | denoting logical or and - denoting logical not. 

% condensed detachment
-P(i(x,y)) | -P(x) | P(y).

In 1962, Horn provided a somewhat different axiomatization, the following. 

% The following 10 clauses provide an axiomatization of intuitionistic
% logic taken from Horn's 1962 paper
P(i(x,i(y,x))).                       % 1
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).   % 2
P(i(k(x,y),x)).                       % 3
P(i(k(x,y),y)).                       % 4
P(i(i(x,y),i(i(x,z),i(x,k(y,z))))).   % 5
P(i(x,a(x,y))).                       % 6
P(i(x,a(y,x))).                       % 7
P(i(i(x,y),i(i(z,y),i(a(x,z),y)))).   % 8
P(i(i(x,n(y)),i(y,n(x)))).            % 9
P(i(n(x),i(x,y))).                    % 10

The first challenge is to find proofs of each of the eleven Heyting axioms from Horn's set of ten. As noted, Heyting's fifth, seventh, and tenth are respectively axioms 1, 6, and 10 of the Horn system used here and, therefore, do not need proving.

Now, if you have found the asked-for proofs, I offer as the next challenge a few additional theorems to prove, and these do present a substantial challenge. As before, I present the theorems in negated form, using numbers from my files. Of course, I assume you will not seek a shortcut, not browse in my other writings. Here are eleven, but that for HIF4 appears at least strange according to my years-ago notes and is perhaps easy to prove after all; I chose to offer these eleven because Heyting's system relies on eleven formulas. 

-P(i(n(p),i(n(b),n(a(p,b))))) | $ANS(H443).
-P(i(n(a(p,b)),k(n(p),n(b)))) | $ANS(H4441).
-P(i(k(n(p),n(b)),n(a(p,b)))) | $ANS(H4442).
-P(i(a(p,n(p)),i(n(n(p)),p))) | $ANS(H445).
-P(i(a(n(p),b),i(p,b))) | $ANS(H446).
-P(i(a(p,b),i(n(p),b))) | $ANS(H447).

% Following 5 are expanded theorems corresponding to iff theorems, if and only if.
-P(k(i(k(i(p,q),i(p,r)),i(p,k(q,r))),i(i(p,k(q,r)),k(i(p,q),i(p,r))))) | $ANS(HIF1).
-P(k(i(i(p,i(q,r)),i(k(p,q),r)),i(i(k(p,q),r),i(p,i(q,r))))) | $ANS(HIF2).
-P(k(i(i(p,i(q,r)),i(q,i(p,r))),i(i(q,i(p,r)),i(p,i(q,r))))) | $ANS(HIF3).
-P(k(i(a(k(p,q),r),k(a(p,r),a(q,r))),i(k(a(p,r),a(q,r)),a(k(p,q),r)))) | $ANS(HIF4).
-P(k(i(n(a(p,q)),k(n(p),n(q))),i(k(n(p),n(q)),n(a(p,q))))) | $ANS(HIF5).

My files (in which I made at least two lengthy studies of intuitionism) indicate that, depending on the approach, some of the just-given challenge problems will take a long time to solve.

Herbrand Award: Call for Nominations

Martin Giese
Secretary of AAR and CADE
On behalf of the CADE Inc. Board of Trustees

The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at IJCAR 2016 is

1 April 2016

Nominations pending from previous years must be resubmitted in order to be considered.

Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to

Maria Paola Bonacina, President of CADE Inc.
mariapaola.bonacina (at) univr.it

with copies to

Martin Giese, Secretary of CADE Inc. and AAR
martingi (at) ifi.uio.no

Ackermann Award: Call for Nominations

Anuj Dawar
President of the European Association for Computer Science Logic (EACSL)

Nominations are now invited for the 2016 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2014 and 31 December 2015 are eligible for nomination for the award. The deadline for submission is 15 April 2016. Submission details follow below. Nominations can be submitted from 1 January 2016 and should be sent to the chair of the Jury, Anuj Dawar, by e-mail.

The 2016 Ackermann award will be presented to the recipient(s) at the annual conference of the EACSL, 29 August to 2 September 2016, in Marseille (France). The award consists of

The jury is entitled to give the award to more (or less) than one dissertation in a year.

The jury consists of:

The candidate or his/her supervisor should submit

  1. the thesis (PS or PDF file);
  2. a detailed description (not longer than 20 pages) of the thesis in English (PS or PDF file);
  3. a supporting letter by the PhD advisor and two supporting letters by other senior researchers (in English); supporting letters can also be sent directly to Anuj Dawar (anuj.dawar@cl.cam.ac.uk);
  4. a short CV of the candidate;
  5. a copy of the document asserting that the thesis was accepted as a PhD thesis at a recognized University (or equivalent institution) and that the candidate has received his/her PhD within the specified period.

The submission should be sent by e-mail as attachments to the chairman of the jury, Anuj Dawar (anuj.dawar@cl.cam.ac.uk), with the following subject line and text:

Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text. Letters of support and documents can also be faxed to: Anuj Dawar, Ackermann Award, +44 1223 334678.

The Jury has the right to declare submissions to be out of scope or not to meet the requirements.

The Award is sponsored by the Kurt Gödel Society.

Church Award: Call for Nominations

An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see the ACM web site.

The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2016 award, the cut-off date is 1 January 1991. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Gödel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference.

Nominations for the 2016 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness.

Nominations are due by 1 March 2016 and should be submitted to Moshe Vardi.

The 2016 award will be presented at LICS, the flagship conference of SIGLOG. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared.

The 2016 Alonzo Church Award Committee consists of the following four members: Catuscia Palamidessi, Gordon Plotkin, Wolfgang Thomas, and Moshe Vardi (chair).

TABLEAUX Steering Committee Election: Call for Nominations

Jens Otten
President of, and on behalf of, the TABLEAUX Steering Committee

The Steering Committee of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (“TABLEAUX”) currently has three elected members whose terms will expire:

The Steering Committee is therefore calling for nominations of candidates who wish to contest an election for three positions, which will be held in February 2016.

To nominate please send an email to jeotten@cs.uni-potsdam.de containing:

Only members of the TABLEAUX community may act as nominators and a person may nominate or second only one candidate. Closing date for nominations is 20 February 2016.

The TABLEAUX community consists of all people who have been registered participants in at least one of the three most recent TABLEAUX Conferences including IJCAR (i.e. TABLEAUX 2013, IJCAR 2014 and TABLEAUX 2015) and all members of the current TABLEAUX Program Committee.

The current Steering Committee rules and more information can be found on the new TABLEAUX website.

Call for Bids to Host TABLEAUX 2017

Jens Otten
President of, and on behalf of, the TABLEAUX Steering Committee

The TABLEAUX Steering Committee is now calling for bids to host the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (“TABLEAUX”) in 2017. TABLEAUX typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years. Previous TABLEAUX/IJCAR conferences took place in Wrocław/Poland (TABLEAUX 2015), Vienna/Austria (IJCAR 2014), Nancy/France (TABLEAUX 2013), Manchester/UK (IJCAR 2012), Bern/Switzerland (TABLEAUX 2011), Edinburgh/UK (IJCAR 2010), and Oslo/Norway (TABLEAUX 2009).

A bid should cover at least the following aspects:

Bids that consider co-locating TABLEAUX with other conferences or workshops are in particular welcome. In 2013 and 2015 TABLEAUX was co-located with FroCoS (the International Symposium on Frontiers of Combining Systems).

The TABLEAUX tradition is that the leader or leaders of the winning bid will become the PC Chair or Co-Chairs for TABLEAUX 2017. The PC Chair or Co-chairs will create a PC in consultation with the TABLEAUX Steering Committee. The PC Chair or Co-Chairs will also be expected to edit the conference proceedings.

The bid should be submitted as PDF file to Jens Otten.

The deadline for submissions is 31 March 2016.

The TABLEAUX Steering Committee will decide which bid to accept and announce a decision as soon as possible after the deadline. Perspective organizers are encouraged to register their intention informally and to get in touch with the TABLEAUX Steering Committee for informal discussion.

More information about the TABLEAUX conference, its history and previous locations can be found on its web site.

Special Issue

Sci. Comput. Program.: Automated Verification of Critical Systems

Guest editors: Gudmund Grov and Andrew Ireland
Submission deadline: 20 May 2016
Notification: 31 August 2016

This special issue of Sci. Comput. Program. is devoted to the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), hosted in September 2015 by Heriot-Watt University in Edinburgh (UK). The aim of AVoCS is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. These topics are to be interpreted broadly and inclusively. It covers all aspects of automated verification, and typical (but not exclusive) topics of interest are: Model Checking; Automatic and Interactive Theorem Proving; SAT, SMT or Constraint Solving for Verification; Abstract Interpretation; Specification and Refinement; Requirements Capture and Analysis; Verification of Software and Hardware; Specification and Verification of Fault Tolerance and Resilience; Probabilistic and Real-Time Systems; Dependable Systems; Verified System Development; Industrial Applications.

Submission to this special issue is open. We expect original articles (typically 20-30 pages) that present high-quality contributions, have not been previously published in an archival venue and that must not be simultaneously submitted for publication elsewhere. Submissions must be written in English and comply with SCP's author guidelines. Submission is over the SCP website. When submitting your paper please choose the article type "Special issue: AVoCS 2015". Please send any queries you may have to Gudmund Grov.

Conferences

NFM 2016: NASA Formal Methods

7 to 9 June 2016, Minneapolis, Minnesota

The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and the aerospace industry requires advanced techniques that address their specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and the industry, with the goal of identifying challenges and providing solutions towards achieving assurance for such critical systems.

The focus of the symposium will be on formal techniques and other approaches for software assurance, their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.

The paper submission deadline is 19 February 2016. See the conference web site for details.

SAT 2016: Theory and Applications of Satisfiability Testing

5 to 8 July 2016, Bordeaux, France

The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. In addition to plain propositional satisfiability, it also includes Boolean optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning.

SAT 2016 aims to further advance the field by soliciting original theoretical and practical contributions in these areas with a clear connection to Satisfiability. Specifically, SAT 2016 invites scientific contributions addressing different aspects of SAT interpreted in a broad sense, including (but not restricted to) theoretical advances (such as exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, applications (including both novel application domains and improvements to existing approaches), as well as case studies and reports on findings based on rigorous experimentation.

The abstract submission deadline is 14 February 2016. See the conference web site for details.

RuleML 2016: Web Rule Symposium
Special Track: Rule- and Ontology-Based Data Access and Transformation

6 to 9 July 2016, Stony Brook, New York, USA

Ontologies and rule systems, isolated and in combination, have established themselves as viable approaches to a number of pressing IT problems: giving both humans and client software (e.g. data analysis) intuitive, domain-oriented, uniform access to data; integrating multiple data sets with heterogeneous schemas; migrating data from legacy systems, etc.

This track solicits contributions on theoretical and practical aspects of rule- and ontology-based data access and transformation. Topics of interest include, but are not limited to:

The abstract submission deadline is 11 March 2016. See the special track web page for details.

CICM 2016: Conference on Intelligent Computer Mathematics

25 to 29 July 2016, Białystok, Poland

Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas. CICM has been held annually as a joint meeting since 2008, co-locating related conferences and workshops to advance work in these subjects.

The principal tracks of the conference will be:

Like in previous years, project descriptions are welcomed as well.

We plan to have proceedings of the conference as in previous years with Springer Verlag as a volume in Lecture Notes in Artificial Intelligence (LNAI). The abstract submission deadline is 28 February 2016. See the conference web site for details.

CSL 2016: Computer Science Logic

29 August to 1 September 2016, Marseille, France

Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. CSL 2016 is the 25th EACSL annual conference, and will be organized by Aix-Marseille Université in Marseille, France.

Suggested topics of interest include (but are not limited to): automated deduction and interactive theorem proving, constructive mathematics and type theory, equational logic and term rewriting, automata and games, game semantics, modal and temporal logic, model checking, decision procedures, logical aspects of computational complexity, finite model theory, computational proof theory, bounded arithmetic and propositional proof complexity, logic programming and constraints, lambda calculus and combinatory logic, domain theory, categorical logic and topological semantics, database theory, specification, extraction and transformation of programs, logical aspects of quantum computing, logical foundations of programming paradigms, verification and program analysis, linear logic, higher-order logic, nonmonotonic reasoning.

Three affiliated workshops will be held as co-located events in the days following the conference:

The CSL 2016 conference proceedings will be published in Leibniz International Proceedings in Informatics (LIPIcs). Authors are invited to submit papers of no more than 15 pages in LIPIcs style (including references) presenting work not previously published, fitting the scope of the conference. Abstracts are due on 8 April 2016. See the conference web site for details.

AiML-2016: Advances in Modal Logic

29 August to 2 September 2016, Budapest, Hungary

Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained at http://www.aiml.net. AiML-2016 is the 11th conference in the series.

We invite submission on all aspects of modal logic, including: history of modal logic; philosophy of modal logic; applications of modal logic; computational aspects of modal logic; theoretical aspects of modal logic; specific instances and variations of modal logic. Papers on related subjects will also be considered.

There will be two types of submissions to AiML-2016: full papers for publication in the proceedings and presentation at the conference; short presentations intended for presentation at the conference but not for the published proceedings.

Both types of papers should be submitted electronically using the EasyChair submission page. We also ask authors of full papers to submit the abstract in plain text via EasyChair by 10 March 2016. See the conference web site for details.

ECAI 2016: European Conference on Artificial Intelligence

29 August to 2 September 2016, The Hague, the Netherlands

The biennial European Conference on Artificial Intelligence (ECAI) is Europe's premier venue for presenting scientific results in AI. Under the general theme of “AI for human values”, the 22nd edition of ECAI will be held in the city of The Hague, in sight the Peace Palace, seat of the International Court of Justice, a location highly appropriate to the conference theme. The conference dates are 29 August to 2 September 2016, with the workshops taking place on 29 and 30 August.

We invite the submission of papers for the technical programme of the 2016 European Conference on Artificial Intelligence (ECAI 2016). High-quality original submissions are welcome from all areas of Artificial Intelligence. ECAI 2016 welcomes contributions to a special topic: Artificial Intelligence for Human Values, addressing the ethical, legal, and societal impact of AI.

Submitted papers must be formatted according to the camera-ready style for ECAI'16, and submitted electronically in PDF format. Papers are allowed eight (8) pages, excluding references. Short papers, not exceeding two (2) pages, may be submitted for poster presentation and will be subjected to light review. Accepted short papers will not be published in the conference proceedings.

The paper submission deadline is 15 April 2016. See the conference web site for details.

PAIS 2016: Prestigious Applications of Intelligent Systems

31 August to 2 September 2016, The Hague, the Netherlands

The PAIS 2016 Programme Committee invites papers describing innovative applications of AI techniques to real-world systems and problems to be submitted to the Technical Programme of the 9th International Conference on Prestigious Applications of Intelligent Systems–a sub-conference of the 22nd European Conference on Artificial Intelligence (ECAI 2016).

Papers highlighting all aspects of the application of intelligent systems technology are most welcome. Our aim is to provide a forum for academic and industrial researchers and practitioners to share experience and insight on the applicability, development and deployment of intelligent systems. PAIS is the largest showcase of real applications using AI technology in Europe and is the ideal place to meet developers of successful applications.

Papers on all novel and significant applications of intelligent systems are welcome. In particular, we encourage submissions on deployed (in production use for some time) and emerging applications (in field testing). Papers considering deployed applications should clearly highlight the benefits of the application, describe how AI methods are applied or enhanced, and finally present the contribution of AI methods to the overall success.

The paper submission deadline is 15 April 2016. See the conference web site for details.

CP 2016: Principles and Practice of Constraint Programming

5 to 9 September 2016, Toulouse, France

The International Conference on Principles and Practice of Constraint Programming is the 22nd edition of the annual conference on all aspects of computing with constraints, including: theory, algorithms, environments, languages, models, systems, and applications such as decision making, resource allocation, scheduling, configuration, and planning.

The CP 2016 programme will include presentations of high quality scientific research papers and applications of constraints technology. A number of invited talks will also be presented that will describe important topics relevant to the field. As well as the usual workshop, tutorial and doctoral programmes, we will repeat the published paper track in which important results that have recently appeared in journals or sister conferences will be presented, the journal publication fast track for outstanding submissions, and the industry outreach programme.

To encourage authors and delegate to participate, the CP 2016 conference will features new tracks in addition to the technical track and the application track. Each track has a specific sub-committee to make sure that competent reviewers will review the papers submitted by people of these domains. We introduce also to this conference a challenge based on a realistic industrial grade optimization problem.

The abstract submission deadline is 13 April 2016. See the conference web site for details.

RV 2016: Runtime Verification

23 to 30 September 2016, Madrid, Spain

Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they are significantly more powerful and versatile than conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair.

Application areas of runtime verification include cyber-physical systems, safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.

All papers and tutorials will appear in the conference proceedings in an LNCS volume. Research Papers (regular and short), Tool Papers (regular and exhibition), and Tutorials are solicited. The abstract deadline is 8 May 2016. See the conference web site for details.

CADE-26 (2017) to Be Held in Gothenburg, Sweden

In the previous newsletter, we solicited proposals for the site of CADE-26 in 2017. The conference will be organized at TU Chalmers in Gothenburg (Göteborg), Sweden, with Moa Johansson and Magnus Myreen as conference chairs.

Workshops

Third Workshop on Automated Inductive Theorem Proving

23 and 24 March 2016, Vienna, Austria

Inductive theorem proving is a topic of growing interest in the automated reasoning community. This workshop aims to give researchers interested in the topic a chance to meet, exchange ideas and perhaps also try out some of the available theorem provers. We would like to invite talks featuring demos and tutorials of inductive theorem provers, challenging problems, new directions of research or anything else of interest to the inductive theorem proving community.

Participation will be free of charge but we ask you to register on our website. The registration deadline is 16 February 2016.

HCVS 2016: Horn Clauses for Verification and Synthesis, Participation

3 April 2016, Eindhoven, the Netherlands

Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses, and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses.

This workshop aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g. ICLP and CP) and Program Verification community (e.g. CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.

Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.

The early registration deadline is 1 March 2016. See the workshop web site for details.

LINEARITY '16

25 June 2016, Porto, Portugal

Ever since the birth of Girard's linear logic, there has been a stream of research in Computer Science where linearity is a key issue, covering both theoretical topics and applications, such as work on proof technology, complexity classes and more recently quantum computation, program analysis, expressive operational semantics, linear programming languages, and techniques for program transformation, update analysis and efficient implementation.

The aim of this workshop is to bring together researchers who are currently developing theory and applications of linear calculi, to foster their interaction and provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area.

New results that make central use of linearity, ranging from foundational work to applications in any field, are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: sub-linear logics; linear term calculi; linear type systems; linear proof-theory; linear programming languages; applications to concurrency; interaction-based systems; verification of linear systems; quantum models of computation; biological and chemical models of computation.

Authors are invited to submit an extended abstract (8 pages max) describing original ideas and recent results not published nor submitted elsewhere, or a 5-page abstract presenting relevant work that has been or will be published elsewhere, or work in progress. Preliminary proceedings will be available at the workshop. After the workshop, authors of the extended abstracts will be invited to submit a longer version of their work (typically a 15-pages paper) for publication in an electronic journal such as EPTCS. Papers should be submitted in PDF format using the EPTCS style files via EasyChair. The abstract submission deadline is 8 April 2016. See the workshop web site for details.

UNIF 2016: Unification

26 June 2016, Porto, Portugal

The 30th International Workshop on Unification is the 30th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.

The International Workshop on Unification (UNIF) is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory. The workshop will be hosted by the 1st International Conference on Formal Structures for Computation and Deduction (FSCD).

Following the tradition of UNIF, we call for submissions of abstracts (5 pages) in EasyChair style, to be submitted electronically as PDF files through the EasyChair submission site. The paper submission deadline is 1 May 2016. Based on the number and quality of submissions we will decide whether to organize a special journal issue. See the workshop web site for details.

IJCAR 2016: International Joint Conference on Automated Reasoning, Workshops

1 and 2 July 2016, Coimbra, Portugal

IJCAR is the premier international joint conference on all aspects of automated reasoning, including foundations, implementations, and applications, comprising several leading conferences and workshops. The following workshops are co-located with IJCAR 2016.

SMT 2016: Satisfiability Modulo Theories (1 and 2 July)

Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, test-vector generation, compiler optimization, scheduling, and other areas.

The aim of this workshop is to bring together researchers working on SMT and users of SMT techniques and tools. Relevant topics include but are not limited to: New decision procedures and new theories of interest; Combinations of decision procedures; Novel implementation techniques; Benchmarks and evaluation methodologies; Applications and case studies; Theoretical results.

GeTFun: Compositional Meaning in Logic (1 and 2 July)

The workshop GeTFun is dedicated to the study of various well-motivated ways in which the attractive properties and metaproperties of truth-functional logics may be stretched so as to cover more extensive logical grounds. The ubiquity of non-classical logics in the formalization of practical reasoning demands the formulation of more flexible theories of meaning and compositionality that allow for the establishment of coherent and inclusive bases for their understanding. Such investigations presuppose not only the development of adequate frameworks from the perspectives of Model Theory, Proof Theory and Universal Logic, but also the construction of solid bridges between the related approaches based on various generalizations of truth-functionality. Applications of broadly truth-functional logics, in their various guises, are envisaged in several areas of computer science, mathematics, philosophy and linguistics, where the ever increasing complexity of systems continuously raise new and difficult challenges to compositionality.

ARQNL: Automated Reasoning in Quantified Non-Classical Logics (1 July)

Non-classical logics—such as modal logics, conditional logics, intuitionistic logic, description logics, temporal logics, linear logic, dynamic logic, fuzzy logic, paraconsistent logic, relevance logic—have many applications in AI, Computer Science, Philosophy, Linguistics, and Mathematics. Hence, the automation of proof search in these logics is a crucial task.

For many propositional non-classical logics there exist proof calculi and automated theorem proving (ATP) systems. But proof search is significant more difficult than in classical logic. For first-order and higher-order non-classical logics the mechanization and automation of proof search is even more difficult. Furthermore, extending existing non-classical propositional calculi, proof techniques and implementations to quantified logics is often not straightforward. As a result, for most quantified non-classical logics there exist no or only few (efficient) ATP systems.

LRPP: Logics for Resources, Processes, and Programs (1 July)

The purpose of this workshop would be to discuss recent results on logics, including systems formulated in the style of Hoare and Hennessy-Milner, for modelling resources, processes, programs, and their interactions. We envisage a range of perspectives: proof-theoretic foundations, including decidability and complexity; semantic foundations (e.g., new resource semantics); specification of properties and behaviours; verification and analysis of programs and systems. It should help to establish and publicize a research agenda for such logics and their use in the development of trusted systems. The workshop is intended to provide a forum for discussion between researchers interested in logics of resources (from foundations to related calculi and applications) and researchers interested in languages and methods for specification of mobile, distributed, concurrent systems and their verification.

HaTT 2016: Hammers for Type Theories (1 July)

HaTT 2016 is the first workshop on Hammers for Type Theories and related tools, techniques, and experiments. Sledgehammer for Isabelle/HOL, HOLyHammer for HOL Light and HOL4, and other similar tools can have a huge impact on user productivity. These integrate automatic theorem provers (including SMT solvers) with proof assistants. However, users of proof assistants based on type theories, such as Agda, Coq, Lean, and Matita, currently miss out on this convenience. The HaTT workshop aims at gathering researchers working on these and other aspects of hammer-style automation for type theories, to exchange experiences and foster collaborations, to finally reach end users.

PAAR: Practical Aspects of Automated Reasoning (2 July)

PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brings together different groups toconcentrate on practical aspects of the implementation and application of automated reasoning tools. It allows researchers to present their work in progress, and to discuss new implementation techniques and applications.

The paper submission deadline is 2 May 2016. See the workshop web site for details.

UITP: User Interfaces for Theorem Provers (2 July)

The UITP workshop series brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulae.

3rd Vampire Workshop (2 July)

The workshop aims at discussing the development and use of the first-order theorem prover Vampire. The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas.

Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The developers can learn more about the use of Vampire, its efficiency in various application areas and needs of the users.

Social Aspects of Proofs (1 or 2 July)

No details are available yet.

ITP 2016: Interactive Theorem Proving, Workshops

25 to 27 August 2016, Nancy, France

ITP 2016 is the seventh conference on Interactive Theorem Proving and related issues, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The following workshops will be co-located with ITP 2016:

HOL Workshop 2016 (25 to 27 August)

This workshop is for anyone with an interest in the HOL theorem prover (HOL4) and its applications. This workshop continues the reboot of the HOL Workshop series, started at FLoC 2014.

The theme of the present workshop is “ProTips”. We invite both expert and novice users to share tips and tactics for building efficient, maintainable, and scalable formal developments. We are especially interested to hear from the authors of new or neglected features that could aid the engineering of large proofs. We also solicit opinions from experienced users on good proof style. A portion of the workshop will be dedicated to large examples, including CakeML, exhibiting uses or opportunities to use the protips above. We will also encourage discussion of, planning of, and hacking on improvements to HOL and its applications during the workshop.

Isabelle Workshop 2016 (25 and 26 August)

This informal workshop will bring together Isabelle users and developers. Participants are invited to present their research and projects, including applications of Isabelle, internal developments, add-on tools, and reports on work in progress. Isabelle workshops have been held at irregular intervals for more than a decade, usually associated with international conferences (e.g. CADE 2007, TPHOLs 2009, ITP 2012, and ITP 2014).

Coq Workshop 2016 (26 August)

The Coq Workshop brings together Coq users, developers, and contributors. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks. This series of events was started in 2009.

Mathematical Components, an Introduction (27 August)

Mathematical Components is the name of a Coq library covering a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to advanced results in various flavors of algebra. This library constitutes the infrastructure for the formal proofs of the Four Color Theorem and of the Odd Order Theorem. The aim of this tutorial is to present the ingredients used throughout this development, like the Ssreflect proof language or small scale reflection methods, and the basic libraries of general interest. The schedule will interleave small lectures by developers and advanced users of the library with supervised hands-on sessions. The intended audience is both people familiar with Coq but not with the Mathematical Components libraries and people with a background in proof assistants but not regular users of Coq.

LC 2016: Logic Colloquium

31 July to 6 August 2016, Leeds, UK

The Logic Colloquium 2016, organized under the auspices of the Association for Symbolic Logic, will be held at the University of Leeds (UK) from July 31 to August 6. There will be 12 plenary speakers, one of whom will give the Gödel Lecture.

The deadline for submission of abstracts for contributed papers is 29 April 2016. The deadline for student travel grant applications is 2 May 2016. See the colloquium web site for details.

STAIRS 2016: European Starting AI Researcher Symposium

29 and 30 August 2016, The Hague, the Netherlands

We invite students and young post-doctoral AI fellows to submit their work to the Eighth European Starting AI Researcher Symposium (STAIRS). STAIRS is an international meeting intended to support AI researchers, from all countries, at the beginning of their career: PhD students or people holding a PhD for less than one year. STAIRS 2016 will be co-located with ECAI 2016, the European Conference on AI, in The Hague, the Netherlands, from 26 August to 2 September 2016.

STAIRS offers doctoral students and young post-doctoral AI researchers:

Papers are welcome on all aspects of contemporary AI. The paper submission deadline is 16 May 2016. The proceedings of STAIRS will be published and distributed by IOS Press' Frontiers in Artificial Intelligence and Applications (FAIA) series. See the symposium web site for more information.

FMICS-AVoCS 2016: Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems

26 to 29 September 2016, Pisa, Italy

The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. The aim of the AVoCS workshop series is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. In 2016, FMICS and AVoCS join their forces to hold a workshop combining their themes on Formal Methods and Automated Verification. For FMICS, this will be the 21st, for AVoCS the 16th edition.

FMICS-AVoCS 2016 aims to bring together scientists and engineers that are active in the area of formal methods, develop tools and techniques for the automated verification of critical systems, and are interested in exchanging their experiences in the industrial usage of these methods and tools.

Topics of interest include (but are not limited to): Design, specification, refinement, code generation and testing of critical systems based on formal methods; Methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of critical systems, in particular distributed, real-time systems and embedded systems; Automated verification (model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, etc.) of critical systems; Verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues); Tools for the development of formal design descriptions; Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions; Impact of the adoption of formal methods on the development process and associated costs; Application of formal methods in standardization and industrial forums.

Submissions should not exceed 15 pages formatted according to the LNCS style (Springer), and should be submitted as Portable Document Format (PDF) files using the EasyChair submission site. The abstract submission deadline is 18 April 2016. See the workshop web site for details.

Summer Schools

SAT/SMT/AR Summer School 2016

22 to 25 June 2016, Lisbon, Portugal

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 programme and more information will be added soon to the summer school web site.

ESSLLI 2016: European Summer School in Logic, Language and Information

15 to 26 August 2016, Bolzano, Italy

The 28th European Summer School in Logic, Language and Information (ESSLLI 2016) takes place at the Free University of Bozen-Bolzano, Bolzano, Italy, from August 15 to 26, 2016. It is organized with the support of the University of Trento under the auspices of FoLLI, the European Association for Logic, Language and Information.

The scientific program of ESSLLI 2016 consists of 45 courses, the Student Session, 3 workshops, 4 evening lecturers and a talk by the Beth Dissertation Prize winner. Moreover, the school features 3 satellite events. See the summer school web site for details.

Open Positions

Three post-doctoral positions at the Software Languages Lab in Brussels, Belgium

The Software Languages Lab of the Vrije Universiteit Brussel is welcoming applications for 3 vacant positions for post-doctoral researchers with respective expertise in formal aspects of programming languages, software analysis and tooling, or reactivity and event-based systems.

Our group is located on a green campus in the de facto capital of Europe. It is headed by professors Viviane Jonckers, Wolfgang De Meuter, Elisa Gonzalez Boix, and Coen De Roover. As we host researchers of various nationalities, our working language is English.

See the positions' web page for details.

PhD and Post-doc Positions in Programming Methodology at ETH Zürich, Switzerland

The Chair of Programming Methodology at ETH Zurich is recruiting PhD students and post-docs for several projects on program verification, static program analysis, and testing. An overview of our current projects is available on our research page, but we are always interested in exploring new directions.

Key requirements for successful applications:

Applications and questions should be sent to Mrs. Marlies Weissert. The application should include a CV and a description of research interests. We will consider applications until the positions are filled. The start date is negotiable.

PhD Positions in Information Security at ETH Zürich, Switzerland

The Institute of Information Security headed by Prof. David Basin at ETH Zurich has multiple open positions for PhD students on research projects in the area of formal methods for information security.

We are looking for enthusiastic outstanding Computer Science or Mathematics students with a strong background in at least two of the following topics:

Additionally, experience in the following specialized areas would be advantageous:

ETH Zurich regulations require PhD students to hold a Masters or equivalent degree (e.g., Diplom). All candidates matching the profile above are encouraged to apply as soon as possible. We will process applications until all positions are filled. Successful candidates are expected to start soon after acceptance, but the starting date is negotiable.

Please contact Sasa Radomirovic for details.

Post-doctoral Positions at University of California, San Diego, USA

The UCSD Theoretical Computer Science group is looking for strong applicants for post-doctoral positions. Research topics include, but are not limited to: algorithm design, computational complexity, cryptography, proof complexity and coding theory. The positions are for one academic year, with a start date of October 2016. After the first year, it may be possible to continue the post-doctoral positions for a 2nd year, contingent on approval by the theory faculty and on available funding.

The application deadline is 1 March 2016. See the application website for details.

Three PhD and Two Post-doc Positions on Programming Languages and Verification in London, UK

Alexandra Silva has three PhD and two post-doc positions available in London. These are funded by the department and also by her ERC starting grant project. The group where she is now—Programming Principles, Logic And Verification—has people doing research that spans both theory and practice, including logic, programming language design, program verification, and theorem proving. They have great connections with industry (Amazon, Facebook, Google) and with other groups at UCL, including Systems and Networks, Information Security, and Software Systems Engineering.

From the three PhD positions, two are already advertised online (first advert, second advert). The post-doc positions are not yet advertised but suitable candidates can contact Alexandra Silva directly.

Positions for Students and Young Researchers at Inria Paris, France

The Prosecco research team at Inria Paris is looking for excellent, highly motivated students and young researchers for research internships and PhD, PostDoc, Research Engineer, or Researcher positions. We have external funding for a couple of PhD and PostDoc positions we can fill over several years with significant flexibility and can also support strong candidates for Researcher positions funded and awarded competitively by Inria.

Prosecco does formal and practical security research on cryptographic protocols, web security, and hardware security mechanisms. To this end, we design and implement programming languages, formal verification tools, dynamic monitors, testing frameworks, verified compilers, etc. Our current projects include:

If you are interested in applying or have any questions please send us an email at Karthikeyan Bhargavan and Catalin Hritcu.

Postdocs, PhDs, and Visitors on Deep Specification at Princeton, Penn, Yale, and MIT, USA

Andrew W. Appel
Princeton University, USA

The U.S. National Science Foundation has just announced this year's three Expeditions in Computing, their major, high-profile, “flagship” grants; including:

The Science of Deep Specification
Andrew W. Appel, Adam Chlipala, Benjamin Pierce, Zhong Shao, Stephanie Weirich, Steve Zdancewic
(Princeton, Penn, Yale, MIT)

This 5-year “Expedition” will focus on specification and verification of software and hardware in Coq. We invite you to browse the DeepSpec web site to learn more of our plans.

We invite participation from the community of researchers interested in software specification and functional-correctness verification, both in the U.S. and around the world, both in academia and industry. We will be looking for postdocs and PhD students, and visitors.

Postdoc and PhD Positions on Foundations for Rust in Saarbrücken, Germany

Derek Dreyer
Max Planck Institute for Software Systems, Saarbrücken, Germany

I am very pleased to announce that I have been awarded a 2015 ERC Consolidator Grant for the project "RustBelt: Logical Foundations for the Future of Safe Systems Programming". This 5-year project concerns the development of rigorous formal foundations for the Rust programming language.

I am seeking exceptional candidates to fill several postdoc and PhD positions. Please see the project web page for more details, and do not hesitate to contact me if you are interested in joining the RustBelt team!

See the project web page for details.

Postdoc Positions on Security Protocol and Hardware Verification at NTU Singapore

One postdoc position is available at the School of Computer Engineering, Nanyang Technological University (NTU) Singapore, for a project on verification of security protocols. A particular emphasis will be on designing and implementing decision procedures for finding attacks on protocols or producing formal proofs of their security. We will be using a mixture of process algebraic and logical frameworks to express protocols and their properties, in particular, equivalence properties of security protocols.

In addition, one postdoc position is available at the School of Computer Engineering, Nanyang Technological University (NTU) Singapore, for a project on hardware verification.

Candidates must possess a PhD degree in Computer Science or related areas. Candidates with strong backgrounds in process calculus, such as the pi-calculus and its variants, and/or formal logic and theorem proving are preferred. The salary range is between SGD 4000–6000 per month. The position will be initially offered for one year, but can be extended up to three years, subject to satisfactory performance and availability of funding.

To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu. Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 February 2016. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in April 2016.

Faculty Positions in Programming Languages and Computational Logic at CMU in Qatar

Carnegie Mellon University in Qatar invites applications for two teaching-track positions at any level, one in the fields of robotics and artificial intelligence (position CMUQ-CS15-003), and the other in the fields of programming languages and computational logic (position CMUQ-CS15-004). This is a career-oriented renewable appointment that involves teaching high-achieving international undergraduate students. Candidates must have a Ph.D. in Computer Science or related field, substantial exposure to Western-style education, good leadership skills, an outstanding teaching record, and excellent research accomplishments. As Carnegie Mellon University takes pride in its diverse faculty and student population, the successful applicant shall demonstrate experience and effectiveness in teaching, mentoring and inspiring female undergraduates. Applications by female candidates are especially encouraged.

The position offers a competitive salary and benefits including a foreign service premium, excellent international health care coverage, and allowances for housing, transportation, dependent schooling, and travel. Further information can be found in the job advert.

Funded Doctoral Positions in Computer Science in Austria

TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program LogiCS. The LogiCS doctoral college focuses on interdisciplinary research topics covering (i) computational logic, and applications of logic to (ii) databases and artificial intelligence as well as to (iii) computer-aided verification.

LogiCS is a doctoral college focusing on logic and its applications in computer science. Successful applicants will work with and be supervised by leading researchers in the fields of computational logic, databases and knowledge representation, and computer-aided verification. The LogiCS faculty comprises 15 renowned researchers with strong records in research, teaching and advising, complemented by 12 associated members who further strengthen the research and teaching activities of the college.

We are looking for 1 doctoral students per faculty member, where 30% of the positions are reserved for highly qualified female candidates. The doctoral positions are funded for a period of 3 years according to the funding scheme of the Austrian Science Fund. The funding can be extended for one additional year contingent on a placement at one of our international partner institutions.

At the moment we are particularly looking for people in the following areas: Automated reasoning and symbolic computation; Formal Verification of hybrid systems; Model Checking.

Detailed information about the application process is available on the LogiCS web page. The applicants are expected to have completed an excellent diploma or master's degree in computer science, mathematics, or a related field. Candidates with comparable achievements will be considered on a case-by-case basis. The next application deadline is 1 March 2016.

Researcher in Verification of Embedded Systems at Oxford, UK

Department of Computer Science, Wolfson Building, Parks Road, Oxford
Researcher in Verification of Embedded Systems
Fixed term for up to 1 year
Grade 7: £30,738–£37,768 p.a.

The department has a new opening for a full-time Researcher in Verification of Embedded Systems, fixed-term for up to 1 year. Reporting to Professor Daniel Kroening and Dr Martin Brain, you will be a member of the Systems Verification research group.

The primary selection criteria are a doctoral degree (or very close to completion) in a relevant area of Computer Science or a related discipline together with a strong background in either the theory or the practical application of formal verification or program analysis. Experience with program analysers, verification tools such as Model Checkers and a prior background in verification for embedded systems (such as avionics or automotive) are highly desirable.

The post, which is a full-time appointment is funded by ERC, is available for up to 1 year, and has a salary on the University grade 07S scale (currently £30,738–£37,768 p.a.) This includes membership of the Universities Superannuation Scheme (USS) and has an annual leave entitlement of 38 days per year (inclusive of all public holidays and university closed periods).

The closing date for applications is 12 noon on 7 March 2016. See the job advert for details.

The Editor's Corner

In newsletter #112, I presented a small puzzle:

Does there exist a function f from reals to reals such that for all x and y, f(x + y * y) − f(x) >= y?

The solution followed in newsletter #113. It turns out there is no better way to precipitate response than to offer an overly complex solution.

My first correspondent, John Harrison, wrote:

The proof I came up with ultimately amounts to the same thing as yours but for my money is a bit cleaner and more explicit, just using induction rather than manipulating sums.

[1] f(x + y^2) - f(x) >= y for any x and y (given)

[2] f(x + n y^2) - f(x) >= n y for any x, y and natural number n
(by an easy induction using [1] for the step case)

[3] f(1) - f(0) >= m + 1 for any natural number m
(set n = (m + 1)^2, x = 0, y = 1/(m + 1) in [2])

[4] Contradiction of [3] and the Archimedean property of the reals.

It is not clear whether it would be easy to automate this, but a priori it doesn't seem fanciful that a Boyer-Moore style inductive theorem prover could find it. I suspect something like induction and the Archimedean property are essential but I haven't actually tried to find a counterexample in a non-Archimedean field.

…

P.S. Of course I could not resist doing it manually in HOL Light anyway.

let lemma = prove
(`!f:real->real. ~(!x y. f(x + y * y) - f(x) >= y)`,
 REWRITE_TAC[real_ge] THEN REPEAT STRIP_TAC THEN
 SUBGOAL_THEN `!n x y. &n * y <= f(x + &n * y * y) - f(x)` MP_TAC THENL
  [MATCH_MP_TAC num_INDUCTION THEN SIMP_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
   REWRITE_TAC[REAL_SUB_REFL; REAL_LE_REFL; GSYM REAL_OF_NUM_SUC] THEN
   GEN_TAC THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
   FIRST_X_ASSUM(MP_TAC o SPECL [`x + &n * y * y`; `y:real`]) THEN
   SIMP_TAC[REAL_ADD_ASSOC; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN 
   REAL_ARITH_TAC;
   X_CHOOSE_TAC `m:num` (SPEC `f(&1) - f(&0):real` REAL_ARCH_SIMPLE) THEN
   DISCH_THEN(MP_TAC o SPECL [`SUC m EXP 2`; `&0`; `inv(&(SUC m))`]) THEN
   REWRITE_TAC[REAL_ADD_LID; GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_POW] THEN 
   REWRITE_TAC[REAL_FIELD `(&m + &1) pow 2 * inv(&m + &1) = &m + &1`;
     REAL_FIELD `(&m + &1) pow 2 * inv(&m + &1) * inv(&m + &1) = &1`] THEN
   ASM_REAL_ARITH_TAC]);;

And I could not resist doing it in Isabelle/HOL, by following John's plain-text description, and invoking Sledgehammer on the proof obligations. The two nontrivial sequences of then have and then show in the proof below were generated by automatic theorem provers (and translated back to Isabelle):

The strongest prover was undoubtedly CVC4, but we cannot yet parse its proof output. For the above, it was E that made the difference.

My second correspondent, Viktor Kuncak, provided an informal argument and quite some insights about how to go about automating such things. He remarked:

While I have seen them in puzzles, I have very few practical applications of them. Do you? I rarely find such strong quantified statements about otherwise unknown functions. In fact, I never encounter such functions. Oh, wait, they don't exist…

Ha!

Perhaps one speculative conclusion: I think reasoning about complex problems with unknown functions is most likely to look more like program analysis than resolution-based theorem proving…

Indeed, most of the higher-order problems I run across tend to be rather pedestrian in comparison with the puzzle. Dear reader: Is this also your experience?