In my March column, I featured Tarskian geometry. I offered two theorems to prove as challenges. In that column, I also noted that you might attempt to meet those challenges soon in that I was about to place another notebook on my website, automatedreasoning.net, in which I would provide proofs of the two theorems. That notebook, on Tarskian geometry, now exists on the site. Its title is “An Amazing Approach to Plane Geometry.”
In this column, I again turn to Tarskian geometry, with a small but significant modification to the axiom system presented in the March column. In particular, I include here the axiom for transitivity of betweenness, and I replace two clauses for inner Pasch by two for outer Pasch. First, for your convenience, I again offer the axiom system found in the March column.
% 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).
In these clauses, T denotes betweenness and E equidistance.
Note that, for Tarski, between does not mean strictly between.
For your challenge here, you replace the two clauses for inner Pasch with the
following two for outer Pasch.
% 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)).
You also add the following clause for transitivity of betweenness.
% transitivity axiom of betweenness: -T(x,y,u) | -T(y,z,u) | T(x,y,z).
You are asked to find a proof of connectivity of betweenness from the amended set of clauses:
% connectivity axiom for betweenness: -T(x,y,z) | -T(x,y,u) | (x = y) | T(x,z,u) | T(x,u,z).
Yes, in the cited notebook on plane geometry, I do provide a proof of the theorem. But—and this might amuse you—my proof is a mathematical proof. I have not yet found a proof with OTTER.
Your challenge, then: Find a proof by means of automated reasoning.
in recognition of his pioneering research in automated reasoning, including his seminal contributions to the foundations of computational type theory, the creation of Nuprl - the first constructive type theory based theorem prover - the development of the correct-by-construction programming paradigm, and their applications to verification and synthesis of computer systems, including distributed computing.
Presented at:
IJCAR 2014
The 7th International Joint Conference on Automated Reasoning
July 19, 2014
Bernhard Gramlich, who was serving on the Board of Trustees of CADE Inc., passed away on June 3, 2014. CADE Inc. and the entire automated reasoning community mourn his loss.
After studying computer science in Karlsruhe and Kaiserslautern, Bernhard spent a few years as post-doc at INRIA Lorraine in Nancy. In 1998 he joined the Technische Universität Wien (Vienna), where he became Associate Professor in 2000. Among his many achievements, he served as Program Chair of FroCoS in 2005 and as Program Co-Chair of IJCAR in 2012. His interests in research and teaching centered around term rewrite systems and automated equational reasoning. His career was interrupted approximately one year ago when he was diagnosed with MSA, an aggressive incurable nerve disease. He is survived by his wife Iris and a son from a previous marriage.
We have lost an enthusiastic scientist, an engaged teacher, and a most amiable colleague and friend, always open, generous, forward looking, and capable of connecting with everyone. So long, Bernhard.
Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2014.
The current members of the board of trustees are (in alphabetical order):
The terms of Viorica Sofronie-Stokkermans and Geoff Sutcliffe expire. Both are eligible to be nominated for a second term.
Due to Bernhard Gramlich's untimely passing (cf. the obituary in this Newsletter), an additional trustee needs to be elected.
The term of office of Deepak Kapur as IJCAR 2014 program co-chair also ends. As outgoing ex-officio trustee, he is eligible to be nominated as elected trustee.
In summary, we are seeking to elect three trustees.
Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at IJCAR 2014. 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.
IJCAR 2014 will take place in Vienna, Austria, on 19–22 July 2014, as part of FLoC 2014, the Federated Logic Conference, which in turn is part of the Vienna Summer of Logic (VSL).
The following workshops will be associated with IJCAR:
There are numerous other workshops associated with the seven other FLoC conferences, see here.
IJCAR 2014 will also host the annual CASC (CADE Automated System Competition), and registration for that is still open until 13 June.
For full information about IJCAR, please refer to the conference web page.
GandALF 2014, the 5th International Symposium on Games, Automata, Logics, and Formal Verification will take place in Verona, Italy, on 10–12 September 2014.
The aim of the symposium is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization. Papers focused on formal methods are especially welcome. Authors are invited to submit original research or tool papers on all relevant topics in these areas. Papers discussing new ideas that are at an early stage of development are also welcome. The call of paper mentions automated deduction, decision procedures, first-order, higher-order, modal, and temporal logics among the topics of interest.
For details, go to the conference web site.
The 12th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2014, will take place in Seville, Spain, on 11–13 December 2014.
The conference welcomes papers with a strong AI component that make use of symbolic computation in a wide sense (not excluding but not restricted to computer algebra). However, AISC 2014 aims at extending the scope of this series of conferences to computing in AI thus covering new areas. The call for papers explicitly mentions Automated Reasoning as a topic of interest.
The deadline for paper submissions is 15 June 2014.
For details, please go to the conference website.
FMCAD 14 will be held in Lausanne, Switzerland, on 21–24 October, 2014. The conference will be co-located with MEMOCODE, the ACM/IEEE International Conference on Formal Methods and Models for Codesign, in Lausanne, Switzerland. MEMOCODE will take place from October 19 to 20, followed by a joint FMCAD/MEMOCODE tutorial day on October 21. FMCAD will continue from October 22 to 24, 2014.
FMCAD 2014 is the 14th in a series of conferences on the theory and application of formal methods in computer-aided design and verification of computer systems and related topics. FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing novel methods, technologies, theoretical results, tools, and open challenges in formal reasoning. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
Refer to the conference website for details.
ISR 2014, the 7th International School on Rewriting, will take place in Valparaíso, Chile, on 25–29 August 2014. The School will be co-located with 21st Workshop on Logic, Language, Information and Computation (WoLLIC 2014)
The School will offer two tracks: Track A, for newcomers in the field, or just for people who want to obtain a new, updated exposure; and Track B: for those who want to get deeper in the most recent developments and applications of rewriting.
Rewriting is a branch of computer science whose origins go back to the origins of computer science itself (with Thue, Church, Post, and many other prominent researchers). It has strong links with mathematics, algebra, and logic, and it is the basis of well-known programming paradigms like functional and equational programming, which are taught at the universitary level in many countries. In these programming paradigms and corresponding languages, the notions of reduction, pattern matching, confluence, termination, strategy, etc., are essential. Rewriting provides a solid framework for understanding, using, and teaching all these notions. Rewriting techniques are also used in many other areas of software engineering (scripting, prototyping, automated transformation of legacy systems, refactoring, web services, etc.) and are implemented in popular systems like Mathematica, Autocad, and others. Rewriting techniques play a relevant role in computing research, education, and industry.
See here for details.