ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER No. 91, April 2011

From the AAR President, Larry Wos...

For those of you who enjoy challenges in logic, I offer three theorems to prove in intuitionism. I give ten axioms from Horn, and the negations of the three targets. The inference rule to use is condensed detachment, captured by the following clause in the presence of hyperresolution.

-P(i(x,y)) | -P(x) | P(y).

The ten axioms are the following.

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

The following negated theorem was easy to prove with OTTER.

-P(i(i(p,b),i(a(p,c),a(b,c)))) | $ANS(H334).

In contrast, the following two provided each a challenge.

-P(k(i(a(k(p,q),r),k(a(p,r),a(q,r))),i(k(a(p,r),a(q,r)),a(k(p,q),r)))) | $ANS(HIF4).
-P(k(i(n(a(p,q)),k(n(p),n(q))),i(k(n(p),n(q)),n(a(p,q))))) | $ANS(HIF5).

If any of you find a proof of either of the last two, a proof consisting of strictly fewer than 20 applications of condensed detachment, I would enjoy learning of such.

Woody Bledsoe Student Travel Awards

The Woody Bledsoe Student Travel Award is intended to enable selected students to attend the Conference on Automated Deduction (CADE) by covering much of their expenses.

The winners of the travel award will be (partially) reimbursed for their conference registration, transportation, and accommodation expenses (past awards have varied, but have typically been been 150 - 600 Euro, depending on the degree of active participation and the distance that needs to be travelled). Preference will be given to students who are author or co-author of a paper at the conference or who contributed to an associated event, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.

See the CADE 2011 web pages for more information, including application details.

The deadline for applications is 10 June 2011.

Conferences

CADE 23, Conference on Automated Deduction

The 23rd Conference on Automated Deduction will include an attractive array of satellite workshops, including workshops, tutorials, and of course a competition. Refer to the CADE 23 satellite event web page for up to date information.

Workshops

Competitions

Tutorials

FroCoS 2011, Frontiers of Combining Systems

FroCoS 2011, the 8th International Symposium Frontiers of Combining Systems will take place in Saarbrücken, Germany, on 5–7 October 2011.

In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation and automated reasoning, there is an obvious need for using specialised formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialised systems must be combined with each other, and they must be integrated into general purpose systems.

Like its predecessors, FroCoS 2011 wants to offer a common forum for research activities in the general area of combination, modularisation and integration of systems (with emphasis on logic-based ones), and of their practical use.

Research papers of up to 16 pages may be submitted until 29 April 2011 (abstracts by 22 April). Accepted papers will be published in Springer's LNCS series.

Refer to the conference web page for details.

TIME 2011, Temporal Representation and Reasoning

The 18th International Symposium on Temporal Representation and Reasoning (TIME 2011) will be hosted by the University of Lübeck, Germany. TIME 2011 aims to bring together researchers from distinct research areas involving the management of temporal data as well as the reasoning about temporal aspects of information.

Paper submission is still open until 23 April 2011. Refer to the conference web page for submission details.

RDP 2011, Rewriting, Deduction, and Programming

RDP'11 is the sixth edition of the International Conference on Rewriting, Deduction, and Programming, consisting of two main conferences: Rewriting Techniques and Applications (RTA'11) and Typed Lambda Calculi and Applications (TLCA'11).

RDP'11 will take place in Novi Sad, Serbia, from Sunday, 29 May 2011 to Friday, 3 June 3 2011.

Invited speakers:

Workshops:

Normal registration is open until 10 May 2011.

Workshops

FTP 2011, Workshop on First-Order Theorem Proving

The Eighth International Workshop on First-Order Theorem Proving will take place in Bern, Switzerland on July 4, 2011, co-locating with Tableaux 2011, The 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods on July 4-8, 2011.

The series of FTP workshops focusses on all aspects of theorem proving in first-order logic. It aims to be a forum for the presentation of original work, and for the discussion of work in progress.

Relevant topics for the workshop include (but are not limited to)

Extended abstracts of up to 15 pages, system descriptions of up to 10 pages, and presentation-only papers (which can be submitted or published elsewhere) can be submitted until 2 May 2011.

Accepted submissions will be published as CEUR Workshop Proceedings and will be distributed at the workshop.

As for the previous editions of FTP, a journal special issue is planned after the workshop. The submission will be open to papers on First-Order Theorem Proving.

Full details including submission instructions can be obtained from the FTP 2011 web pages.

WoLLIC 2011, Workshop on Logic, Language, Information and Computation

WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. The eighteenth WoLLIC will be held at the University of Pennsylvania, Philadelphia, USA, from May 18th to 20th, 2011.

Invited Speakers:

Registration is open until May 8, see the workshop web page.

DIFTS'11, Design and Implementation of Formal Tools and Systems

The first DIFTS (Design and Implementation of Formal Tools and Systems) workshop will take place in Austin, Texas, U.S.A., on 3 November 2011, co-located with FMCAD'11. The workshop intends to be a forum for questions of design and implementation of all manner of formal systems, including systems for automated reasoning, theorem proving, verification, etc.

Both 10 page system descriptions, and 8 page tool descriptions can be submitted until 6 June 2011, with abstracts due on 30 May.

Full details are available from the workshop web page.

Beth Dissertation Award: Call for Nominations

Since 2002, FoLLI (the Association for Logic, Language, and Information, http://www.folli.org) awards the E.W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2010. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of three fields of Logic, Language, and Computation. Interdisciplinarity is an important feature of the theses competing for the E.W. Beth Dissertation Prize.

The deadline for nominations is 8 May 2011. See the FoLLI homepage for details.

Special Issue of Studia Logica on Logic and Games

Guest editor: Thomas Ågotnes
Submission deadline: 15 August 2011

Studia Logica is extending its scope. In future the journal will not only cover pure logic but also applications of formal-logical methods in philosophy and cognitive science. To mark this change, the journal will have several special issues, of which this is one.

Theme of the special issue

Formal logic and game theory can meet in many ways. While the use of games-for-logic, e.g., to define semantics of quantifiers or to compare logical models, goes back a long time, logic-for-games is a more recent and currently very active research direction which has been precipitated by the introduction of the notion of (multi-)agency in logic. If agents are assumed to be self-interested and to act rationally, then reasoning about action in a multi-agent setting requires reasoning about game theoretic concepts. Furthermore, logics capturing, e.g., the principles of action, belief, knowledge, time, preference and so on, can help explaining the foundations of game theoretic solutions, algorithms, etc.

The goal of the special issue of Studia Logica on Logic and Games is to illustrate current trends and present recent advances in this field. We invite submissions on all topics in the intersection between formal logic and game theory, including the following topics (not an exhaustive list):

Invited authors

The special issue will contain contributions from the following invited authors, in addition to selected submitted contributions:

Submission

Submitted papers are should be between 15 and 20 pages long (including bibliography), and should be formatted according to the Studia Logica LaTex style. Some contributions in Microsoft Word may also be accepted: authors should consult the guest editor about this possibility. Only electronic submissions will be accepted. The authors should send an email with subject "Studia Logica Submission" to the guest editor (Thomas Ågotnes, thomas.agotnes (at) infomedia (dot) uib (dot) no), with the file of the paper as an attachment, and the following information in the body of the email in plain text: paper title, author names, surface mail, email address of the contact author and a short abstract.

Submission deadline: 15 August 2011

All papers will be refereed according to the standards of the journal.