In December 2012, I fulfilled a promise of giving you some geometry.
I now give you more geometry, using axioms offered by the
brilliant and versatile logician A. Tarski:
In these clauses, T denotes betweenness and E equidistance.
Note that, for Tarski, between does not mean strictly between.
% identity axiom for betweenness: -T(x,y,x) | (x = y). % 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). % Pasch's (Inner Pasch) axiom (2 clauses): -T(x,v,u) | -T(y,z,u) | T(v,f1(x,v,u,y,z),y). -T(x,v,u) | -T(y,z,u) | T(z,f1(x,v,u,y,z),x). % 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).
If you have in hand the December 2012 column, you will note that I again have not included here the axioms regarding equality (such as reflexivity or symmetry). If you wish to see these equality axioms, with a slightly different notation, you can consult Chapter 6 of a book I wrote in 1987, 33 Basic Research Problems.
I have made one important change from the December column. Specifically, I have substituted two clauses for inner Pasch in place of the two clauses, the following, that had simply been labeled “Pasch's axiom” (but could have been called “outer Pasch”).
% Pasch's (outer Pasch) 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)).
And, most important, I have removed two clauses from that December axiom set, the following:
% 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).
I now offer two theorems as challenges to prove. In particular, I ask for proofs of the dependence of transitivity and connectivity of betweenness, dependent on the set of axioms given eralier in this column.
A word of warning: I suggest you tackle these challenges soon, for I address each in a forthcoming notebook of mine to be placed on my website.
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 2014 is:
15th April 2014
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
In the summer of 2014, Vienna will host the largest event in the history of logic. The Vienna Summer of Logic (VSL) will consist of twelve large conferences and numerous workshops, attracting an expected number of 2500 researchers from all over the world.
The conferences and workshops will deal with the main theme, logic, from three important aspects: logic in computer science, mathematical logic and logic in artificial intelligence.
This unique event will be organized by the Kurt Gödel Society at Vienna University of Technology from July 9 to 24, 2014 (see website for more details)
The VSL keynote speakers are
Dana Scott (Carnegie Mellon University) will speak in the opening session.
At the Vienna Summer of Logic, the Kurt Goedel Society will award three fellowship prizes endowed with 100.000 Euro each to the winners of the Kurt Goedel Research Prize Fellowship Competition “Logical Mind: Connecting Foundations and Technology.”
As announced in the previous AAR Newsletter, the 25th jubilee edition of the Conference on Automated Deduction, CADE-25, will be held in Berlin, Germany, from 2nd to 7th August 2015, with Christoph Benzmüller as Conference Chair. The CADE Board of Trustees is delighted to announce that Amy Felty and Aart Middeldorp will serve as PC-chairs.
The User Interfaces for Theorem Provers (UITP) workshop series provides a forum for researchers interested in improving human interaction with interactive and automated deduction systems in a broad sense.
The UITP'14 workshop will be held on 17 July 2014 as part of the Vienna Summer of Logic. For more information see the workshop website.
Papers should describe previously unpublished work (completed or in progress), and be at least 4 pages and at most 12 pages. We encourage concise and relevant papers. The submission deadline is: 4 May 2014.
The 4th Workshop on Practical Aspects of Automated Reasoning will beheld on 23 July 2014 in Vienna. PAAR will be associated with the 7th International Joint Conference on Automated Reasoning, IJCAR'14 and it will be part of the Vienna Summer of Logic 2014.
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.
Short abstracts of up to 10 pages can be submitted until 21 April 2012.
See the workshop web page for details.
UNIF 2014 is the 28th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of identifying terms, 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.
Topics of interest include syntactic and equational unification algorithms, matching and constraint solving, unification in modal, temporal, and description logics, narrowing, disunification, anti-unification, semi-unification, higher-order unification, complexity issues, implementation techniques, applications.
Short papers or extended abstracts, up to 5 pages in EasyChair style, should be submitted electronically as PDF files until 16 April 2014. For more details, please see the workshop web page.
The 9th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice will take place in Vienna, Austria on 17 July 2014.
This workshop will bring together designers, implementers, and practitioners of logical frameworks and meta-languages, where various aspects will be discussed, including their design and implementation on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand.
Both research papers (8 pages) and "work in progress" papers (4 pages) in ACM SIGPLAN style are solicited by the deadline of 2 May 2014.
For more details, including submission instructions, see the workshop web site.
The 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2014) will take place in Timisoara, Romania, on 22–25 September 2014.
SYNASC aims to stimulate the interaction between the two scientific communities of symbolic and numeric computing and to exhibit interesting applications of the areas both in theory and in practice. The choice of the topic is motivated by the belief of the organizers that the dialogue between the two communities is very necessary for accelerating the progress in making the computer a truly intelligent aid for mathematicians and engineers.
Proposals for Workshops, Tutorials, and Special Sessions are invited until 15 March 2014. Research papers are to be submitted until 30 April 2014, with abstracts due on 15 April.
Please refer to the Symposium Web Page for further details.
Semmering, Austria, July 10-12, 2014
http://satsmt2014.forsyte.at/
The application deadline for the school is 19 April 2014. Full details of the registration procedure are available at the school website.
The SAT/SMT Summer School aims at providing graduate students and researchers from university and industry with a comprehensive overview of research and methodology in satisfiability testing (SAT) and satisfiability modulo theories (SMT). The lectures cover the foundational and practical aspects of SAT and SMT technologies and their applications.
The Summer School program will feature four lectures per day, with the first two days dedicated to SAT and SMT, and the last to special topics. Two of the lectures will be organized as tutorials giving hands-on experience on SAT/SMT-based modelling.
List of invited lectures:
A more detailed program is available at the school website.
Organizers:
Pascal Fontaine (Inria, Loria, University of Lorraine, France)
Dejan Jovanović (SRI, U.S.)
Georg Weissenbacher (TU Wien, Austria)
Application deadline: March 31, 2014
Expected starting date of positions: September 1, 2014
The PhD student will join the Formal Methods group and contribute to its research on improving the quality of complex software systems. The Formal Methods group of Chalmers is an internationally recognised research group with a high-profile research track record and an excellent network of collaborators. The group's research focus is in the theoretical and practical aspects of formal software verification, including automated reasoning, interactive theorem proving, runtime verification, and test generation. Together with international collaborators, the group members co-developed widely recognised verification tools like KeY, Vampire, ALIGATOR, and LARVA.
The research of the advertised PhD position will be in the area of Software Verification, with a strong focus on the creative use and development of automated reasoning techniques for software verification. In particular, we are interested in designing and combining new methods in automated first-order theorem proving, satisfiability modulo theory solvers, symbolic computation, and program analysis for the generation and verification of complex program properties, such as invariants, interpolants, pre- and post-conditions.
Background in one or more of the following areas is expected: logic, formal methods, formal verification.
This position will be supervised by Prof. Laura Kovacs in the frame of her recently granted junior researcher project by the Swedish Research Council. Laura Kovacs is the main developer of the ALIGATOR tool and the co-developer of the world-leading theorem prover Vampire for applications of program analysis and verification.
The application should be written in English and include the following items:
It is important to include parts of your own work such as theses and articles that you have authored or co-authored. Please notice also that it is highly recommended that you include letters of recommendation; we typically get a large number of applications, and it is not feasible for us to request individual letters.
The application should be submitted electronically by March 31, 2014, here.
For further inquiries, contact Laura Kovacs, laura.kovacs (at) chalmers.se.