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.
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.
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.
An intermediate verification language (IVL), like Boogie or Why, is used as a stepping stone between a source programming language and a reasoning engine. IVLs promote modularization and sharing of infrastructure. The workshop is intended for topics related to any intermediate verification language, not just Boogie. Submission deadline: 1 May.
This workshop intends to gather the research communities for Computer Theorem proving (CTP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP), as well as Computer Algebra Systems (CAS) and Dynamic Geometry Systems (DGS). The goal of this union is to combine and focus systems of these areas to enhance existing educational software as well as studying the design of the next generation of mechanised mathematics assistants (MMA). Submission deadline: 29 April.
This workshop explores the adaptation of generic proof-search mechanisms to the specificities of particular theories, whether these are expressed in the form of axioms or expressed by sophisticated typing systems or inference systems. It will offer a venue for discussing and comparing techniques arising from communities ranging from logic programming to type theory-based proof assistants, or techniques imported from the fields of automated reasoning and SMT but with an ultimate view to build proofs or at least provide proof traces. Submission deadline: 2 May.
This workshop will bring together researchers working on proof production from automated theorem provers with potential consumers of proofs. The simple idea of proof exchange for theorem proving becomes quite complicated under the real-world constraints of highly complex and heterogeneous proof producers and proof consumers. Submission deadline: 2 May.
Theory engineering means the development and mechanisation of mathematical axioms, definitions, theorems and inference procedures as needed to cover the essential concepts and analysis tasks of an application domain. It is essential for the qualitative and quantitative modelling and analysis of computing systems. The aim is to present users with lightweight domain specific modelling languages, and to devolve the technical intricacies of analysis tasks as far as possible to tools that provide heavyweight automation. Submission deadline 29 April.
Unification is concerned with the problem of identifying given terms, either syntactically or modulo an equational theory. The UNIF workshop brings together researchers interested in theory, implementation, and applications of equational unification, higher-order unification, string unification, context unification, and many more, as well as related topics like constraint solving, matching, and narrowing. Submission deadline: 2 May.
The purpose of the tutorial is to give an overview of first-order theorem proving using the resolution and superposition calculus, to show how this calculus and its modifications are implemented in Vampire, and to explain the new features of Vampire.
The tutorial will provide a practical introduction to GF (Grammatical Framework), a system based on the idea of multilingual grammars, where a shared abstract syntax has reversible mappings to different concrete languages.
The tutorial will introduce the main ideas underlying the presenters' approach to symbolic model checking of infinite state systems based on SMT solving.
The tutorial will provide an overview of how the Mizar system can be used for practical computer formalisation of mathematical theorems. The system is best noted for its formal language derived from informal mathematics and the world's largest repository of formalised and computer-checked mathematical knowledge, the Mizar Mathematical Library (MML).
This tutorial is meant to increase the awareness of researchers in the CADE community for Quantified Boolean Formulas as a challenging, far from closed, research field.
The presenter will make a case for a comprehensive, logic-based theory of human thinking, drawing upon and reconciling a number of otherwise competing paradigms in AI and other fields, including production systems, logic programming, classical logic and decision theory.
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.
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'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.
Normal registration is open until 10 May 2011.
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 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.
Registration is open until May 8, see the workshop web page.
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.
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.
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.
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):
The special issue will contain contributions from the following invited authors, in addition to selected submitted contributions:
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.