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).
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
- equational reasoning
- term rewriting
- model construction
- constraint reasoning
- 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
This special issue welcomes original high quality contributions which have
been neither published in nor submitted to any journals or refereed
The contributions are not limited to those presented at the workshop
Editors of this special issue
University of New Mexico, Albuquerque, USA
LORIA - Université Nancy 2, France
The following papers have been accepted for this special issue that should
appear at the end of 2004.
- 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
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.
Last modified: 24-Mar-2005