WEAK
ARITHMETICS
In three years :
To construct
Nonstandard Models of Buss Arithmetic to establish some bounds on the class NP
inter co-NP.
To solve the
problem of existence of end extensions of countable models of bounded collection.
To explore
further the additive theory of infinite sets of prime numbers, both with
absolute results and its links with number theory via the Schinzel's
hypothesis.
To code natural
numbers, complex numbers, and quadratic integers by automata accepting numbers
(written in non-classical systems).
To prove
results for ultra-linear unary recursive schemata (with individual constants).
To obtain
decidability results for S2S[P] theories.
To build formal constructive theories with (from Grzegorczyk hierarchy)
with applications to databases. To investigate the power of counting in very
small complexity classes and in the corresponding logical or arithmetical
settings.
To explore the relation between
Infinite games, automata, and arithmetic.
To study the
fine structure of the BSS recursive enumerable sets.
To investigate
concurrent processes in distributed conveyer systems and their relation with
corresponding weak arithmetics.
To construct
Diophantine representations of recursively enumerable sets of particular
interest.
To show the
cofinality of primes in D0 (P), where P is the function which counts the
primes below x.
To study subsystems of Goodstein’s Arithmetic (without quantifiers).
To develop families of formalized
languages for presenting arithmetical texts.
Weak arithmetic is the study of problems of Number
theory and Computer Science using methods of mathematical logic, just as
Algebraic Number Theory or Analytic Number Theory use Algebra and Analysis.
Weak arithmetic was born in the
1930’s, then really emerged with a famous paper of Julia Robinson in
1949 ; Weak arithmetic has known its most famous result with the
(negative) solution of Hilbert’s tenth problem in 1970 by Yuri Matiyasevich,
and is involving more and more topics.
Works in weak arithmetic are founded
on a common field of mathematical interest, a common set of questions and
logical methods to investigate problems, and
a general culture within computer science. Basically, a scientist
interested in weak arithmetics knows some mathematical logic, likes Peano
Arithmetic and the two Gödel Theorems, works or has been working on decision
problems, on algorithms and their complexities, and uses all kinds of abstract machines.
****
Five of the main sources of results
in weaks arithmetics are undecidability of the field of rational numbers,
Matiyasevich-Davis-Robinson-Putnam theorem, solving Hilbert’s tenth problem,
Erdös-Woods conjecture, Buss arithmetic and study of the real exponential
field.
**
For a first-order structure M, one denotes by DEF(M) the set of constants, functions and relations which are
first-order definable within M.
Following Church and Turing's proof in 1936 that the theory of natural integers
equipped with addition, multiplication, and identity is not decidable, one
obtains a method for proving the undecidability of the theory of a structure M which consists in showing DEF(M) = DEF(N,+, x, =). Julia Robinson
has proved in 1949 than the set N of
natural numbers is definable in the structure (Q,+,x,=), hence undecidability of the first-order theory of the
field of rational numbers. There exist many other results in this vein. At the
origin, these results were important for speculation but now we need analog
result for Computer Science.
**
The most famous questions to have
been solved in the framework of arithmetical definability is Hilbert's tenth
problem; it asks for an algorithm to determine whether a given diophantine
equation has a solution or, in other words whether there exists a program such
that given a polynomial P(x1,
… , xn) with integer coefficients as input, we can say whether
the set of integer solutions of P(x1,
… , xn) = 0 is nonempty. In 1970, Y. Matiyasevich proved the
key-results leading to a negative answer to this problem: exponentiation is definable by a diophantine equation,
i.e. by a S1-formula within Peano Arithmetic. Of course, this
result was obtained after years of research and collaboration with M. Davis, H.
Putnam, J. Robinson who provide many classical theorems and conjectures.
This result has many generalisations
for various number fields. The main question is to know whether there exists a
program such that given a polynomial P(x1,
… , xn) with integer coefficients as input, we can say whether
the set of rational solutions of P(x1, … , xn) = 0
is nonempty. Matiyasevich and his team look at this question thirty years
later.
**
The question of whether first-order arithmetic on the set of nonnegative integers is
definable in terms of the successor function S and the coprimeness
predicate ^ is a typical problem of Weak Arithmetics and perhaps, historically
speaking, one of the first to be posed in this modern framework. It was raised
in 1949 by Julia Robinson in her thesis, when she investigated the
axiomatizability of different theories of elementary structures on numbers.
More precisely, Julia Robinson stated: We
might also try to improve the theorem by replacing divisibility by the relation
of relative primeness. However I have not been able to determine whether x is arithmetically definable in terms of ^ and S or even in terms of ^ and +. This question, and some others of the same
nature such as the definability of all arithmetical relations in terms of
addition and
coprimeness, were neglected for decades. In the eighties, Alan Woods returned
to these problems. He was the first to realize that the question of
definability within mathematical logic is equivalent to the following
conjecture of Number Theory: there is an
integer k such that for every pair (x,y) of integers, the equality x = y holds if and only if x+i and y+i have the same prime
divisors for 0 £ i £ k. This
number-theoretical form of Julia Robinson’s question is itself very closely
linked to some open questions proposed by Paul Erdös and for which he had
conjectured a positive answer. In the book by Richard Guy entilted Unsolved Problems of Number Theory, the
question is attributed to Alan Woods, but due to its close relation with
conjectures of Erdös which were known to A. Woods, it is called the Woods-Erdös conjecture, or WE. This problem has been and is the
subject of works from team 8.
**
Buss arithmetic was introduced by Buss in 1985. He considers a
first-order logical language L(BA)
which contains symbols for successor, addition, multiplication, constant 0,
integer part of x/2, length of x, written in binary form, the function 2|x |.|y |, identity and
natural order. In this language, Buss defines a special induction-schema on
certain subset of formulas providing a Weak Arithmetical theory S such that a subset A of the set N of natural integer is in the complexity class P (we may determine wether an integer
belongs to A in polynomial time) if and only if it is S-provably in NP Ç co-NP. In doing so, Buss provides a promising method to
prove a set A to be in P since, according to this result, it
is sufficient to prove it is both NP
and co-NP in some explicitly known
and specific (weak) theory. Practically, if we know a set is both NP and co-NP, then the method used to prove this result certainly is not
too abstract and the proof can be formalized in such a theory. However, up to
now, no set has been shown in P by
such a method. The main reason is that bounded arithmetics are still not widely
developed. For instance we do not know which classical theorems of Number
Theory are true in these Weak Arithmetics. The length of proof of any classical
theorem increases greatly with weakness of the arithmetical theory in which
this proof takes place. For instance, a proof of Dirichlet theorem on (infinity
of) primes in arithmetical sequences in primitive recursive arithmetic PRA, a result of Cegielski in 1990, is
one hundred pages long. More such results would help to apply Buss'results.
**
Tarski has proved in the 1920’s than
the first-order theory of the structure (R,+,x,=),
where R is the set of real numbers,
is decidable, hence the elementary geometry is decidable. He asks the question
of the status of (R,+,x,exp,=),
where exp is the exponential.
Recently very substantial results about this structure and this question have
been obtained by Wilkie, Macintyre and others : decidability assuming
Shammel’s conjecture, quantifier elimination and « o-minimality ».
The proposed
research consists of five tasks.
Task 1.- Construction of Nonstandard
Models of first-order Arithmetics
The objective
is to construct Nonstandard Models of first-order Arithmetics in order to
investigate:
- 1) which functions and sets cannot
be defined in the Arithmetic axiomatizations of subtheories of Peano Arithmetic
(denoted PA) in which induction schemata are restricted to a special subset of
formulas;
- 2) and what is the algorithmic
complexity of those who can be defined.
This theme is
closely linked, on the one hand, to the study of induction schemata which are
respectively called logarithmic, open, parameter free, Sk-induction, etc. In this theme, logicians try to
construct (nonstandard) models having specific properties (for example an
ordered field without an integer part (Boughattas in 1996)). One tries also to
prove (or disprove) some axiomatizability properties such as the fact that
open-induction in normal rings is not finitely axiomatisable (Boughattas in
1996). Algorithmic Complexity theory is also connected to this theme because
computability in polynomial time corresponds to some specific axiomatisations
one can characterize: for instance P. Pudlak, Takeuti and Krajicek proved the
equivalence between the provability in bounded arithmetic of the collapsing of
the strict polynomial time hierarchy and the finite axiomatizability of this
arithmetical theory in the language of addition, multiplication and x|x|.
Subtask 1-1.- Jean-Pierre Ressayre, Sedki
Boughattas, from team 1, want to
build non standard models of Buss Arithmetic and of related axiom systems. The
aim is to extend the theorem of Buss and to establish some bounds on the class of NP inter co-NP which these theorems
allow to solve in deterministic polynomial time. To this end they start using
non standard models of the structure (R,+,.,exp,=)
and the recent developments about this structure, including those of Ressayre
which rely on formal power series of transfinite length.
Subtask 1-2.- Members of the team 9 will work towards, which was
posed by J. Paris and L. Kirby (1978) and studied by A. Wilkie and J. Paris
(1989). This problem is related to the question whether or not bounded
induction proves the so-called MDRP theorem.
Task 2.- Definability and decidability
of weak substructures of the Standard Model of Peano.
In the present
theme, usually one considers an arithmetical substructure M of the standard model and one tries to prove that either the
whole arithmetical standard model is definable within M, or M is decidable and
in this case we investigate the complexity of the considered structure. This is
not an alternative: there are undecidable weak substructure of Peano where
addition and multiplication are not simulteneously definable and which are
undecidable. Arithmetical definability is closely related to Number Theory and,
in a sense, sheds new light on its classical results. Weak Arithmetics
therefore also include arithmetical decision problems such as decidable
extensions of Presburger (additive) arithmetic and Skolem (multiplicative) arithmetic.
The decision problem for additive prime number theory is adressed both within Number Theory and the Theory of
Automata.
Subtask 2.1.- There are conditional results in
this field (mostly due to A. Woods and M. Boffa) under Shinzel's Hypothesis on
primes. Boffa, from team 7, will
explore further the additive theory of infinite sets of prime numbers and its
links with number theory via the Schinzel's hypothesis. He will investigate the
conjecture that this theory is undecidable in any case. Also there exists
absolute results recently proved by Cegielski, Richard and Vsemirnov. The last
authors (from team 1, team 2 and team 8) and the Ph.D. student Francois Heroult (from team 8) will continue to explore this
way.
Subtask 2.2.- The directions of research of a
part of team 7, in Mons University,
are concerned with extensions and
generalizations of the theories of <N,+>
and <N,£>. In this context, V. Bruyère, A. Maes, C. Michaux,
and F. Point already have obtained definability and decidability results thanks
to codings by finite automata accepting numbers written in non-classical
systems. The coding problem of the addition by an automaton is not completely
settled as well as the relationship between two different systems of numbers.
Extensions to complex numbers and quadatric integers will be considered with a
study of possible axiomatizations of the theories.
Subtask
2.3.- Systems of Diophantine Linear Equations and Applications.
Members of team 5 are going to develop the method of a semi-linear reservoir. Using this
method, the decidability of the problem of equivalence for the meta-linear unary recursive schemata with
individual constants has been
already proved. They plan to prove even more strong result for ultra-linear unary recursive schemata (with individual constants), namely to show that the problem above can be expressed in the
Presburger Arithmetic.
They hope to find new applications of the
decidability of the universal theory of addition and decidability in the
automata theory and schematology. (Namely, for two-way automata with one
finite-turned counter this result
can be generalized to the models connected with the calculations over infinite labeled trees.)
They also plan to obtain results on
undecidability for finite substitutions over regular languages. The equivalence problem of finite
substitutions on regular languages is undecidable (L. Lisovik). They will investigate
this problem over bounded regular languages, for instance over the language ab*c.
Subtask 2-4.- Decidability results for S2S[P]
theories.
Members of team 5 plan to obtain the decidability results for S2S[P]
theories (i.e. for monadic second order arithmetic of two successors with extra unary predicate).
Subtask 2-5.- Formal constructive theories.
Members of team 3 and
Henri-Alex Esbelin, from team 8,
want to develop a
method of building formal constructive theories with the following properties:
1. The task of finding proofs in these theories is tractable ;
2. The algorithms that can be extracted from these proofs belong to some
known small subrecursive classes (from Grzegorczyk
hierarchy) and to some analogs of these
classes for word and tree functions ;
3. with applications to databases.
Also Esbelin, from team 8, searches properties of reals definable by subrecursive
classes, particularly rudimentary reals.
Task 3.- Abstract Machines, Automata
and Words.
Any program in
a specified language which we use in a computer has a corresponding abstract
machine, for instance a Turing machine. Actually, we can formalize any program
because with addition and multiplication we can define (or simulate) all
recursive schemata. Now if we consider
only some Weak Arithmetics (for instance Presburger Arithmetic) then a
corresponding abstract machine computing functions and relations definable in
this theory, or in a model of this one, is of course weaker than a Turing
Machine (for instance it is a finite automaton for Presburger Arithmetic). In
this way, it is natural to associate abstract machines (Finite Automata,
Pushdown Automata, Cellular Automata, Beltiukov Machines, Alternating Turing
Machines, etc) with different weak
arithmetical theories and to the models we investigate.
To this theme
also belong general coding theory and all problems of weak arithmetical
structures consisting of the usual integers with pairing functions (such as
Cantor pairing polynomial) or codings of n-tuples (using for example the
well-known beta-function of Godel). Machines as tools for solving problems of
definability or decidability were used by I. Korec, from Slovakia, A. Bès, V.
Bruyère, C. Michaux, from Belgium, J.E. Pin, J. Tomasik, etc. Machines are not
only tools but are themselves the objects of investigation such as for instance
the Matiyasevich machines introduced to solve problems of trace monoid.
Subtask
3-1.- Ressayre and Finkel, from team
1, want to explore the relation between Infinite games, automata, and
arithmetic. For various classes of machines (for instance push down and blind
counter automata), they study which infinite games accepted by a machine have
winning strategies that can be performed by a machine of the same class. This
has applications to processor synthesis, and to the decidability of extensions
of monadic second order arithmetic.
Subtask
3-2.- BSS model of computation A
part of team 7, explores the Blum,
Shub, and Smale model of computation for which strong links with weak
arithmetics and relative complexity questions were proved (S. Smale, H.
Fournier, P. Koiran). A first research plan is the study of the fine structure
of the BSS recursive enumerable sets. This work was initiated by C. Michaux and
C. Troestler with a characterization of the isomorphism type of these sets. A
second research project is the continuation of the work of J.-S. Gakwaya on the
extension of the Grzegorczyk hierarchy to BSS recursive functions and
relations. Separation of some small classes of complexity for this hierarchy in
relation to the classical open problem for small classes of the Grzegorczyk
hierarchy will be studied. A third theme is related to works of C. Michaux on
the P=NP problem. It is planned to investigate how some notions of classical
complexity for polynomials are related to the P=NP question. This will begin by
a study of some differential structures for the solutions of liouvillian
differential equations (as a part of future PhD work by C. Rivière).
Subtask 3-3.- Yuri Shoukourian and K.
V. Shakhbazyan, from team 4, are in
charge of investigating concurrent processes in distributed conveyer systems
and their relation with corresponding weak arithmetics.
Subtask 3-4.- D. Beauquier and A.
Slissenko, from team 1, will work on
verification of real-time distributed systems in a logical framework in several
directions:
- development of efficient heuristic algorithms for a practical verification
and its implementation (a russian PhD student will work on this topic with a
fellowship given by french government
for a joint supervision) ;
- extension of the logical framework
in order to include the treatment of system’s behavior uncertainty.
Subtask 3-5.- Classification of real functions.
Members of team 5 were going to explore the classification of real functions
according to the type of the memory of "optimal" machines, which
define the functions, particularly, to obtain new results about the connections
between the memory structure of a transducer and differentiability of the
corresponding function. The finite transducers defining the nowhere
differentiable functions and Peano curve with the overlapping coefficient 3
already have been constructed. It has been shown that the class of functions
differentiable on a given interval and defined by a push-down binary transducer
is included in the class of functions linear on the interval. They plan to generalize
this fact to the stack transducers and explore the situation for the k-nested
stack transducers.
Subtask 3-6.- Counting classes
A. Durand (from team 1), H.A. Esbelin and M. More (both from team 8) investigate the power of counting in very small complexity
classes and in the corresponding logical or arithmetical settings. Counting is
a basic natural algorithmic operation, and the counting ability of a small
class of predicates or problems is a good measure of its expressive or
computing power. More precisely, on the one hand, these researchers look for
robust and convenient abstract machine characterizations of closure under
counting of weak arithmetical classes (such as the rudimentary relations). On
the other hand, they also intend to determine logical counterparts of small
complexity classes involving counting (such as #TC0, the closure under counting of the class of
circuits families with bounded height with majority gates). Finally, they study
the possible closure of various weak arithmetical classes under various
weakened forms of counting (eg. modular counting).
Subtask 3-7.- Jerzy Tomasik and Malika More,
from team 8, will investigate
methods from classical model theory, fusion theory and multihead automata in
order to improve some lower bounds in circuit complexity and examine their
links with small
complexity classes.
Subtask 3-8.- Purposes of members of team 2 is
1) To study definability and
decidability problems for weak theories of integers and polynomial rings. For
this purpose both number-theoretic and logical methods will be used
(Vsemirnov).
2) To construct Diophantine
representations of recursively enumerable sets of particular interest
(Vsemirnov, Matiyasevich).
3) To study properties of sets of
pseudoprimes defined by formulas with small number of quantifiers (Eterevsky).
4) To construct universal
self-delimiting exponential Diophantine equation; such equations are of
interest in algorithmic infomation theory developed by G. J. Chaitin
(Matiyasevich).
Task 4.- Elementary proofs of classical
Number Theory results.
Arithmetical
Proof Theory stems from the work Erdös and Selfridge who were the first to ask
for what they called elementary proofs (i.e. in the framework of real analysis
instead of complex analysis) of results such as the Dirichlet Theorem on the
infinity of primes in arithmetical sequences. Logicians such as Takeuti,
Kreisel and Simpson (with his reverse mathematics) have contributed to the
subject but in a general way. P. Cegielski and O. Sudac have constructed proofs
for specific classical theorems (such as the Prime Number Theorem of De La
Vallée Poussin). They have also
constructed some first order denumerable structures modelling a version
of Peano Analysis to provide proofs within Peano Arithmetic models or even
within the standard model of weaker arithmetical theories (e.g. PRA, the
Primitive Recursive Arithmetic). It is clear that this work should be continued
in order to strengthen the tools developed by Buss.
Subtask 4-1.- Let D0 be the subsystem of Peano Arithmetic (PA) where induction is applied only to
formulas with bounded quantifiers. It is well known that in D0 the exponential function is not provably total. This
is the main obstacle in reproducing elementary number theory in D0, whose interest is motivated by its connections with
complexity theory.
The study of
classical results of number theory in D0 requires a
fine analysis of the classical proofs and gives many computational information.
In some cases new proofs are required and functions of exponential growth are
substituted by some combinatorial principles of pigeon hole type. This
principle is available in the theory D0 + W1, where the axiom W1 guarantees the
totality of the function xlog2 y. The
following classical results where proved in th D0 + W1:
1) cofinality
of primes, proved by Woods ;
2) Lagrange’s
theorem, proved by Berarducci and Intrigila;
3) existence
and uniqueness of an extension of every finite degree for a residue field of a
model of D0 + W1, proved by
D'Aquino and Macintyre.
Team 6 and team 9
plan to improve Woods result by showing the cofinality of primes in the system
theory D0 (P) which is
obtained by adding a new function symbol P to the
language of arithmetic (which has to be thought as the function which counts
the primes below x) and considering D0 -induction in
the expanded language. A partial result towards proving the conjecture is due
to Cornaros (1996).
The quadratic
reciprocity law is one of the most celebrated theorems of classical number
theory. There exist many proofs of this classical result but all of them seem
to require functions which grow exponentially. Analysis of Gauss'second proof,
in which he uses quadratic forms of given discriminant and finiteness of class
number, is under way. For primes p,q
equiv 3 (mod 4) we have already a proof in D0 + W1. It appears one can obtain a local result relating
correctness of quadratic reciprocity law for p,q to solvability of Pell
equation x2 – d.y2 =1,where d is one of p,pq, or a small
multiple of them.
In connection
with 3) above team 6 plan to study
curves over residue fields of models of D0 + W1, in order to show that they are pseudofinite, i.e.
perfect, they have a unique extension of each degree and every absolutely
irreducible curve has a point in it. (This was proved by Macintyre for residue
fields of models of PA.) In this
context we plan also to study Chevalley theorem over models of D0 or D0 + W1.
Subtask 4-2.- Subsystem and Modifications of
Goodstein’s Arithmetics; their application to the Logical Programming
The objective
is the study of subsystems of R.L.Goodstein’s Arithmetic (without quantifiers)
based on the A.Grzegorczyk’s scheme of bounded recursion and on the modified
scheme of bounded recursion relating to the words in a fixed alphabet, the
study of the arithmetical systems based on the corresponding classes of
functions and predicates with some restrictions to the induction scheme, the
comparison of the possibilities of such systems and of the complexity of
logical deductions in them, the comparison of these systems with the systems
based on the rudimentary and s-rudimentary predicates of R.M. Smullyan, the
study of corresponding systems of Logical Programming, and the study of the
modifications of these systems based on many-valued logic.
Team
4 and Esbelin, from team
8, are in charge of this task
Task 5.- Weak arithmetics, Pure and
Computational Logic.
Subtask 5-1.- Nezondet's p-destinies.
It is mainly concerned with
Nezondet's p-destinies which are a
general tool founded on trees for deciding closed sentences within theories
consisting of a set of sentences in a relational language which have a bounded
number of quantifiers. When applied to weak arithmetical theories, this
promising new method gives rise to many interesting new questions in Number
Theory (M. Guillaume, JeLei Yin, D. Richard). In addition, the computation of a
p-destiny, when successfully carried out, effectively generates a finite
structure, namely a set of labelles trees. This structure exactly encodes the
necessary and sufficient information for deciding the sentences of the
considered theory. The decision algorithms such obtained are expected to be
efficient and useful in databases theory as well as in descriptive complexity.
Denis Richard and Annie Château, from team
8, intend to develop the applications of p-destinies to weak arithmetical
theories, as well in its number theoretic implications as in its connexions
with theoretical Computer Science.
Subtask 5-2.- Computational Logic.
Members of team 5 and K. Verchinine, from team
1, will investigate:
- development of families of
formalized languages for presenting mathematical texts in a form the most
appropriate for a user: the languages must be used as tools to write and verify mathematical publications and as the
universal interfaces of declarative mathematical knowledge;
- formalization
and evolutionary development of computer-made prover: computer-oriented sequent
methods will be constructed for classical and intuitionistic logics, which will
be reflect linguistic peculiarities of declarative mathematical knowledge and
will use results of Computational Logic and Arithmetic; these methods should
satisfy the following requirements: syntactical form of the initial problem
should be preserved; deduction should be done in the signature of initial
theory, proof search should be goal oriented, definition and lemma applications
should be incorporated in deductions as unique rules, equality handling should
be separated from deductive processes;
- combining
deduction steps with arithmetical calculations and symbolic transformations.
Of course normal discussions from distant members of
different teams will be by e-mail but we expect a workshop every year to
present results and, mainly, lively discussions. Normal dissemination will
consist of papers in reviews (Journal of
Symbolic Logic, Theoretical Computer
Science, Annals of Pure and Applied
Logic…). Also we expect to publish communications either in a special issue
of a review or as a Lecture Note in
Mathematics (Springer).
TEAM 1: Université de Paris (France)
Indeed
`université de Paris’ is used for three universities. Members are Patrick Cegielski, Danièle Beauquier, Anatole Slissenko,
and Konstantin Verchinine,
Professors at université Paris XII, Arnaud Durand
and Tristan Crolard, lecturers at
université Paris XII, Irène Guessarian,
Professor at université Paris VI, Jean-Pierre Ressayre, Directeur de
recherche (analog of Professor at CNRS) at université Paris VII, Serge Grigorieff, Professor at université
Paris VII, Sedki Boughattas,
lecturer at université Paris VII, Olivier Finkel,
Eugenio Chinchilla, and A. Rambaud, from université Paris VII.
Team 1 is
involved in subtasks 1-2, 2-1, 3-1, 3-4, 3-6, and 5-2.
TEAM 2: Saint-Petersburg (Russia)
Members are Yuri Matiyasevich
(doctor of science) and Maxim Vsemirnov (candidate, researcher, born in 1972), from Steklov
Institute of Mathematics at St.Petersburg, Russia, and Oleg Eterevsky, student at St.Petersburg
State University, born in 1981.
Team 2 is
involved in subtasks 2-1 and 3-8.
TEAM 3:
Udmurt University (mathematics faculty, software chair), Russia.
Members are Anatoly Petrovich Beltiukov, Professor, Vyacheslav Viktorovich
Pupyshev, born in 1970, senior
lecturer, Tatiana Gennadievna Azhimova,
born in 1964, senior lecturer, and Evgeny Valerievich Fadeev, born in 1977, postgraduate student.
Team 3 is involved in subtask 2-5.
TEAM 4: Yerevan (Armenia)
Members are
Yuri Shoukourian, doctor of
sciences, Professor, head of department, director of IIAP (Institute for
Informatics and Automation Problems), Igor Zaslavsky,
doctor of sciences, Professor, head of department, deputy director of IIAP,
Karine Shakhbazyan, candidate of
sciences, senior scientific researcher at IIAP, Mikael Khachatryan, candidate of sciences, senior scientific researcher at
IIAP, Seda Manukian, candidate of
sciences, senior scientific researcher at IIAP, Vahagn Khachatryan, born in 1978, post-graduate student (magistrant) at
Yerevan State University, junior scientific researcher at IIAP, and Karen Hambartzumyan, born in 1972, candidate
of sciences, junior researcher at IIAP.
Team 4 is
involved in subtasks 3-3 and 4-2.
TEAM 5: Kiev (Ukraine)
TEAM 6: Naples (Italy)
Members are
Paola D’Aquino, senior researcher at
Second University of Naples, Alessandro Berarducci,
Professor at University of Pisa, Domenico Zambella,
senior researcher at University of Torino, and Andrea Vietri, graduate student at University of Roma, "La
Sapienza" (31 year old).
Team 6 is
involved in subtask 4-1.
TEAM 7: Université de Mons-Hainaut (Belgium)
Members are Maurice Boffa, Véronique Bruyère, and Christophe Troestler
(29 year old), both Professor at université de Mons, Christian Michaux, associate Professor, Francoise
Point, Senior Research Associate,
Jean-Sylvestre Gakwaya (29 year old)
and Arnaud Maes (27 year old), both
Post-Doctoral researcher, and Cédric Rivière
(22 year old), PhD Student.
Team 7 is involved in subtasks 2-1,
2-2, and 3-2.
TEAM 8: Université de Clermont-Ferrand (France)
Members are Denis Richard
(Professor), Jersy Tomasik (senior
lecturer), Henri-Alex Esbelin
(lecturer), Malika More (lecturer),
Annie Château, and François Heroult.
Team 8 is
involved in subtasks 2-1, 5-1, 2-5, 3-6, 3-7, and 4-2.
TEAM 9: University of Athens (Greece)
Members are Constantinos Dimitracopoulos,
Associate professor at University of Athens, Michael Mytilinaios, Associate professor at Athens University of Economics
and Business, Thanases Pheidas,
Associate professor at University of Crete, Konstantinos Hatzikiriakou, Assistant professor at University of Thessaly,
Charalampos Cornaros, Researcher at
University of Athens, and Chrysovalantis Verykios,
Graduate student at University of Athens, born in 1974.
Team 9 is involved in subtasks 1-2
and 4-1.
1. Danièle Beauquier and Anatole Slissenko, A., A First Order Logic for Specification of Timed Algorithms: Basic
Properties and a Decidable Class, to appear in Annals of Pure and Applied Logic.
2. Sedki Boughattas, L'induction ouverte dans les anneaux discrets ordonnés et normaux n'est pas finiment axiomatisable
(French) [Open induction in ordered and normal discrete rings is not finitely
axiomatizable], J. London Math. Soc.
(2) 53 (1996), no. 3, 455-463.
3. Patrick Cegielski, Definability, decidability and complexity,
Annals of Mathematics on Artificial
Intelligence 111, 1996, pp.
311-341.
4. Eugenio Chinchilla, A model of R_2_# inside a subexponential time resource, Notre Dame J. Formal Logic 39 (1998),
no. 3, 307-324.
5. Arnaud Durand, Claus Lauteman, and Thomas
Schwentick, Subclasses of Binary-NP, Journal of Logic and Computation, vol.
8(2), 1998, pp. 189-207.
6. Olivier Finkel and Jean-Pierre Ressayre, Stretchings,
J. Symbolic Logic 61 (1996), no. 2,
563-585.
7. Jean-Pierre Ressayre, Polynomial time
uniformization and non-standard methods,
Ann. Math. Artificial Intelligence 16 (1996), no. 1-4, 75-88.
See also joint works in team 2 (papers 4, 7, 8)
and 8 (papers 1, 2).
1. M.A. Vsemirnov, Infinite sets of primes that admit
Diophantine representations in eight
variables, Zapiski Naychnukh
Seminarov POMI, 220 (1995), pp. 36-48. (in Russian).
English translation: Journal of
Mathematical Sciences. 87 (1997), no.1, pp. 3200-3208.
2. M.A. Vsemirnov, Diophantine
representations of linear recurrent sequences. I, Zapiski Naychnukh
Seminarov POMI, 227 (1995), pp. 52-60. (in Russian). English translation: Journal of Mathematical Sciences, 89
(1998), no.2, pp.1113-1118.
3. M.A. Vsemirnov, Diophantine
representations of linear recurrent sequences. II,
Zapiski Naychnukh Seminarov POMI,
241(1997), pp.5-29. (in Russian). English translation: Journal of Mathematical Sciences.
4. Patrick Cegielski, Denis Richard, and Maxim A. Vsemirnov, On the
additive theory of primes. LLAIC, Universite d'Auvergne - Clermont 1, Preprint
No. 78 (1999), to appear in The
Journal of Symbolic Logic.
5. M.A. Vsemirnov, Woods-Erdos conjecture for polynomial
rings, to appear in Annals
of Pure and Applied Logic.
6.
Yu. Matiyasevich, A new technique for
obtaining Diophantine representations via elimination of bounded universal
quantifiers, Zapiski Nauchnykh
Seminarov POMI, vol. 220, pp. 83-92, 1995.
7. Patrick Cegielski, Yuri Matiyasevich, and Denis Richard, Definability and decidability issues in
extensions of the integers with the divisibility predicate, The Journal of Symbolic Logic, vol.
61, June 1996, pp.515-540.
8. Luc Boasson, Patrick Cegielski, Irène Guessarian, and Yuri Matiyasevich, Window-Accumulated Subsequence matching
Problem is linear, PODS’99 (Principle Of Databases Systems), ACM Press, pp. 327-336.
9. Yuri Matiyasevich, Hilbert's tenth
problem: A two-way bridge between number theory and computer science, People and Ideas in Theoretical Computer
Science, C. S. Calude, editor, Springer-Verlag, Singapore, 1999, pp.
177-204.
10. Maurice Margenstern and Yuri Matiyasevich, A binomial representation of the 3x+1 problem, Acta Arithmetica, vol. XCI.4, 1999, pp. 367-378.
1. A.P. Beljtjukov, Tractable
tasks of deductive algorithms synthesis, Abstracts of second international conference "Mathematical algorithms",
NNSU publishers, Nizhni Novgorod, 1995, pp.9-10.
2. A.P. Beljtjukov, Word stack register
machines, Logic Colloquium'95
Abstracts, Finite Model Theory and Computer Science, Haifa, Technion, 1995,
p.31.
3. A.P. Beljtjukov, Hierarchy of Small
Subrecursive Classes Based on Bounded Simultaneous Recursion, Logic Colloquium'96,
San-Sebastian,1996, p. 98.
4. A.P. Beltiukov, Hierarchy of Small
Subrecursive Operator Classes Based on Bounded Recursion, Logic Colloquium'97, University of
Leeds, 6th-13 July, 1997, Abstracts, 1997, p.11.
5. A.P. Beltiukov, Intuitionistic formal
theories with realizability in subrecursive classes, Annals of Pure and Applied Logic, 89, 1997, p. 3-15.
6. A.P. Beltiukov, One-way
one-dimensional cellular automata and small subrecursive classes, Proceedings of JAF'15 (Fifteenth Days
of Weak Arithmetic), University of Mons-Hainaut, December 11-12, 1997, Mons,
Belgium, 1998, pp. 21-27.
7. A.P. Beltiukov, Alternating time complexity
bounds for protothetics, Logic
Colloquium'98 The 1998 ASL European Summer Meeting, August 9-15, 1998,
Prague, Chech Republic, 1998, p.81.
8. A.P. Beltiukov, Smullyan Rudimentary
Predicates and Skolem Elementary Functions on Trees, Logic Colloquium 2000, Paris 2000.
TEAM 4
1. Y. Shoukourian and K. Schakbazyan, On the recognition of languages in free
semilattices, Kibernetika, vol.
2, Kiev, 1996, pp. 179-182.
2. Y. Shoukourian, Parallelization of Automata, Cybernetics and System Analysis, vol.
34, n° 4, 1998, pp. 540-544 [translation of Kibernetika I Sistemnyi Analiz, n° 4, pp. 78-84].
3. Y. Shoukourian and K. V.
Shakhbazyan, On process Languages in
Finite Graphs, Proceedings of Sci.
Seminar of Petersburg Branch of Math. Institute, vol. 248, 1998, pp. 205-215.
4. Y. Shoukourian and K.
Shakhbazyan, Distributed Conveyor
Processing of Data Streams, Proceedings
of the Conference CSIT-99, Yerevan, 1999, pp. 9-12.
5. I.D. Zaslavsky, Dual realizability in symmetric logic,
to appear in Annals of Pure and Applied
Logic.
6. I.D. Zaslavsky, On the theory of
constructive reducibility, Proceedings of Intern. Conference on Computer
Science and Information Technologies (CSIT`97),
Yerevan, pp.10-11 (1997).
7. I.D.
Zaslavsky, The realization of three-valued
logical functions by recursive and Turing operators, Selecta Mathematic Sovetica, Vol.7, N1, Birkhäuser Verlag, pp.
15-22 (1988).
8.
I.D.Zaslavsky, On logically but not
functionally complete calculus in three-valued logic, The Tbilisi Symposium
on Logic, Language and Computation, Selected papers, CSLI Publications, Stanford, California, pp.309-313 (1998).
9. M.A.
Khachatryan, Sequent calculus with
restricted antecedent and succedent, Proceedings of the Intern. Conference
on Comp.Science and Informational Technologies (CSIT’97), Yerevan, pp.12-14 (1997).
10.
S.N.Manukian, On the structure of the
recursive enumerable fuzzy sets, Proceedings of IIAP of National Acad. Sci. Armenia and Yer. State
University, vol.17, pp.86-91 (1997). (in Russian).
1. Lyaletski, A., A sequent formalism and deductive systems
for 1st-order classical logic, Proc.
of Intern. Conf. ``Logic and Applications'', Novosibirsk, Russia (2000).
2. A. Lyaletski and M. Morokhovets, On
principles of proof search and
construction of mathematical knowledge bases in the Evidence, Algorithm, Proc. of the International Congress
IMACS'2000, Switzerland, 2000.
3. A. Lyaletski and M. Morokhovets, On linguistic aspects of integration of
computer mathematical knowledge, CALCULEMUS Workshop, Trento, Italy, 1999,
Elsevier, Electronic Notes in
Theoretical Computer Science, vol. 23, issue 3, 1999, p. 165-178.
4. A.I. Degtyarev, A.V. Lyaletski, and M.K. Morokhovets, On the EA-style integrated processing of self-contained mathematical
texts, Proc. of the International Workshop CALCULEMUS'2000, Great Britain, 2000.
5. A.I. Degtyarev, A.V. Lyaletski, and M.K. Morokhovets, Evidence Algorithm and Sequent Logical Inference Search, Springer, Lecture Notes in Artificial Intelligence,
Vol.1705, 1999, pp.44-61.
6. A.I. Lyaletski, On Herbrand theorem, Proc. of the European Congress of the
Association for Symbolic Logic of the millennium, Sorbonne, Paris, 2000, to
appear in Bulletin of Symbolic Logic.
7. L.P. Lisovik, Hard sets methods and semilinear reservoir
method, with application (Review), Springer, Lecture Notes in Computer Science, Vol. 1099, 1996, pp. 219-231.
8. L.P. Lisovik, Nondeterministic systems and finite
substitutions on regular laguages, Bulletin
of European Association for Theoretical Computer Science, v. 63, 1997, pp.
156-160.
9. J. Karhumaki and L.P. Lisovik, On the equivalence of finite substitutions
and transducers, Jewels are Forever (dedicated to the 65th anniversary of A.
Salomaa), Springer, 1999, pp. 97-108.
10. L.P. Lisovik and O.Yu.
Shkaravskaya, On the Real Functions
Defined by Transducers, Kibernetika
i Sistemny Analiz, No 1, 1998, pp. 82-93.
TEAM 6
1. Alessandro Berarducci and
Benedetto Intrigila, Linear recurrence
relations are D0-definable, Logic and Foundations of Mathematics,
Selected contributed papers, LMPS '95
(A.Cantini, E.Casari, P.Minari editors), Kluwer Academic Publishers, Dordrecht,
The Netherlands, 1999, 67-81.
2. Alessandro Berarducci, Factorization in generalized power series,
Transactions of AMS, Vol. 352, N. 2
(1999) 553-557.
3. Alessandro Berarducci and
Margarita Otero, Intersection theory for
o-minimal manifolds, to appear in Annals
of Pure and Applied Logic.
4. Paola D’Aquino, Towards the limits to the Tennenbaum
phenomenon, Notre Dame Journal of Formal
Logic, 38, 1997, pp. 81-92.
5. Paola D’Aquino, Solving Pell equations locally in models of
ID0, Journal of
Symbolic Logic, vol 63, 1998, pp. 402-410.
6. Paola D’Aquino and Angus
Macintyre, Non standard finite fields
over ID0+W1, Israel
Journal of Mathematics 117 (2000), pp. 311-333.
7. Paola D’Aquino, Quotient fields of a model of ID0+W1, to appear in Mathematical
Logic Quarterly.
8. D. Zambella, Foundation versus induction in Kripke-Platek set theory, Journal of Symbolic Logic 63 (1998),
no.4, pp. 1399-1403.
9. D. Zambella, End extensions of models of linearly bounded
arithmetic, Annals of Pure and Applied Logic 88 (1997), no.2-3, pp.
263-277.
10. D. Zambella, Algebraic methods and bounded formulas, Notre Dame J. Formal Logic 38 (1997),
no. 1, pp. 37-48.
TEAM 7
1. M. Boffa, More on a undecidability result of Bateman, Jockusch and Woods, Journal of Symbolic Logic 63 (1998), p.
50.
2. A. Maes, An automata theoretic
decidability proof for the first-order theory of <N;<,P> with morphic
predicate P, Journal of Automata,
Languages and Combinatorics, 4 (1999), p. 229-245.
3. A. Maes, Revisiting Semënov's results
about decidability of extensions of Presburger Arithmetic, Definabillity in Arithmetics and
Computability, Cahiers du Centre de Logique 11 (2000) p. 11-59.
4. V. Bruyère and G. Hansel, Bertrand numeration systems and
recognizability, Theoret. Comput.
Sci. 181 (1997) 17-43.
5. S. Ben-David, K. Meer, and C. Michaux, A
note on Non-Complete Problems in NPR, The
Journal of Complexity 16 (2000), p. 324-332.
6. J.-S. Gakwaya, Extended Grzegorczyk's Hierarchy in the BSS
model of computability, FoCM'97,
F. Cucker - M. Shub Eds, Springer Verlag (1997), p. 127-151.
7. C. Michaux and R. Villemaire, Presburger arithmetic and recognizability
of sets of natural numbers by automata: New proofs of Cobham's and Semenov's
theorem, Annals of Pure and Applied
Logic 77 (1996), p. 251-277.
8. C. Michaux and C. Troestler, Isomorphism Theorem for BSS Recursively
Enumerable Sets over Real Closed Fields, Theoretical Computer Science 231 (2000), 253-273.
9. F. Point and V. Bruyère, On the
Cobham-Semenov theorem, Theory
Computer Systems, 30 (1997), p. 197-220.
10. F. Point, On decidable extensions of
Presburger arithmetic: From A. Bertrand numeration systems to Pisot numbers,
to appear in J. Symb. Logic.
1. Patrick Cegielski and Denis
Richard, Decidability of natural integers
equipped with Cantor pairing function and successor, to appear in Theoretical Computer Science.
2. Patrick Cegielski and Denis
Richard, On arithmetical first-order
theories allowing encoding and decoding of lists, Theoretical Computer Science, vol. 222, 1999, pp. 55-75.
3. Henri-Alex Esbelin, Counting
modulo semi-groups, to appear in
Theoretical Computer Science.
4. Henri-Alex Esbelin and Malika More, Rudimentary
relations and primitive recursion : a toolbox, Theoretical Computer Science 193 (1998) 129-148.
5. M. Kokar and Jerzy Tomasik, Towards
a goal-driven autonomous fusion system,
Proc. International Conference on Information Fusion FUSION'99 July 6-8, 1999, Sunnyvale, CA (Org. NASA, IEEE, ISIF)
Vol. 1, pp. 148-153.
6. M. Kokar, Jerzy Tomasik, and J. Weyman, A
formal approach to information fusion, Proc. International Conference on
Information Fusion FUSION'99 July
6-8, 1999, Sunnyvale, CA (Org. NASA, IEEE, ISIF) Vol. 1, pp. 133-142.
7. Rémy Malgouyres and Malika More, On
the computational complexity of basic problems of 2D digital topology, to
appear in Theoretical Computer Science.
8. Malika More and Frédéric Olive, Rudimentary
languages and second-order logic, Mathematical
Logic Quarterly 43 (1997) 419-426
9. Jerzy Tomasik, Discrete Dynamic
approach to multisensory multirack fusion, Proc. AeroSense'2000, April 25-28, 2000, Orlando, Florida, Vol. 4051, pp.
369-379.
TEAM 9
1. Ch. Cornaros, On Grzegorczyk induction,
Annals of Pure and Applied Logic 74
(1995), 1-21.
2. Ch. Cornaros & C.
Dimitracopoulos, A note on end extensions,
Arch. Math. Logic 39 (2000), 459-463.
3. K. Hatzikiriakou, WKL0 and Stone's separation
theorem for convex sets, Ann. Pure Appl. Logic 77 (1996), 245-249.
4. M. J. Groszek, M. E. Mytilinaios
& T. A. Slaman, The Sacks Density
Theorem and S2-Bounding, J. Symbolic Logic 61 (1996), 450-467.
5. M. E. Mytilinaios & T. A.
Slaman, On a question of Brown and Simpson,
in "Computability, Enumerability, Unsolvability. Directions in Recursion
Theory", Cambridge University Press, 1996, 205-218.
6. L. Lipshitz & Th. Pheidas, An analogue of Hilbert's Tenth Problem for
p-adic functions, J. Symbolic Logic
60 (1995), 1301-1309.
3.1.6 Management
Main exchanges
are by e-mail but we plan two workshops (a local one and a general) by year,
two co-ordination meeting and exchanges of scientists (already are planned
visits of a student of team 2 and one of team 5 in team 1).
Tasks
|
Teams
|
Months
1-6
|
Months
7-12
|
Months
13-18
|
Month
19-24
|
Months
25-30
|
Months
31-36
|
||||
|
|
|
|
|
|
|
|
|
||||
T1.1
|
Team 1
|
|
|
|
|
|
|
||||
T1.2
|
Team 9
|
|
|
|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
||
T2.1
|
Team 7,1,2,8
|
|
|
|
|
|
|
||||
T2.2
|
Team 7
|
|
|
|
|
|
|
||||
T2.3
|
Team 5
|
|
|
|
|
|
|
||||
T2.4
|
Team 5
|
|
|
|
|
|
|
|
|||
T2.5
|
Team 3,8
|
|
|
|
|
|
|
||||
|
|
|
|
|
|
|
|
|
||||
T3.1
|
Team 1
|
|
|
|
|
|
|
||||
T3.2
|
Team 7
|
|
|
|
|
|
|
||||
T3.3
|
Team 4
|
|
|
|
|
|
|
||||
T3.4
|
Team 1
|
|
|
|
|
|
|
||||
T3.5
|
Team 5
|
|
|
|
|
|
|
||||
T3.6
|
Team 1,8
|
|
|
|
|
|
|
||||
T3.7
|
Team 8
|
|
|
|
|
|
|
||||
T3.8
|
Team 2
|
|
|
|
|
|
|
||||
|
|
|
|
|
|
|
|
|
||||
T4.1
|
Team 6,9
|
|
|
|
|
|
|
|
|||
T4.2
|
Team 4,8
|
|
|
|
|
|
|
|
|||
|
|
|
|
|
|
|
|
|
|
|||
T5.1
|
Team 8
|
|
|
|
|
|
|
|
|||
T5.2
|
Team 5,1
|
|
|
|
|
|
|
|
|||
3.1.7 SUMMARY
Weak arithmetic is the study of problems of Number theory and
Computer Science using methods of mathematical logic, just as Algebraic Number
Theory or Analytic Number Theory use Algebra and Analysis. Five of the main
sources of results in weaks arithmetics are undecidability of the field of
rational numbers, Matiyasevich-Davis-Robinson-Putnam theorem, solving Hilbert’s
tenth problem, Erdös-Woods conjecture, Buss arithmetic and study of the real
exponential field.
The proposed project is constituted
of nine teams from university of Paris, Steklov Institute of Mathematics at
Saint-Petersburg (Russia), Udmurt University (Russia), Institute for
Informatics and Automaton Problems at Yerevan (Armenia), Kiev University
(Ukraine), University of Naples (Italy), university of Mons-Hainaut (Belgium),
university of Clermont-Ferrand (France), and University of Athens (Greece).
Objectives for the three years
were : to construct Nonstandard Models of Buss Arithmetic to establish
some bounds on the class NP inter co-NP ; to solve the problem of
existence of end extensions of countable models of bounded collection ; to
explore further the additive theory of infinite sets of prime numbers, both
with absolute results and its links with number theory via the Schinzel's
hypothesis ; to code natural numbers, complex numbers, and quadratic
integers by automata accepting numbers (written in non-classical
systems) ; to prove results for ultra-linear unary recursive schemata
(with individual constants); to obtain decidability results for S2S[P] theories ; to build formal constructive
theories with (from Grzegorczyk hierarchy) with applications to
databases ; to investigate the power of counting in very small complexity
classes and in the corresponding logical or arithmetical settings ; to
explore the relation between Infinite games, automata, and arithmetic ; to
study the fine structure of the BSS recursive enumerable sets ; to
investigate concurrent processes in distributed conveyer systems and their
relation with corresponding weak arithmetics; to construct Diophantine
representations of recursively enumerable sets of particular interest ; to
show the cofinality of primes in D0 (P), where P is the function which counts the
primes below x ; to study subsystems of Goodstein’s Arithmetic (without
quantifiers) ; to develop families of formalized languages for presenting
arithmetical texts.
Main exchanges are by e-mail but it is planning two workshops (a local
one and a general) by year, two co-ordination meeting and exchanges of
scientists.