You undoubtedly have encountered very long expressions—very complex formulas or equations, for example. They can occur in logic, in mathematics, in circuit validation and design, in program verification, and perhaps in database inquiry. Like many people, you may find such expressions paralyzing! The result? You, and indeed many programs, such as W. McCune's OTTER, which I like to use—ignore them. You focus attention instead on the simpler expressions for initiating a line of reasoning.
What about the opposite situation: a problem that starts with simple axioms and derives a very complex formula? Yes, such problems do exist in the real world. I present one here from logic.
You are given a set of simple formulas or axiom systems, the following:
P(i(i(u,v),i(i(w,u),i(w,v)))). % B P(i(i(u,i(v,w)),i(v,i(u,w)))). % C P(i(u,u)). % I P(i(i(u,i(u,v)),i(u,v))). % W
The rule of inference for drawing conclusions, condensed detachment, is captured by the following, where " | " denotes logical or and "-" logical not.
-P(i(x,y)) | -P(x) | P(y).
For the logic with these four axioms, B, C, I, and W, Adrian Rezus has presented what purports to be a single axiom.
% Following is a Rezus-style single axiom for RI.
P(i(i(i(x, i(i(i(y, y), i(i(z, z), i(i(u, u), i(i(v, v), i(x, w))))), w)),
i(i(i(i(i(v6, v7), i(i(v7, v8), i(v6, v8))),
i(i(i(i(i(v9, i(v9, v10)), i(v9, v10)),
i(i(i(v11, v12), i(i(v12, v13), i(v11, v13))), v14)),
v14),
v15)),
v15),
i(i(v16,
i(i(i(v17, v17),
i(i(v18, v18), i(i(v19, v19), i(i(v20, v20), i(v16, v21))))),
v21)),
v22))),
v22)).
In order to be a single axiom, the Rezus formula must also be a theorem in this logic. So, I am asking you to prove it.
It's messy: 93 symbols.
And were you to start with the Rezus formula, on the way to a proof you would probably encounter expressions with more than 60 symbols. I'm therefore asking you to start with B, C, I, and W.
Actually, as you might expect—I am asking for a bit more. In many axiom systems, the properties are simple (for example, everyone is male or female). My challenge, then, is to find a general method that can derive (prove) very complex expressions from a set of axioms each of which is simple.
in recognition of his numerous seminal contributions to several areas of automated reasoning, including first-order theorem proving, term rewriting, completion, orderings, inductive reasoning, and pioneering research on abstraction, instance-based methods and search complexity in theorem proving.
The Award will be presented at IJCAR 2010, the 5th International Joint Conference on Automated Reasoning, July 19, 2010.
Dear Member of the Association for Automated Reasoning,
Nominations for four CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2010.
The members of the board of trustees are (in alphabetical order):
The terms of Maria Paola Bonacina, Amy Felty, Geoff Sutcliffe, and Andrei Voronkov expire. Amy Felty and Andrei Voronkov are eligible to be nominated for a second term. Maria Paola Bonacina and Geoff Sutcliffe have served two successive elected terms, and therefore are not eligible to be nominated for a third.
The term of office of Juergen Giesl as IJCAR 2010 program co-chair also ends. As outgoing ex-officio trustee, he is eligible to be nominated as an elected trustee.
In summary, we are seeking to elect four trustees.
Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at IJCAR 2010. 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.bonacina (at) univr (dot) it) and Wolfgang Ahrendt, CADE Secretary (ahrendt (at) chalmers (dot) se), up to the upcoming CADE business meeting (to be held on July 17th, at IJCAR 2010), or otherwise during the CADE business meeting.
The 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning will be held in Yogyakarta, Indonesia on October 10–15, 2010. The conference welcomes submissions on both theory and application of automated reasoning for any kind of logic, amongst other topics.
Note that the submission deadlines are very soon:
Abstract submission: June 14
Paper submission: June 18
See the conference web page for details.
The Federated Logic Conference, which includes most of the central events in automated reasoning this year, like IJCAR, the CASC competition, ITP, SAT, etc. will take place in Edinburgh, UK, on July 9–12, 2010.
The early registration phase is over, but regular registration fees still apply until June 30. You can register via the conference web page.
The 20th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2010) will be held in the Castle of Hagenberg, Austria, on July 23–25, 2010. The program consists of papers on a wide range of topics from program specification, verification, logic programming, etc. LOPSTR 2010 will be collocated with the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010)
Early registration is possible until June 21. See the symposium web page for full details.
This workshop will be held in Yogyakarta, Indonesia, on October 10, 2010, in the context of the LPAR conference.
Analyticity is a topic that connects foundational issues in logic with applications, mainly in automated deduction and analysis of proofs. The workshop is primarily intended to enhance awareness for its topic and to promote corresponding discussions and contacts between experienced experts and younger colleagues.
Organizers: Matthias Baaz, Christian Fermueller
Abstracts of 1–2 pages should be submitted until September 10.
See the workshop web page for details.
This workshop will be held in Yogyakarta, Indonesia, on October 10, 2010, in the context of the LPAR conference.
The purpose of IWIL is to share information about successful implementation techniques for automated reasoning systems and similar programs. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies.
Organizers: Evgenia Ternovska, Stephan Schulz, Geoff Sutcliffe
Contributions should be submitted until August 9, 2010.
See the workshop web page for details.