General Information

First-order theorem proving is one of the core themes of Automated Deduction and one of its most mature subfields. First-order logic is sufficiently expressive to allow the specification of a wide range of problems in a natural way. At the same time an extensive variety of sound and complete calculi for first-order logic exists which have been implemented in a number of high-quality, fully automated reasoning systems. These in turn make it not only possible to effectively solve problems formulated in first-order logic, but also make it attractive to consider closely related logics, for example, many-valued, description and modal logics, from a first-order perspective.

This special issue is intended to present recent advances in the field to an audience of applied logicians, automated deduction theorists and applications specialists.

Topics

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

Submissions

This special issue welcomes original high-quality contributions that have been neither published in nor submitted to any journals or refereed conferences.

Authors of papers presented at FTP 2007 are welcome to submit extended and revised versions of their papers. However, contributions are not limited to those based on papers presented at FTP 2007; other submission are welcome as well. All submissions will be refereed to usual journal standards.

Submissions should be formatted according to the Instructions for AMAI submissions and authors are encouraged to use the AMAI LaTeX style files for preparing their submission. Preferably, submissions should be between 20 and 40 pages long.

Submissions should be made via Easychair at the following address:

http://www.easychair.org/conferences/?conf=ftp07specialissue/

Important Dates

Editors

The Journal

The scope of Annals of Mathematics and Artificial Intelligence is intended to represent a wide range of topics of concern to scholars applying quantitative, combinatorial, logical, algebraic and algorithmic methods to Artificial Intelligence areas as diverse as decision support, automated deduction, reasoning, knowledge-based systems, machine learning, computer vision, robotics and planning. It is hoped to influence the spawning of new areas of applied mathematics and the strenghtening of the scientific underpinnings of Artificial Intelligence.