In earlier columns, typically you have been asked to use some automated reasoning program to prove a theorem or solve a puzzle. Indeed, often you were offered a set A of assumptions or axioms and asked to deduce some conclusion C from A. But what would you do if asked to show that some conclusion C does not follow from A—that is, that C is not provable from A? And, of course, you would be asked to do so with the aid of an automated reasoning program. Almost certainly, you would look for a model generator and use it to find an appropriate model.
Occasionally, some of the proofs you were asked to find involved constructing an object. Arguably, however, many proofs are not constructive.
Does this situation bring to mind a debate that has occurred in mathematics and in logic, a debate about which type of proof is acceptable? As a graduate student at the University of Chicago, I experienced such a debate, in which the idea of intuitionism came into play. Yes, the names Brouwer, Heyting, and Horn were most relevant in that debate. And those names and intuitionism are relevant, in fact central, to this column.
Heyting (a student of Brouwer) in 1930 was the first to provide an axiomatization of intuitionistic propositional calculus. Such a system is designed to allow only those theorems and rules that intuitionists find acceptable in proving (constructively) results in mathematics. In 1962, Horn provided a somewhat different axiomatization, a system I present shortly.
So, now, I will offer you challenges that address model finding and related challenges that address proof finding. I begin by giving you the following two formulas, where the function n denotes negation and the function i denotes implication, and where I rely on the clause language with - denoting negation and | denoting logical or.
(1) P(i(n(n(x)),x)).
(2) P(i(x,n(n(x)))).
Both formulas are theorems of classical logic, specifically classical propositional calculus, a logic that admits a single axiom. The first of the two, however, is not a theorem of intuitionistic logic, whereas the second is; the two together are sometimes called the law of double negation.
Your first challenge is to find a model that satisfies an axiom system (due to Horn and consisting of ten formulas that I shall give) that fails to satisfy the first of the two just-given formulas. Your next challenge is to prove from the system of ten formulas, expressed as clauses, the second of the two.
% 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
Specifically, you are asked to use condensed detachment, for which I supply a clause, and where the function i (as noted) denotes implication, and for the Horn axioms, n denotes negation, a denotes logical or, and k denotes logical and.
% condensed detachment
-P(i(x,y)) | -P(x) | P(y).
If the first of the formulas is adjoined to intuitionistic logic, you obtain classical propositional calculus.
Here is another example.
(3) P(i(i(n(x),x),x)).
(4) P(i(i(x,n(x)),n(x))).
Both (3) and (4) are theorems of classical logic. The first is not a theorem of intuitionistic logic, but the second is. So, as expected, you are offered two additional challenges. In the first challenge, you are asked to find a model of the given ten Horn axioms that does not satisfy (3). In the second challenge, you are asked to find a proof of (4) from the given 10-axiom system.
Some of you might be disappointed, classifying the four challenges each to be too easy to meet.
Therefore, I offer you two more theorems to prove, each of greater difficulty than what you have been offered earlier here.
(5) -P(i(k(n(p),n(b)),n(a(p,b)))) | $ANS(H442).
(6) -P(i(n(p),i(n(b),n(a(p,b))))) | $ANS(H443).
Since you know what the symbols denote, you can, therefore, understand the meaning of each.
For those of you who, as I do, find intuitionistic logic intriguing, note that I plan in a future column to offer more difficult theorems to prove in this context.
An election was held from 21 September to 26 October 2015 to fill two positions on the board of trustees of CADE, Inc. Christoph Benzmüller, Konstantin Korovin, Aart Middeldorp, and Philipp Rümmer were nominated.
Ballots were sent by electronic mail to all members of AAR on 21 September, for a total of 1084 ballots. 119 valid ballots were returned, which translates to a participation level of 11.0% (as compared to 10.0% in 2014, 11.8% in 2013, 13.0% in 2012, 16.2% in 2011, 13.3% in 2010, and 18.3% in 2009).
The counting of the votes according to the single transferrable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.
The two candidates elected are Christoph Benzmüller and Aart Middeldorp.
After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:
On behalf of the AAR and CADE Inc., I thank Renate Schmidt and Christoph Weidenbach for their service on the board during the last six years, and in particular Renate Schmidt for acting as vice-president of the board.
I further thank all candidates for running in the election, and all members who voted.
Congratulations to Christoph Benzmüller and Aart Middeldorp on being elected!
We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2017. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome.
The deadline for proposals is 8 December 2015.
In addition, we encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
Prospective organizers are encouraged to get in touch with the CADE secretary and president (at martingi (at) ifi.uio.no and mariapaola.bonacina (at) univr.it) for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.
The Vienna Center for Logic and Algorithms announces the 2015 edition of the VCLA International Student Awards and calls for the nomination of authors of outstanding scientific works in the field of Logic and Computer Science, in the following two categories:
In both categories, the work must make an original contribution to a research field that can be classified as part of Logic in Computer Science, understood broadly as the use of logic as a tool that enables computer programs to reason about the world. The main areas of interest are: Databases and Artificial Intelligence; Verification; Computational Logic.
The committee will select a winner for each category. The winners will be invited to Vienna to present their project and participate in a festive award ceremony. Additionally, the Outstanding Master Thesis Award category is accompanied by a prize of 1,200 EUR, and the Outstanding Undergraduate Research Award by a prize of 800 EUR.
The nomination deadline is 15 November 2015 (AoE). See the online call for further information.Applying formal methods may involve the usage of different formalisms and different analysis techniques to validate a system, either because individual components are most amenable to one formalism or technique, because one is interested in different properties of the system, or simply to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modeling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding both modeling and analysis. The conference covers all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.
Areas of interest include but are not limited to: Formal and semi-formal modelling notations; Integration of formal methods into software engineering practice; Hybrid systems; Program verification; Program synthesis; Model checking; Static analysis; Runtime analysis, monitoring, performance evaluation; Decision procedures, SAT and SMT solving; Software engineering; Component-based systems (compositional, embedded, distributed, etc.); Testing; and Abstraction and refinement.
iFM 2016 solicits high quality papers reporting research results and/or experience reports related to the overall theme of method integration. We solicit papers in the following categories: research papers (max. 15 pages); regular tool papers (max. 15 pages); short tool papers (max. 8 pages); and case study papers (max. 15 pages).
The abstract submission deadline is 21 December 2015. See the conference web site for details.
FSCD'16 is the first installment of the International Conference on Formal Structures for Computation and Deduction. FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, proof theory and new emerging models of computation such as quantum computing and homotopy type theory.
Suggested, but not exclusive, list of topics for submission are: Calculi; Methods in Computation and Deduction; Semantics; Algorithmic Analysis and Transformations of Formal Systems; Tools and Applications.
The abstract submission deadline is 29 January 2016. See the conference web site for details.
IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks.
IJCAR 2016 is a merger of leading events in automated reasoning:
IJCAR 2016 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited.
The abstract submission deadline is 18 January 2016. See the conference web site for details.
Workshop proposals on IJCAR-related topics are solicited. Proposals that promise to bring new topics into IJCAR, of either practical or theoretical importance, or provide a forum for more detailed discussion on central topics of continuing importance are highly welcome. Proposals that close the gap between automated reasoning and related areas, e.g., formal methods or software engineering, are especially encouraged.
The workshop proposal submission deadline is 15 November 2015. See the conference web site for details.
The fifth instalment of the conference Logic, Algebra and Truth Degrees (LATD) will take place in Phalaborwa, South Africa from 28 to 30 June 2016. The conference will be hosted by the Faculty of Science of the University of the Witwatersrand, Johannesburg, at the Hans Merensky Hotel, situated on the border of the world renowned Kruger National Park Game Reserve. Detailed travel information is available on the conference website.
Mathematical Fuzzy Logic is the sub-discipline of Mathematical Logic that is concerned with the notion of comparative truth. The assumption that "truth comes in degrees" has proved to be very useful in many theoretical and applied areas of Mathematics, Computer Science, and Philosophy. This conference series started as an official meeting of the working group on Mathematical Fuzzy Logic and has evolved into a wider meeting in algebraic logic and related areas. Its main goal is to foster collaboration between researchers in these areas, and to promote communication and cooperation with members of neighbouring fields. We encourage contributions on any relevant aspects of logical systems (including fuzzy, substructural, modal and quantum logics, and many-valued logics in general).
The featured topics include: proof theory and computational complexity; algebraic semantics and abstract algebraic logic; first, higher-order and modal formalisms; applications and foundational issues; geometric and game theoretic aspects.
Potential participants are encouraged to complete the expression of interest form on the conference's web site. The deadline for submissions is 24 February 2016.
The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability. The TAP conference aims to promote research in the intersection of testing and proving by bringing together researchers and practitioners from both areas of verification.
TAP 2016 is co-located with STAF 2016. It accepts regular-length research papers (16 LNCS pages + references), short papers (6 LNCS pages + references), and tool demonstration papers (8 LNCS pages + references). The abstract submission deadline is 29 January 2016. For details, see the submission instructions on the conference's web site.
CAV 2016 is the 28th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as biological systems and computer security. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer LNCS series. A selection of papers will be invited to a special issue of Formal Methods in System Design and the Journal of the ACM.
Submissions on a wide range of topics are sought, particularly ones that identify new research directions. CAV 2016 will follow a lightweight double-blind review process. Submissions that are not "blinded" will be rejected without review.
Submissions will be in two categories: Regular Papers and Tool Papers. The abstract submission deadline is 24 January 2016. See the conference web site for details.
Workshop proposals will be reviewed by the Workshop chair along with the program chairs and members of the steering committee. Proposals are due by 1 December 2015. by email to the Workshop chair. Organizers will be notified by 8 December 2015. See the conference web site for details.
The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Papers should be no more than 16 pages in length. In addition to regular papers, there will be a "rough diamond" section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract.
The abstract submission deadline is 29 February 2016. See the conference web site for details.
Researchers and practitioners are invited to submit proposals for co-located workshops on topics relating to interactive theorem proving. Workshops can target the ITP community in general, focus on a particular ITP system, or highlight more specific issues or recent developments. Proposals for in-depth tutorials or tool introductions are also welcome. The submission deadline is 12 December 2015. See the conference web site for details.
Rewriting is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application domains. It also has good properties as a metalogical framework for representing logics. Several successful languages based on rewriting (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of WRLA is to bring together researchers with a common interest in rewriting and its applications, and to give them the opportunity to present their recent work, discuss future research directions, and exchange ideas. The 2016 edition of WRLA, co-located with ETAPS, will mark its 20th anniversary since its first edition in Asilomar, California, in 1996.
The topics of the workshop include, but are not limited to: Foundations; Rewriting as a Logical and Semantic Framework; Rewriting Languages; Verification Techniques; and Applications. We solicit submissions of regular papers, tool papers, and work-in-progress papers.
The abstract submission deadline is 6 January 2016. See the workshop web page for details.
We are proud to present our book that has appeared with Cambridge University Press (CUP). See the book's web page for a more detailed description of the aims and the content of the book. CUP provides the book in a hardback version and as an eBook. Google Books (search: type+theory+formal+proof) gives an impression of the printed book text.
Applications are invited for a postdoctoral position in the Software Analysis Research Lab (SOARlab), School of Computing, University of Utah.
The position is primarily tied to two projects on verification of operating systems code, and in particular protocol stacks (e.g., Android Bluetooth stack) and concurrent Linux kernel modules (e.g., novel file systems). The projects involve developing novel symbolic verification techniques for low-level concurrent OS codes. An effort is already underway by our OS collaborators to develop an approach for decomposing parts of the Linux kernel into isolated modules, which we plan to leverage by performing composition verification. The ultimate goal is to release verified versions of real world OS components. We expect to rely on and extend our mature LLVM-based software verifier to achieve this.
See the SOARlab web site for details.
The KWARC group at Jacobs University Bremen is looking for Ph.D. candidates and PostDocs in multiple projects, e.g., Open Archive of Formalizations and OpenDreamKit. See the official posting for details.
Jacobs University Bremen is a private, English-speaking research university in Germany. The KWARC group conducts research on the representation and management of formal and informal knowledge in the STEM disciplines (Science, Technology, Engineering, and Mathematics).
Our interests cover the whole range from formal to informal knowledge and include logics and foundations of mathematics; formalizing/verifying knowledge; informal and semi-formal documents (specifications, papers, web pages, etc.); domain-specific applications (spreadsheets, CAD, etc.); and knowledge management (search, user interfaces, system integration, etc.).
We build systems that cover these diverse areas uniformly and integrate across domains, languagues, and tools, always combining logical correctness, wide-range applicability, and large-scale inter-operability.
Interested candidates can introduce themselves or ask for further information by email to Prof. Michael Kohlhase (m.kohlhase@jacobs-university.de). Applications (including the usual documents) should be directed to the same email address.
The Faculty of Computing and Information Sciences at Cornell University is looking to hire a post-doc for the CertiCoq project.
The goal of CertiCoq is to build a compiler for Coq within Coq, as an alternative to the "extraction" mechanism, and to verify the correctness of the compiler. There are many interesting things to explore, from advanced optimizations enabled by the linguistic structure of Gallina, to foundational questions about how to preserve dependent-types through compilation.
You can find out more about the project on the CertiCoq web site.
Just as the last year, this year the School of Mathematics at the Institute for Advanced Study in Princeton is looking for applications for memberships from people working in the Univalent Foundations as well as other areas of Type Theory, Constructive Mathematics and formalization of mathematics.
Applications can be submitted through MathJobs.
This year we will be specifically looking for one mid- or late career person to help Vladimir Voevodsky with the mentoring of the young members of the group. The salary for this position will be substantially higher than the standard membership salary.
Clark Barrett maintains a web site with opportunities in SAT, SMT, and related research areas.
119 valid ballots were returned. Therefore, in each iteration of the single transferrable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 60 first preference votes. Otherwise, the votes of the candidate with the least first preference votes are redistributed.
The following table reports the initial distribution of preferences among the candidates:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
| Christoph Benzmüller | 49 | 32 | 20 | 9 | 9 |
| Konstantin Korovin | 16 | 28 | 28 | 28 | 19 |
| Aart Middeldorp | 30 | 35 | 23 | 20 | 11 |
| Philipp Rümmer | 24 | 20 | 28 | 26 | 21 |
No candidate reaches at least 60 first preference votes.
By redistributing the votes of Konstantin Korovin, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Christoph Benzmüller | 56 | 38 | 16 | 9 |
| Aart Middeldorp | 33 | 48 | 27 | 11 |
| Philipp Rümmer | 30 | 22 | 46 | 21 |
No candidate reaches at least 60 first preference votes.
By redistributing the votes of Philipp Rümmer, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Christoph Benzmüller | 71 | 39 | 9 |
| Aart Middeldorp | 44 | 64 | 11 |
Now, Christoph Benzmüller reaches at least 60 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Christoph Benzmüller and get the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Konstantin Korovin | 30 | 38 | 32 | 19 |
| Aart Middeldorp | 55 | 29 | 24 | 11 |
| Philipp Rümmer | 34 | 36 | 28 | 21 |
No candidate reaches at least 60 first preference votes.
By redistributing the votes of Konstantin Korovin, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Aart Middeldorp | 70 | 38 | 11 |
| Philipp Rümmer | 46 | 52 | 21 |
Now, Aart Middeldorp reaches at least 60 first preference votes, and is elected.
To summarize, the 2 candidates elected are Christoph Benzmüller and Aart Middeldorp.
First, two important messages:
* * *
In the March 2015 installment of this newsletter, I briefly mentioned that the CoCon conference system would be used for TABLEAUX 2015 in Wrocław, Poland. CoCon's main innovation is that it does not leak information that should not be leaked. The non-leakage proof has been formalized in the Isabelle/HOL proof assistant. CoCon at TABLEAUX has turned out to be a success, and we are now evaluating it for ITP 2016, which will be held in Nancy, France.
CoCon is the latest manifestation of a strange connection between the automated reasoning community and conference management systems. That both EasyChair and CoCon are developed by researchers called Andrei (Voronkov, Popescu) is another coincidence which I cannot explain. The ConfiChair system, which encrypts the data on disk (or in the cloud), finally breaks the symmetry, and has the cleverest name of the three (except when I try to pronounce it–it invariably comes out as "confiture").
* * *
In the last installment of this newsletter, I asked the following question:
Does there exist a function f from reals to reals such that for all x and y, f(x + y * y) − f(x) >= y?
Let us assume that there exists such a function. We can then add
(A) for all X, Y, f(X + Y * Y) − f(X) >= Y
to our axiom set. Thanks to skolemization (let's drop the uppercase S), which takes care of the function f, the axiom conveniently falls within the expressive power of first-order logic. Now, this axiom does not seem to fall into any known safe fragment (e.g., primitively recursive functions on freely generated datatypes), so we assume the worst (or the best, depending on your point of view): that by cleverly choosing instantiations for X and Y, and invoking some basic arithmetic knowledge, we might be able to derive falsity.
First, we can assume without loss of generality that f(0) = 0. After all, we never observe f directly, only differences between two of its values. Now, let us assume that f(1) = 1. This is the smallest value possible, by (A) with X = 0 and Y = 1. Taking Y = 0.1, and carpeting the interval between 0 and 1, we get
f(0 + 0.01) − f(0) >= 0.1
f(0.01 + 0.01) − f(0.01) >= 0.1
⋅⋅⋅
f(0.98 + 0.01) − f(0.98) >= 0.1
f(0.99 + 0.01) − f(0.99) >= 0.1
By summing all terms on the left and all terms on the right, we end up with
f(1) − f(0) >= 10
contradicting our hypothesis that f(1) = 1 by one order of magnitude. A similar argument can be carried out for any other possible value of f(1). For example, if f(1) = 50, we can take Y = 0.01 and use a finer granularity for the carpeting. In general, one can take any Y < 1/f(1) such that m * Y = 1 for some natural number m.
As far as automating this goes, my impression is that we need to be able to infer such basic things as the invariance under translation and to perform efficient calculations on summations. Although (A) is first-order, the summation operator, with its bound variable, is higher-order, and hence beyond the scope of most current automatic theorem provers. I would be delighted to hear from anybody who has some ideas on how to attack this problem systematically. It appears to be related to telescoping and to amortized complexity analyses.