Journal of Automated Reasoning Special issue on First-order Theorem Proving Volume 33, Numbers 3-4 Springer Science+Business Media B.V., October 2004. ISSN: 0168-7433 (Paper) 1573-0670 (Online).

Contents

• Call for papers
• Scope
• Special issue editors
• Accepted Papers
• Related Links

Following the tradition of the previous Workshops on First-order Theorem Proving, a special issue will be edited to commemorate the fourth workshop in this series. The special issue will be published by Kluwer Academic Publishers within the Journal of Automated Reasoning.

This special issue will focus on First-order Theorem Proving as a core theme of Automated Deduction, including:

• theorem proving in first-order classical, many-valued, and modal logics, including:
  • resolution
  • equational reasoning
  • term rewriting
  • model construction
  • constraint reasoning
  • unification
  • description logics
  • propositional logic
  • specialized decision procedures
• strategies and complexity of theorem proving procedures,
• applications of first-order theorem provers, for example to problems in verification, artificial intelligence, mathematics or education.

This special issue welcomes original high quality contributions which have been neither published in nor submitted to any journals or refereed conferences.
The contributions are not limited to those presented at the workshop FTP'2003.

Deepak Kapur, University of New Mexico, Albuquerque, USA

Laurent Vigneron, LORIA - Université Nancy 2, France

• Model-Theoretic Methods in Combined Constraint Satisfiability, by Silvio Ghilardi.
• A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions. I. The Two-Level Case, by Calogero G. Zarba, Domenico Cantone and Jacob T. Schwartz.
• On the Complexity of Deduction Modulo Leaf Permutative Equations, by Thierry Boy de la Tour and Mnacho Echenim.
• MPTP - Motivation, Implementation, First Experiments, by Josef Urban.
• Reachability Analysis over Term Rewriting Systems, by Guillaume Feuillade, Thomas Genet and Valérie Viet Triem Tong.

• Journal of automated Reasoning: http://www.kluweronline.com/issn/0168-7433/
• FTP workshop series: http://www.mpi-sb.mpg.de/conferences/FTP-WS/
• FTP'2003 workshop: http://rewriting.loria.fr/FTP-2003/valencia/
• Rewriting Home Page: http://rewriting.loria.fr/