Do you have in hand a program that proves theorems? Would you like to have access to a set of problems, focusing on geometry, that are graduated in difficulty and that might, if considered, lead you to the formulation of a new strategy? This column offers just such a set of problems.
Yes, the problems you find here focus on plane geometry, an area of mathematics you most likely first studied in high school. But plane geometry is hardly “simple”. I note, for example, that the eminent logician Alfred Tarski took an interest in geometry and worked on it for many years. Among his accomplishments in the area was a 13-axiom system that enables a person, or a program if sufficiently powerful, to prove a large number of theorems. Points were all he needed: just the notions of betweenness, denoted by T, and equidistant, denoted by E.
For Tarski, betweenness does not mean for points x, y, and z that y is necessarily strictly between x and z; in fact, for him, T(x,y,z) admits that x and y and z are all the same point. When I encountered this axiom system, I found it most surprising that just betweenness and equidistance sufficed.
The following axioms provide the basis of any study you might undertake.
identity axiom for betweenness:
-T(x,y,x) | (x = y).
transitivity axiom of betweenness:
-T(x,y,u) | -T(y,z,u) | T(x,y,z).
connectivity axiom for betweenness:
-T(x,y,z) | -T(x,y,u) | (x = y) | T(x,z,u) | T(x,u,z).
reflexivity axiom for equidistance:
E(x,y,y,x).
identity axiom for equidistance:
-E(x,y,z,z) | (x = y).
transitivity axiom for equidistance:
-E(x,y,z,u) | -E(x,y,v,w) | E(z,u,v,w).
Outer Pasch's axiom (2 clauses):
-T(x,v,u) | -T(y,u,z) | T(x,f1(v,x,y,z,u),y).
-T(x,v,u) | -T(y,u,z) | T(z,v,f1(v,x,y,z,u)).
Euclid's axiom (three clauses):
-T(x,u,v) | -T(y,u,z) | (x = u) | T(x,z,f2(v,x,y,z,u)).
-T(x,u,v) | -T(y,u,z) | (x = u) | T(x,y,f3(v,x,y,z,u)).
-T(x,u,v) | -T(y,u,z) | (x = u) | T(f2(v6,x,y,z,u),v6,f3(v6,x,y,z,u)).
five-segment axiom:
-E(x1,y1,x2,y2) | -E(y1,z1,y2,z2) | -E(x1,u1,x2,u2) | -E(y1,u1,y2,u2) | -T(x1,y1,z1) | -T(x2,y2,z2) |
(x1 = y1) | E(z1,u1,z2,u2).
axiom of segment construction (two clauses):
T(x,y,f4(x,y,u,v)).
E(y,f4(x,y,u,v),u,v).
lower dimension axiom (three clauses):
-T(c1,c2,c3).
-T(c2,c3,c1).
-T(c3,c1,c2).
upper dimension axiom:
-E(x,u,x,v) | -E(y,u,y,v) | -E(z,u,z,v) | (u = v) | T(x,y,z) | T(y,z,x) | T(z,x,y).
weakened continuity axiom (two clauses):
-E(u1,x1,u1,x2) | -E(u1,z1,u1,z2) | -T(u1,x1,z1) | -T(x1,y1,z1) | E(u1,y1,u1,f5(x1,y1,z1,x2,z2,u1)).
-E(u1,x1,u1,x2) | -E(u1,z1,u1,z2) | -T(u1,x1,z1) | -T(x1,y1,z1) | T(x2,f5(x1,y1,z1,x2,z2,u1),z2).
I strongly conjecture that, in the following set of theorems, your program will find the first few perhaps easy to prove. I believe, however, that the set will tax your program after the first few successes.
E(x,y,x,y). % Satz 2.1, CHZ1
-E(xa,xb,xc,xd) | E(xc,xd,xa,xb). % Satz 2.2, CHZ2
-E(xa,xb,xc,xd) | -E(xc,xd,xe,xf) | E(xa,xb,xe,xf). % Satz 2.3, CHZ3
-E(xa,xb,xc,xd) | E(xb,xa,xc,xd). % Satz 2.4, CHZ4
-E(xa,xb,xc,xd) | E(xa,xb,xd,xc). % Satz 2.5, CHZ5
E(x,x,y,y). % Satz 2.8, CHZ8
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1). % Satz 2.11, CHZ11
xq = xa | -T(xq,xa,u) | -E(xa,u,xc,xd) | f4(xq,xa,xc,xd) = u. % Satz 2.12, CHZ12
-E(u,v,x,x) | u=v. % Not one of Szmielew's theorems but we proved it, CHZZ
-T(xa,xb,xc) | T(xc,xb,xa). % Satz 3.2., CH4
T(x,y,y). % Satz 3.1, CH3
T(xa,xa,xb). % Satz 3.3, CH2
-T(xa,xb,xc) | -T(xb,xa,xc) | xa = xb. % Satz 3.4, CHZ34
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xb,xc). % Satz 3.51, CHZ351
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xc,xd). % Satz 3.52, CHZ352
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xb,xc,xd). % Satz 3.61, CHZ361
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd). % Satz 3.61a, CHZ361a
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xc,xd). % Satz 3.71, CHZ71
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd). % Satz 3.62, CHZ362
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xb,xd). % Satz 3.72, CH72
The goal is to prove all 20 theorems. A systematic approach that merits study and that offers an interesting challenge consists of proving a theorem, adjoining that theorem for the next experiment, and then seeking another proof. The results of this iterative approach might shed light on the power of your program.
As you probably have surmised, I have used OTTER to prove all 20 theorems; but I relied on a wide variety of approaches, only one of which was the cited iterative approach. If your program is able to prove all the theorems with this approach or any approach, I would enjoy hearing from you about your success.
I am happy to announce that Andrei Voronkov will be awarded the Herbrand Award at CADE 2015, in recognition of his numerous theoretical and practical contributions to automated deduction, and the development of the award-winning Vampire theorem prover.
The Skolem Award was instituted to reward a CADE paper that has passed the test of time by being most influential in the field.
The Skolem award committee for CADE-25 consisted of Alessandro Armando, Gilles Barthe, Claude Kirchner (chair), Christopher Lynch, Leonardo de Moura, Ulrike Sattler, Geoff Sutcliffe, Toby Walsh, and Christoph Weidenbach.
According to this committee's recommendation, the following papers receive Skolem Awards in 2015:
It is a pleasure to report that the IJCAR Steering Committee appointed Nicola Olivetti and Ashish Tiwari as PC Co-Chairs of IJCAR 2016. Both join the IJCAR Steering Committee, and Ashish also joins the CADE Board as ex officio trustee.
Nominations for two CADE trustee positions are being sought, in preparation for the elections to be held after CADE-25.
The current members of the board of trustees are (in alphabetical order):
The terms of Renate Schmidt and Christoph Weidenbach expire. Both have served for two terms, and therefore cannot be nominated for a third term.
The term of office of Amy Felty as CADE-25 program co-chair also ends. As outgoing ex-officio trustee, she is eligible to be nominated as elected trustee.
In summary, we are seeking to elect two trustees.
Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at CADE-25 in Berlin. 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) de), up to the upcoming CADE business meeting.
As requested by the participants of the RTA-TLCA conference in Vienna 2014, the united Steering Committees of Rewriting Techniques and Applications (RTA) and Typed Lambda Calculi and Applications (TLCA) have prepared a proposal to replace our existing two conferences by a new one of a broader scope.
As we embark on this exciting journey, we invite all members of the computer science community to provide comments, remarks, and suggestions for the new conference. All input will be passed on to the steering committee of the new conference after its constitutional general meeting on 1 July 2015.
It is our thesis that formal elegance is
a prerequisite to efficient implementation.
-- Gérard Huet[4]
We, the communities behind the RTA[1] and TLCA[2] conferences, believe
that our field has evolved and developed richer connections with many
both practical and theoretical aspects of computer science and logic
research since the inception of RTA in 1983 and TLCA in 1993. In
particular, the scope of the two original conferences widened to
include a significant overlap, and in fact the conferences have
already collaborated by having most of our meetings since 2003 as the
joint RDP[3] conference.
We have therefore decided to propose a new conference,
Formal Structures for Computation and Deduction (FSCD)
which not only combines our scope but further extends it to cover all
the inter-related formal areas that researchers in formal structures
for computation and deduction engage in.
The name of the new conference comes from an unpublished but important
book by Gérard Huet[4] that was a strong influence on many researchers
in our area. We are grateful to Gérard for allowing us to reuse the
name.
The extended scope of the conference will include all research related
to formal structures for computation and deduction, in particular all
areas/categories included in the attached non-exhaustive list of
topics.
We look very much forward to serve the scientific community with this
new conference, which inherits as well as updates and modernizes the
scope of the conferences it replaces.
References.
[1]http://rewriting.loria.fr/rta/
[2]http://www.mimuw.edu.pl/tlca/
[3]http://users.dsic.upv.es/~rdp03/
[4]http://pauillac.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz
FSCD initial non-exhaustive list of topics (intended to extend the
current RTA and TLCA scope, and expected to evolve over time):
1. Calculi
a. Lambda-calculus
b. Rewriting formats (string, term, higher-order, graph, conditional, ...)
c. Proof theory (natural deduction, sequent calculi, proof nets, ...)
d. Strategies in computation and deduction
2. Type Theory and Logical Frameworks
a. Type systems (recursive, intersection types, polymorphism, ...)
b. Dependent types and homotopy type theory
c. Linear logic and other constructive logics
d. Implicit complexity
3. Fundamentals of Functional and Declarative Programming
a. Unification and narrowing
b. Tree automata
c. Continuations and control operators
d. Coinduction and infinitary systems
4. Semantics
a. Abstract machines
b. Categorical semantics
c. Denotational and game semantics
d. Quantitative models (timing, probabilities)
5. Algorithmic Analysis of Formal Systems
a. Type inference and type checking
b. Complexity analysis
c. Checking termination, confluence, and related properties
d. Formalisation and certification
6. Tools and Applications
a. Proof assistants and interactive theorem proving
b. Automated deduction (completion, constraints, equational logic...)
c. Symbolic computation
d. Implementation techniques for formal systems
e. Case studies and applications based on formal systems
Registration, accommodation, and travel information for CADE-25 and all the affiliated events can be found at the conference website. The call for the Woody Bledsoe Student Travel Award is included below.
1-3 August 2015: Workshops, Tutorials, Special Session, Competitions
4-7 August 2015: CADE main conference, Competitions
CADE is the major forum for the presentation of research in all aspects of automated deduction. The CADE-25 conference programme will include invited talks, paper presentations, system descriptions, workshops, tutorials, system competitions, a poster session, and a special jubilee session on the past, present, and future of automated deduction.
Invited speakers (CADE-25 jubilee session)
Invited speakers (CADE-25 main conference)
Numerous further invited presentations will be part of the CADE-25 workshop program. Reception and dinner speeches will be given by Wolfgang Bibel and Jörg Siekmann.
The Woody Bledsoe Student Travel Award was created to honor 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 CADE-25 Woody Bledsoe Student Award will be partially reimbursed (e.g., between Euro 200 and Euro 750) 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 CADE-25 should be sent by e-mail to the chairs and conference organizers.
Nominations must arrive no later than 21 June 2015. The winners will be notified by 28 June 2015.
The awards will be presented at CADE-25; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.
This is the seventh conference on this topic. The first, second, fourth and sixth editions of conference were organized by Department of Logic and Methodology at Łódź University. The third and fifth edition was organized by Department of Logic at NCU in Toruń. The thematic range of the conference remains the same: theories of nonclassical logics (modal, many-valued, temporal, paraconsistent, epistemic, deontic, substructural, and nonmonotonic logic) and their applications in computer science, artificial intelligence, formal linguistics, cognitive studies, as well as to the deeper analysis of traditional philosophical problems.
The deadline for abstracts is 15 July 2015. See the conference web site for details.
Since 1994, the RelMiCS meetings on Relational Methods in Computer Science have been a main forum for researchers who use the calculus of relations and similar algebraic formalisms as methodological and conceptual tools. The AKA workshop series on Applications of Kleene algebra started with a Dagstuhl seminar in 2001 and was co-organised with the RelMiCS conference until 2009. Since 2011, joint RAMiCS conferences continue to encompass the scope of both RelMiCS and AKA.
If you are doing a PhD or an MSc in the research areas of the RAMiCS conference, please consider submitting an extended abstract of your ongoing work for presentation at the conference. The deadline for extended abstracts is 3 July 2015. See the conference web site for details.
MICAI is an international conference covering all areas of Artificial Intelligence, traditionally held in Mexico. The conference is organized by the Mexican Society for Artificial Intelligence (SMIA) and hosted by the Instituto de Investigaciones Eléctricas, Cuernavaca, Mexico, near Mexico City. The scientific program includes keynote lectures, paper presentations, tutorials, panels, and workshops.
The deadline for abstracts is 23 June 2015. See the conference web site for details.
Knowledge engineering refers to all technical, scientific and social aspects involved in building, maintaining and using knowledge-based systems. Knowledge engineering is a multidisciplinary field, bringing in concepts and methods from several computer science domains such as artificial intelligence, databases, expert systems, decision support systems and geographic information systems. The KEOD conference aims at becoming a major meeting point for researchers and practitioners interested in the study and development of methodologies and technologies for knowledge engineering and ontology development.
The deadline for regular papers is 2 July 2015. See the conference web site for details.
The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world.
Prospective authors are required to register a title and an abstract by 30 June 2015. See the conference web site for details.
FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.
The paper submission deadline is 14 September 2015. See the conference web site for details.
iFM 2016 is concerned with how the application of formal methods may involve modelling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modelling and analysis; i.e., the combination of methods for system development, regarding modelling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.
Prospective workshop organizers are invited to submit proposals for workshops to be affiliated to iFM 2016, on topics related to the conferences main subjects. The deadline is 20 July 2015. Contact the workshop chair, Marcel Kyas, for details.
The minisymposium intends to discuss usability of technology applications in education in relation to proving and primarily focuses on a specific technology, Computer Theorem Proving (TP), for education in academia and beyond. The proposal is backed by increasing interest in technology integration in education to support proofs as well as the applications of TP.
For preparing discussions we invite submission of abstracts (at most 3 pages) on topics including, but not limited to: demonstration of tools supporting proofs and using TP technology; experiences from academic courses of various kinds using TP-based software; applications of mathematics and mathematical activities which might specifically take advantage from support by TP-based software; mathematical concepts and TP technology specifically relevant for software support in teaching and learning to prove; and experiences from initiatives and activities filling the gap between school and university. The submission deadline is 15 June 2015. See the minisymposium's web site for details.
The British Logic Colloquium is a general logic meeting covering a variety of topics within mathematical, philosophical and computer science logic. The meeting will include ten invited talks and a number of contributed talks. Anyone wishing to contribute a talk should send an abstract (of about 250 words) to blc-2015@cl.cam.ac.uk by 15 July 2015.
Moreover, the BLC PhD day (on 1 and 2 September) provides an opportunity for postgraduates to meet and discuss their research or area of interest with fellow young logicians. If you wish to attend the PhD day, please email blc-2015-phd@maths.cam.ac.uk, including your name, affiliation, and whether you would like to present a talk or a poster.
There is a limited number of bursaries available for students who wish to attend. A bursary will provide a subsidy for travel and accommodation costs. Applications for bursaries should be accompanied by a short paragraph stating your affiliation, the name of your supervisor and a brief description of your research; priority will be given to those contributing a talk in either the PhD day or the main BLC meeting. Deadline: 15 July 2015.
Strategic reasoning is one of the most active research areas in the multi-agent system domain. The literature in this field is extensive and provides a plethora of logics for modelling strategic ability. Theoretical results are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, and automatic players capable of beating expert human adversary, just to cite a few. All these examples share the challenge of developing novel theories and tools for agent strategies that take into account the likely behaviour of adversaries. The SR international workshop aims to bring together researchers working on different aspects of strategic reasoning in computer science, artificial intelligence and multi-agent systems research, both from a theoretical and a practical viewpoint.
Submissions should be an abstract of at most 5 pages. The submission deadline is 1 July 2015 (strict). See the workshop web site for details.
The Design and Implementation of Formal Tools and Systems (DIFTS) workshop emphasizes insightful experiences in formal tools and systems design. The workshop provides an opportunity for discussing engineering aspects and various design decisions required to put formal tools and systems into practical use.
The workshop is co-located with FMCAD 2015 and SAT 2015. The regular talks of DIFTS workshop will be on September 26, 2015. The full-day tutorial (joint with FMCAD 2015, SAT 2015, and MEMOCODE 2015) will be on September 27, 2015.
The workshop specifically solicits contributions with substantial engineering details that often do not get published but have significant practical impact. Papers in the following two categories are solicited: (a) system category (10 pages, double column, 11pt), and (b) tool category (8 pages, double column, 11pt). The abstract submission deadline is 7 July 2015. See the workshop web site for details.
The 2nd International Workshop on Learning and NonMonotonic Reasoning (LNMR 2015) is co-located with the 13th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2015).
This workshop follows from its first edition in 2013 in an attempt to provide an open forum for the identification of problems and discussion of possible collaborations among researchers with complementary expertise. To facilitate interactions between researchers in the areas of (machine) learning and nonmonotonic reasoning, we welcome contributions focusing on problems and perspectives concerning both learning and nonmonotonic reasoning.
Papers must be registered by 22 June 2015. See the workshop web site for details.
The 2015 ACL2 Workshop will be held in Austin, Texas, in conjunction with (and immediately following) FMCAD 2015. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. Keynote talks will be given by J Strother Moore and John O'Leary.
See the workshop web site for further information including paper submission, organization, venue, lodging, and eventually, registration and program information.
The 11th International Workshop on Developments in Computational Models will be a satellite event of ICTAC 2015 (International Colloquium on Theoretical Aspects of Computing). The aim of this workshop is to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.
Submissions should be an abstract of at most 5 pages. The submission deadline is 3 August 2015. See the workshop web site for details.
A full-day tutorial on superposition, organized by Stephan Schulz and Christoph Weidenbach, is scheduled as associated event of CADE-25. Superposition is the calculus behind successful automatic theorem provers such as E, SPASS, and Vampire. See the CADE web site for details.
A full-day tutorial on Isabelle is scheduled as associated event of CADE-25. Isabelle is a popular proof assistant based on higher-order logic.
A half-day tutorial on the Abella proof assistant is scheduled as associated event of CADE-25. Abella is based on lambda-tree syntax and is well-suited for reasoning about the meta-theory of programming languages and other logical systems which manipulate objects with binding.
A half-day tutorial on the Beluga language is scheduled as associated event of CADE-25. Beluga allows specification of formal systems (such as lambda-calculi and type systems) using a foundation of contextual modal logic.
A half-day tutorial on the CPROVER program verification system is scheduled as associated event of CADE-25. CPROVER is one of the largest, most established and powerful automatic verification systems for C and C++.
A half-day tutorial on the KeY system's sequent calculus is scheduled as associated event of CADE-25. is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented (e.g., Java) software as seamlessly as possible.
A half-day tutorial on the Lean prover is scheduled as associated event of CADE-25. Lean is a new theorem prover that aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.
A three-day tutorial on the Isabelle proof assistant will precede the ITP 2015 conference.
A three-day tutorial on the Coq proof assistant will follow the ITP 2015 conference.
The University of Innsbruck invites applications for a 6 year postdoctoral position in the Computational Logic research group. Candidates must hold a PhD degree in computer science. A strong background in computational logic (in particular term rewriting) is desired. The ideal candidate enjoys working with students at all levels. Candidates are expected to conduct research leading to a habilitation and contribute to teaching and administration. Knowledge of German is not essential.
The position is a full-time "B1/3 position" with teaching obligations of 4 hours per semester. The annual gross salary is approximately EUR 50,000. See also the official job advert (reference MIP-8628). Applications (including CV, publication list, and two letters of recommendation) must be submitted electronically no later than 30 June 2015. The starting date for the position is 1 October 2015. Informal inquiries may be addressed to aart.middeldorp at uibk.ac.at.
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.
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. Detailed information about the application process is available on the LogiCS web-page. Next application deadline: 1 July 2015.
The Inria Nancy – Grand-Est research center, colocated with LORIA, is looking for a confirmed (or an outstanding junior) software engineer for the development of a new counterexample generator for higher-order logic. The targeted hiring date is 1 October 2015. The contract is for two years. The montly salary is expected to be between 2600 to 3200 EUR gross, depending on experience. This position can be interesting for an outgoing Ph.D. student or a strong programmer with a master's degree. Neither knowledge of French nor European citizenship are required.
This project aims at developing a generic counterexample generator for higher-order logic, targeted at the hundreds of users of Coq, Isabelle, and similar systems, to help them debug their specifications. This generator will be based on an SMT solver. Solid bases in functional programming and experience with logic are prerequisites.
See the official job advert or contact the newsletter editor for more information.
The Skolem award was established to reward a CADE paper that has passed the test of time. Starting this year, at every CADE the Skolem Award Committee selects a paper presented at the CADE held 10 years earlier to receive the Skolem award. Until 2025, additional awards will be given to cover CADE since its beginnings in 1968. The CADE board of trustees appointed Claude Kirchner to chair the first Skolem Award Committee, responsible for selecting the first round of awards at CADE-25. The first year's results are presented above. Congratulations to the winners!
I am also pleased to see the Herbrand award go to Andrei Voronkov. My students and I use Vampire (and countless other automatic theorem provers) on a daily basis to discharge interactive proof obligations. Congratulations, Andrei!
* * *
Back in March, I attended the second workshop on automating induction in Gothenburg, Sweden. It is exciting to see that many problems that looked very difficult are perhaps not as difficult as we thought. I went there as an observer, hoping to benefit from this research as an end user. I am particularly excited about combinations such as “superposition + induction” and “SMT + induction”. So far, the workshop series has been a mostly European affair, despite the pioneering work on automating induction in the ACL2 prover. The third workshop is expected to be held next spring in Vienna, Austria, hopefully with a wider geographical reach. A wiki and mailing list have been set up to discuss shared issues, such as benchmark problems and formats for problems and solutions. You are welcome to join!
* * *
This brings me to my last point. Increasingly, we see software reuse in the world of reasoners. The higher-order automatic prover LEO-II relies on a first-order prover to detect inconsistent clause sets early. Its rival Satallax is built around a SAT solver, and recent versions (starting with CASC 2013) also invoke a first-order prover. SMT solvers are built on SAT solvers in a nice modular fashion (at least in principle). And there are dozens more examples of the kind, sometimes with many layers of nesting. Basing your work on other people's work means that your software will get better even if you stop working on it actively. It is a great recipe for academic success!
However, for such a cooperative architecture to work well, each reasoner must be a good “team player”. Often, we put a lot of work into processing the input and forget about the output. When connecting formal tools together, it is crucial that the output is detailed enough and at the same level of abstraction as the input. This I call the Russian doll principle, and I like to see it as the practical materialization of institution theory. The TPTP/TSTP languages are well designed in that respect, since they closely reflect each other. Parallel efforts for SMT-LIB should be encouraged. As developers, we often forget that our software might be embedded in other tools. This belief that we stand at the top of the food (or tool) chain is usually either wrong or self-fulfilling.
Another related lesson, from Bjarne Stroustrup, is what he calls the zero-overhead principle. Consider a reasoner (prover, solver, model finder, etc.) B based on a reasoner A for a less rich logic. In an ideal world, B should be as efficient as A on problems within A's fragment. Such problems should just “slide through”. And problems mostly within A's fragment should still mostly slide through, with most of the work performed by A. I attribute much of the success of SMT solvers to this observation and find it unsurprising that Vampire's new SAT-based AVATAR architecture is giving that venerable prover such a boost. (Un)fortunately, it takes much more than a blind observance of the Russian doll and zero-overhead principles to get one's hands on an Herbrand award!