ASSOCIATION FOR AUTOMATED REASONING

• From the AAR President, Larry Wos...
• Results of the CADE Trustee Elections 2008
• Reiner Hähnle re-elected as CADE vice-president
• Call for Nominations for Herbrand Award
• Call for Nominations: Editor-in-Chief of ACM Transactions on Computational Logic (ToCL)
• Woody Bledsoe Student Travel Awards
• Practical Progress in the Development of Automated Theorem Proving for Higher-order Logic
  • Abstract
  • The Higher-order TPTP
    • The Typed Higher-order Form (THF) Language
    • Collecting THF Problems, for the TPTP
    • TPTP Infrastructure for THF Problems
  • Collecting Solutions to THF Problems, for the TSTP
  • Higher-Order ATP for the TPTP
    • LEO-II
    • TPS
    • IsabelleP and IsabelleM
  • Current Work
• Conferences
  • RDP 2009, Fed. Conf. on Rewriting, Deduction, and Programming
  • CICM, Conferences on Intelligent Computer Mathematics
  • TABLEAUX 2009, Automated Reasoning with Analytic Tableaux and Related Methods
  • CADE-22: The Intl. Conference on Automated Deduction
  • TPHOLs, Theorem Proving in Higher-Order Logics
  • FroCoS'09, Frontiers of Combining Systems
  • The Intl. Tbilisi Symposium on Language, Logic and Computation
• Workshops
  • FTP 2009, the Workshop on First-Order Theorem Proving
  • VLL, Workshop on Visual Languages and Logic
• Special Issues
  • Special Issue of Studia Logica: The Contributions of Logic to the Foundations of Physics
• Positions
• System Announcement: the ProofWeb system
• Book Announcement: Handbook of Practical Logic and Automated Reasoning

From the AAR President, Larry Wos...

Many areas of logic can be studied successfully with an automated reasoning program. Equivalential calculus, classical propositional calculus, and others are such. Indeed, reasoning programs have occasionally played a key role in answering open questions in logic. Here you are offered a challenge.

An automated reasoning program can sometimes be used to show that no proof exists, where the argument does not depend on finding an appropriate model. For example, in the early 1980s, certain formulas in equivalential calculus were shown to be too weak, by characterizing all of the deducible formulas from each and showing that certain theorems could, therefore, not be deduced. From the viewpoint of logic, knowing that a formula cannot serve as a single axiom is often as interesting as knowing that it can.

Let's consider the axioms of the BCI logic.

P(i(i(x,y),i(i(z,x),i(z,y)))).  % B
P(i(i(x,i(y,z)),i(y,i(x,z)))).  % C
P(i(x,x)).                      % I

Condensed detachment is a typical rule of inference used to study such systems. It is captured by the following in the presence of hyperresolution.

-P(i(x,y)) | -P(x) | P(y).  %  condensed detachment

And here is a candidate formula that I find enticing.

P(i(u,i(i(v,w),i(i(i(x,x),i(y,i(u,v))),i(y,w))))). % BCI-Candidate 42

You are asked to formulate, if possible, an automated method showing that Candidate 42 is not a single axiom. It is, in fact, a theorem of BCI, but so far I have been unable to show that it is strong enough to be a single axiom. I doubt it is, my suspicion being based on the fact that, as it appears, all deducible theorems from the formula contain an alphabetic variant of i(x,x). But I would love to be proved wrong.

Here's another candidate formula presenting a challenge of a different type.

P(i(i(i(i(i(u,u),i(v,w)),i(i(x,v),w)),y),i(x,y))). % BCI-Candidate 46

I've included Candidate 46 in that its use as the sole hypothesis in the BCI logic seems somewhat promising, for it leads to theorems that are interesting. Yet I have not been able to prove its status as a single axiom.

Lest you be discouraged, let me assure you that I and a few of my colleagues have played with other candidate formulas that, after considerable effort, turned out to be single axioms.

Perhaps you will prove something of interest for the forthcoming CADE-22 conference, which focuses on logics and proofs.

Results of the CADE Trustee Elections 2008

An election was held from November 4 through Noveber 25 to fill two positions on the board of trustees of CADE Inc. Alessandro Armando, Christoph Benzmüller, Reiner Hähnle, Konstantin Korovin, Brigitte Pientka, and Cesare Tinelli were nominated for these positions. (See AAR Newsletter No. 82, November 2008.)

Ballots were sent by electronic mail to all members of AAR on November 4, for a total of 773 ballots. Of these, 139 were returned with a vote, representing a participation level of 18% (as compared to 16.4% in 2007, 16.0% in 2006, 18.1% in 2005 and 19.8% in 2004 and 2003). All votes were valid. Therefore, in each iteration of the STV algorithm (the STV (Single Transferrable Vote) algorithm is described in the CADE Bylaws), a candidate is elected iff he or she gets strictly more than 69 1st preference votes. Otherwise, the votes of the candidate with the least 1st preference votes are redistributed.

The following table reports the initial distribution of preferences among the candidates:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of K.Korovin one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of C.Tinelli one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of A.Armando one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of B.Pientka one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of C.Benzmüller one gets the following table:

Now, R.Hähnle reaches more than 69 1st preference votes, and is elected to the board of trustees. The redistribution of his votes produces the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of K.Korovin one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of A.Armando one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of B.Pientka one gets the following table:

No candidate reaches more than 69 1st preference votes. By redistributing the votes of C.Tinelli one gets the following table:

Now, C.Benzmüller reaches more than 69 1st preference votes, and is elected to the board of trustees.

Altogether, the two candidates who are elected to the board of trustees in this election are Reiner Hähnle and Christoph Benzmüller.

After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:

• Wolfgang Ahrendt (Secretary, appointed 5/2007)
• Franz Baader (President, CADE-19 Program Chair, elected 10/2003, reelected 10/2006)
• Peter Baumgartner (elected 10/2003, reelected 10/2006)
• Christoph Benzmüller (elected 11/2008)
• Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004, reelected 10/2007)
• Amy Felty (Secretary 5/2004 to 5/2007, elected 10/2007)
• Reiner Hähnle (Vice President, elected 10/2005, reelected 11/2008)
• Neil Murray (Treasurer)
• Renate Schmidt (CADE-22 program chair)
• Geoff Sutcliffe (elected 10/2004, reelected 10/2007)
• Aaron Stump (elected 10/2006)
• Andrei Voronkov (CADE-18 Program Chair, elected 10/2002, Vice President 2003, elected 10/2007)

On behalf of the AAR and CADE Inc., I thank Cesare Tinelli for his service as trustee during the past 3 years, Alessandro Armando for his service as ex-officio trustee (as IJCAR 2008 program co-chair), all candidates for running in the election, all the members who voted; and offer congratulations to Reiner Hähnle and Christoph Benzmüller on being elected.

Reiner Hähnle re-elected as CADE vice-president

The newly formed board of trustees held an election of the CADE vice-president, as the term of Reiner Hähnle as vice-president was expiring. Reiner was re-nominated, and furthermore, Maria Paola Bonacina was nominated. Out of these two, Reiner was elected. We thank Maria Paola and Reiner for running in the election, and offer congratulations to Reiner for being re-elected.

Call for Nominations for Herbrand Award

The Herbrand Award is given by CADE Inc. to honor 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

• Larry Wos (1992)
• Woody Bledsoe (1994)
• Alan Robinson (1996)
• Wu Wen-Tsun (1997)
• Gerard Huet (1998)
• Robert S. Boyer and J Strother Moore (1999)
• William W. McCune (2000)
• Donald W. Loveland (2001)
• Mark E. Stickel (2002)
• Peter B. Andrews (2003)
• Harald Ganzinger (2004)
• Martin Davis (2005)
• Wolfgang Bibel (2006)
• Alan Bundy (2007)
• Edmund Clarke (2008)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE 2009 is May 12, 2009.

Nominations pending from previous years must be resubmitted in order to be considered. Nominations should consist of a letter (preferably email) of up to 2,000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2,000 words of endorsement from two other seconders. Nominations should be sent to Franz Baader, president of CADE Inc. (baader (at) tcs.inf.tu-dresden.de) with copies to Wolfgang Ahrendt (ahrendt (at) chalmers.se).

Call for Nominations: Editor-in-Chief of ACM Transactions on Computational Logic (ToCL)

Nominations (including self nominations) are invited for the next Editor-in-Chief of ACM Transactions on Computational Logic (ToCL), see here. The position is for a term (renewable once) of three years, starting on July 1, 2009.

Candidates should be well-established researchers in areas related to computational logic, broadly conceived, and should have sufficient experience serving on conference program committees and journal editorial boards. Nominations, including a current curriculum vita and a brief (one page) statement of vision for ToCL, should be sent to Joseph Halpern , by May 1, 2009.

Final selection will be made by a Selection Committee, consisting of Joseph Halpern (chair – Cornell University), Kryzsztof Apt (CWI), Prakash Panangaden (McGill University), and Gordon Plotkin (University of Edinburgh). Nominations received after May 1, 2009, will be considered up until the position is filled.

Woody Bledsoe Student Travel Awards

The Woody Bledsoe Student Travel Award is intended to enable selected students to attend the 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 corresponding to CA$250 to CA$1000). Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.

The awards are sponsored by CADE Inc.

See the CADE 2009 web pages for more information, including application details. The deadline for applications is 16 June 2009.

Practical Progress in the Development of Automated Theorem Proving for Higher-order Logic

Abstract

There is a well established infrastructure that supports research, development, and deployment of first-order Automated Theorem Proving (ATP) systems, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library. This infrastructure has been central to the progress that has been made in the development of high performance first-order ATP systems. Until recently there has been no corresponding support in higher-order logic. In 2008, work commenced on extending the TPTP to include problems in higher-order logic, and developing the corresponding infrastructure and resources. These efforts aim to have an analogous impact on the development of higher-order ATP systems. This is a description of the practical progress that has been made towards this goal.

The Higher-order TPTP

The Typed Higher-order Form (THF) Language

The TPTP language is a human-readable, easily machine-parsable, flexible and extensible language, suitable for writing both ATP problems and solutions. A particular feature of the TPTP language, which has been maintained in the THF part, is Prolog compatibility. The THF language for logical formulae is a syntactically conservative extension of the existing first-order TPTP language, adding constructs for higher-order logic. The THF language has been divided into three layers: THF0, THF, and THFX. The THF0 core language is based on Church's simple type theory, and provides the commonly used and accepted aspects of a higher-order logic language. The full THF language drops the differentiation between terms and types, thus providing a significantly richer type system, and adds the ability to reason about types. It additionally offers more term constructs, more type constructs, and more connectives. The extended THFX language adds constructs that are "syntactic sugar", but are usefully expressive.

Here is an example of a TPTP problem file in THF0. The constructs that are not part of the first-order TPTP language are:

• The typing of constants and quantified variables. THF requires that all symbols be typed. Constants are globally typed in an annotated formula with role type, and variables are locally typed in their quantification (thus requiring all variables to be quantified).
• $tType for the collection of all types.
• $i and $o for the types of individuals and propositions. $i is non-empty, and may be finite or infinite.
• > (right associative) type mapping.
• ^ as the lambda binder.
• @ for (left associative) application.

Additional THF constructs, not shown in the example, are:

• The use of connectives as terms (THF0).
• !! and ?? for the π (forall) and σ (exists) operators (THF0).
• !> and ?* for Π (dependent product) and Σ (dependent sum) types (THF).
• [ ] for tuples (THF).
• * and + as cross product and union type constructors (THF).
• := as a connective for global definitions, and as a binder and separator for local definitions (ala letrec) (THFX).
• --> as the sequent connective (THFX).

Collecting THF Problems, for the TPTP

TPTP v3.7.0 was released in March 2009. This was a beta release of the THF part of the TPTP, and contained higher-order problems in only the THF0 language. There were 1275 THF problem versions, stemming from 852 abstract problems, in ten domains:

• ALG - 50 problems. These are problems concerning higher-order abstract syntax, encoded in higher-order logic.
• GRA - 93 problems. These are problems about Ramsey numbers, some of which are open in the mathematics community.
• LCL - 61 problems. These are of modal logic problems that have been encoded in higher-order logic.
• NUM - 221 problems. These are mostly theorems from Jutting's AUTOMATH formalization of the well known Landau book. There are also some Church numeral problems.
• PUZ - 5 problems. These are "knights and knaves" problems.
• SET and SEU - 749 problems. Many of these are "standard" problems in set theory. Many have TPTP versions in first-order logic, which allows for an evaluation of the relative benefits of the different encodings with respect to ATP systems for the logics. There is also a significant group of problems in dependently typed set theory, and a group of interesting problems about binary relations.
• SWV - 37 problems. The two main groups of problems are (i) security problems in access control logic, initially encoded in modal logic, and subsequently encoded in higher-order logic, and (ii) problems about security in an authorization logic that can be converted via modal logic to higher-order logic.
• SYN and SYO - 59 problems. These are simple problems to test properties of higher-order ATP systems.

1002 of the problems (78%) contain equality. 1166 of the problems (92%) are known or believed to be theorems, 26 (2%) are known or believed to be non-theorems, 4 (0%) are are known or believed to be unsatisfiable sets of formulae, 3 (0%) are are known or believed to be satisfiable sets of formulae, 68 (5%) are open, and the remaining 8 problems (0%) have unknown status. These problems can be downloaded as part of TPTP v3.7.0 from the TPTP web site, or browsed online. Many more problems are expected by the time TPTP v4.0.0 is released in August 2009.

TPTP Infrastructure for THF Problems

From a TPTP user perspective, the TPTP2X utility distributed with the TPTP will initially be most useful for manipulating THF problems. TPTP2X has been extended to read, manipulate, and output (pretty print) data in the full THF language. Additionally, format modules for outputting problems in the TPS, Twelf, OmDoc, and Isabelle formats have been implemented. The TPTP4X tool has also been extended to read, manipulate, and output data in the THF0 language, and will be extended to the full THF language in 2009.

The SystemOnTPTP interface for running ATP systems and tools on TPTP problems and solutions has been updated to deal with THF data, including use of the new higher-order formats output by TPTP2X.

Internally, an important resource is the Twelf-based type checking of THF problems, implemented by exporting a problem in Twelf format, and submitting the result to the Twelf tool. The BNF based parsers for the TPTP naturally parse the full THF language, and the lex/yacc files used to build these parsers are freely available.

Collecting Solutions to THF Problems, for the TSTP

The Thousands of Solutions from Theorem Provers (TSTP) solution library, the "flip side" of the TPTP, is a corpus of contemporary ATP systems' solutions to the TPTP problems. Three higher-order ATP systems, LEO-II 0.99a, TPS 3.0, and two automated versions of Isabelle 2008 (one - IsabelleP - trying to prove theorems, the other - IsabelleM - trying to find (counter-)models), have been run over the 1275 THF problems in TPTP v3.7.0, and their results added to the TSTP. The systems are described below. This table tabulates the numbers of problems solved. The results show that the GRA Ramsey number problems are very difficult - this was expected. For the remaining domains the problems pose interesting challenges for the ATP systems, are the differences between the systems lead to different problems being solved, including some that are solved uniquely by each of the systems.

Higher-Order ATP for the TPTP

Research and development of computer-supported reasoning for higher-order logic has been in progress for as long as that for first-order logic. It has become clear that the computational issues in the higher-order setting are significantly harder than those in first-order. Thus, while there are many interactive proof assistants based on some form of higher-order logic, there are few automated systems for higher-order logic. The three (fully automatic) higher-order ATP systems that we know of are LEO-II, TPS, and IsabelleP/M. These are available for use in the SystemOnTPTP interface.

LEO-II

LEO-II is a resolution based higher-order ATP system. LEO-II is implemented in Objective Caml, and is freely available under a BSD like licence. LEO-II is designed to cooperate with specialist systems for fragments of higher-order logic. Currently, LEO-II is capable of cooperating with the first-order ATP systems E, SPASS, and Vampire. LEO-II directly parses THF0 input, communicates with the cooperating first-order ATP system uses TPTP standards, has been debugged using examples in the TPTP library, and will soon produce THF0 output.

TPS

TPS is a higher-order theorem proving system that has been developed under the supervision of Peter B. Andrews since the 1980s. Theorems can be proven either interactively or automatically. In TPS there are flags that can be set to affect the behavior of automated search. The automated TPS used for solving THF problems uses two different collections of flags, in modes called MS98-FO-MODE and BASIC-MS04-2-MODE. As the two modes have quite different capabilities, they are run in competition parallel as a simple way of obtaining greater coverage. It was this competition parallel version of TPS that produced the 532 proofs noted in the table above.

IsabelleP and IsabelleM

Isabelle is a proof assistant for higher-order logic, which is normally used interactively. A fully automatic version, called IsabelleP, has been implemented using strategy scheduling of the nine automatic tactics simp, blast, auto, metis, fast, fastsimp, best, force, and meson. While it was probably never intended to use Isabelle as a fully automatic system, this simple automation provides useful capability. The ability of Isabelle to find (counter-)models using the refute tactic has also been integrated into an automatic system, called IsabelleM.

Current Work

• The first THF division of CASC is being organized, and will be part of CASC-22 at CADE-22.

• The core work of collecting THF problems is proceeding.

• Problems in the full THF and THFX languages are being collected, and TPTP infrastructure for processing these problems is being developed.

• The Java parser for the TPTP language is being extended to read the THF language.

• Users are being identified.

Users and developers of ATP for higher-order logic are encouraged to submit higher-order problems to the TPTP, and to enter systems into CASC-22. Questions, suggestions, and contributions should be sent to Geoff Sutcliffe.

Conferences

RDP 2009, Fed. Conf. on Rewriting, Deduction, and Programming

The Federated conference on Rewriting, Deduction, and Programming will take place on June 28 to July 03, 2009, in Brasília, Brazil.

It consists of two main events:

• RTA'09, the conference on Rewriting Techniques and Applications.
• TLCA'09, the conference on Typed Lambda Calculi and Applications.

There are a number of collocated events, namely:

• ISR'09, the Intl. School on Rewriting
• HOR'09, the Intl. Workshop on Higher-Order Rewriting
• LSFA'09, the Workshop on Logical and Semantic Frameworks, with Applications
• RULE'09, the International Workshop on Rule-Based Programming
• WFLP'09, the Workshop on Functional and (Constraint) Logic Programming
• WRS'09, the Workshop on Reduction Strategies in Rewriting and Programming
• IFIP WG 1.6, the IFIP Working Group 1.6 meeting

Early registration closes on May 1.

See the conference web page for full details!

CICM, Conferences on Intelligent Computer Mathematics

This is a federated conference that will take place on July 6–12, 2009 in Ontario, Canada.

It consists of two conferences:

• Calculemus 2009, the Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, July 6–7. Calculemus is dedicated to the integration of computer algebra systems and systems for mechanised reasoning, interactive theorem provers or proof assistants, and automated theorem provers.

  For short papers on emerging trends, the abstract submission deadline is April 30, and the submission deadline May 7, 2009.

• MKM 2009, the Intl. Conf. on Mathematical Knowledge Management, July 10–12.

Additionally, there will be the following workshops:

• CCA, Compact Computer Algebra, 10 July - 11 July
• DML, Towards a Digital Mathematics Library, 7 July - 9 July
• MathUI Mathematical User Interfaces, 6 July
• OpenMath Workshop on OpenMath, 9 July
• Pen-Math Pen-Based Mathematical Computation, 8 July - 9 July

See the conference web page for full details on all events.

TABLEAUX 2009, Automated Reasoning with Analytic Tableaux and Related Methods

The next International Conference on Automated Reasoning with Analytic Tableaux and Related Methods will take place in Oslo, Norway, July 6–10, 2009.

TABLEAUX 2009 will be collocated with FTP 2009.

There will be three smaller workshops on July 6:

• Tableaux versus automata as logical decision methods, organised by Valentin Goranko (Univ. of the Witwatersrand, Johannesburg, South Africa), see the workshop web page for details.
• Proofs and Refutations in Non-Classical Logics, organised by Roy Dyckhoff (Univ. of St Andrews, Scotland) and Didier Galmiche (LORIA, Henri Poincaré Univ., Nancy, France), see the workshop web page for details.
• Genzen Systems and Beyond, organised by Kai Brünnler (Univ. of Bern, Switzerland) and George Metcalfe (Vanderbilt Univ., Nashville, USA), see the workshop web page for details.

Submission to all three workshops is still possible.

Two tutorials will be part of the Tableaux programme:

• The Theory of Canonical Systems, given by Arnon Avron and Anna Zamansky from Tel-Aviv University, Israel.
• LoTREC: Theory and Practice. Proving by Tableau becomes easier, given by Bilal Said and Olivier Gasquet from Université Paul Sabatier in Toulouse, France.

Registration will open soon, early registration will be possible until June 5.

For full details about this event, please refer to the conference web pages

CADE-22: The Intl. Conference on Automated Deduction

This year's International Conference on Automated Deductions will be hosted by McGill University, Montreal, Canada August 2–7, 2009.

CADE is the major forum for the presentation of research in all aspects of automated deduction.

The following subsidiary events will be part of CADE this year:

• Workshops:
  • Automated Deduction: Decidability, Complexity, Tractability (ADDCT)
  • Beyond SAT: What About First-Order Logic?
  • Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
  • Modules and Libraries for Proof Assistants (MLPA)
  • Proof Search in Type Theories (PSTT)
  • Satisfiability Modulo Theories (SMT)
  • The International Workshop on Unification (UNIF)
  • TPTP World Workshop (TPTPWoWo)
• Tutorials:
  • Hierarchical and Modular Reasoning in Complex Theories
  • Probabilistic Analysis Using a Theorem Prover
  • (Challenges and Solutions for) Precise, Automated and Scalable Verification of Systems Software Using SMT solvers
  • Logics with undefinedness: How to modify a traditional logic so that it handles undefinedness in accordance with mathematical practice
• System competitions:
  • The CADE ATP System Competition (CASC)
  • Satisfiability Modulo Theories Competition (SMT-COMP)

Submission to all workshops is still possible!

Registration will open around May 20. The deadline for early registration is June 30.

See here for full details on this conference.

TPHOLs, Theorem Proving in Higher-Order Logics

The 22th International Conference on Theorem Proving in Higher Order Logics, TPHOLs, will take place on August 17–20, 2009 in Munich, Germany.

TPHOLs is a series of international conferences that brings together researchers working in all areas of interactive theorem proving, higher-order logics, and related topics.

The following workshops will be collocated with TPHOLs:

• PLMMS, Programming Languages for Mechanized Mathematics Systems (21 August)
• Coq Workshop (21 August)
• Isabelle Developers Workshop (13 - 15 August)

See the conference web page for full details!

FroCoS'09, Frontiers of Combining Systems

This symposium well take place in Trento, Italy, on September 16–18th, 2009.

FroCoS wants to offer a common forum for research activities in the general area of combination, modularization and integration of systems (with emphasis on logic-based ones), and of their practical use. Topics of interest include (but are not limited to):

• combinations of logics such as combined predicate, temporal, modal, or epistemic logics;
• combinations and modularity in ontologies;
• combination of decision procedures, of satisfiability procedures, and of CS techniques;
• combinations and modularity in term rewriting;
• integration of equational and other theories into deductive systems;
• combination of deduction systems and computer algebra;
• integration of data structures into CLP formalisms and deduction processes;
• hybrid methods for deduction, resolution and constraint propagation;
• hybrid systems in knowledge representation and natural language semantics;
• combined logics for distributed and multi-agent systems;
• logical aspects of combining and modularizing programs and specifications.

Proceedings will be published in the Springer LNAI series.

Abstract submission deadline: April 26th, 2009
Full paper submission deadline: May 3rd, 2009

See the conference web page for further details.

The Intl. Tbilisi Symposium on Language, Logic and Computation

This symposium will take place in Bakuriani, Georgia, September 21–25, 2009.

The program committee invites submissions of two page abstracts on all aspects of language, logic and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:

• Natural language syntax, semantics, and pragmatics
• Constructive, modal and algebraic logic
• Linguistic typology and semantic universals
• Logics for artificial intelligence
• Information retrieval, query answer systems
• Logic, games, and formal pragmatics
• Language evolution and learnability
• Computational social choice
• Historical linguistics, history of logic

The submission deadline is May 1, 2009 ; notification is due June 15. Accepted submissions will appear in the conference proceedings. The proceedings of the Six and Seventh International Tbilisi Symposium have been published in the LNAI series with Springer.

See the conference web page for details.

Workshops

FTP 2009, the Workshop on First-Order Theorem Proving

This years FTP workshop will take place in Oslo, Norway, July 6–7, 2009. FTP be collocated with the Tableaux conference.

The workshop welcomes original contributions on theorem proving in first-order classical, many-valued, modal and description logics, including (but not restricted to):

• theorem proving in first-order classical, many-valued, and modal logics, including:
  • satisfiability in propositional logic,
  • satisfiability modulo theories,
  • specialized decision procedures,
  • constraint reasoning,
  • equational reasoning,
  • term rewriting,
  • resolution,
  • paramodulation/superposition;
• strategies and complexity of theorem proving procedures;
• implementation techniques;
• applications of first-order theorem provers to:
  • program verification,
  • model checking,
  • artificial intelligence,
  • mathematics,
  • computational linguistics.

The deadline for paper submissions is April 20.

Accepted submissions will be published as a technical report of the University of Oslo. They will also be available on the web. As for the previous editions of FTP, a journal special issue is planned after the workshop.

Check the workshop web page for further details.

VLL, Workshop on Visual Languages and Logic

This workshop will take place In Corvallis, Oregon, US, on September 20, 2009.

The purpose of the VLL workshop is to explore the current state of research at the intersection of logic and visual languages, examining notations or software in which a graphical structure provides the foundation for, or a visualisation of, a system of logic. Topics of interest include, but are not limited to:

• Graphical notations for logics (either classical or non-classical, such as first or higher order logic, temporal logic, description logic, independence friendly logic, spatial logic)
• Diagrammatic reasoning
• Theorem proving
• Formalisation (syntax, semantics, reasoning rules)
• Expressiveness of visual logics
• Visual logic programming languages
• Visual specification languages
• Applications
• Tool support for Visual Logics

The submission deadline is June 22, 2009.

See the event's web page for full details.

Special Issues

Special Issue of Studia Logica: The Contributions of Logic to the Foundations of Physics

The special issue specifically, though not exclusively, invites contributions on the following topics:

• The use of techniques originating from classical logic, modal logic and multi-dimensional modal logics, spatial logic, dynamic logic, temporal logic, epistemic logic, linear logic and other resource-sensitive logics, intuitionistic logic, game logics, process algebras, co-algebraic logics, categorical logics, many-valued logics, quantum logics etc. to formalize physical theories or to reason about their concepts, phenomena and/or applications.
• Logical techniques used in quantum information theory, including quantum computation, quantum communication, quantum cryptography and quantum programming.
• Philosophical contributions on the meaning of concepts such as truth, consequence, completeness, implication and (quantum) information viewed at the interface of Logic and Physics.
• Open problems in modern physics, soliciting new techniques from logic, computation or information theory.
• Explorations on how to use new formal methods in combination with insights and interpretations in the philosophy of physics to yield new perspectives on the main foundational issues and open problems in modern physics.
• Answers to the questions: "What can physics learn from logic?" and/or "What can logic learn from physics?"

DEADLINE FOR SUBMISSION OF MANUSCRIPTS: May 31, 2009

The full CfP, including submission instructions is available in PDF format here

Positions

System Announcement: the ProofWeb system

ProofWeb is a system for using proof assistants (also known as interactive theorem provers) through the web. It is taylored specifically to practising natural deduction in logic courses. The ProofWeb home page which is the entry point into the system, and which contains all relevant information about it can be found at:

ProofWeb can be used for free, even without registration. It can be used with just a web browser, without even installing a plug-in. ProofWeb was developed to be used with the logic textbook Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan which is published by Cambridge University Press, but it also can be used in conjunction with other textbooks. ProofWeb both supports "Gentzen-style" natural deduction in which proofs are tree-like derivation, and "Fitch-style" natural deduction in which proofs are lists of lines that grouped using boxes or "flags". ProofWeb was developed for the Coq proof assistant, but has been extended to various other proof assistants. ProofWeb is already being used in several proof assistant courses and introductory logic courses.

ProofWeb has been used in prototypes for more ambitious systems, most notably in the MathWiki prototype for a Wikipedia-like system that is integrated with on-line proof assistants, and the PC-Extra calculator which can calculate numerical expressions to arbitrary precision and where the correctness of the answers is simultaneously being proved by Coq.

ProofWeb was developed in the Netherlands at the Radboud University Nijmegen and Free University Amsterdam with money from the SURF Foundation. The developer of the ProofWeb system is Cezary Kaliszyk from the Radboud University. Currently the other members of the ProofWeb team are Dan Synek, Femke van Raamsdonk, Freek Wiedijk, Herman Geuvers and James McKinna.

Book Announcement: Handbook of Practical Logic and Automated Reasoning

John Harrison

Cambridge University Press 2009, 702 pages

ISBN: 9780521899574

The sheer complexity of computer systems has meant that automated reasoning, i.e. the ability of computers to perform logical inference, has become a vital component of program construction and of programming language design. This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with practical application, all with the minimum of prerequisites. The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the general area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.

• One stop reference that is broad-based and self-contained
• Constructive approach that enables topics to be discussed algorithmically
• Implementation of these algorithms provided as code
• Can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study

For more information, see the publisher's web page.

For code and resources, see here.