The Computational Complexity of Logical Theories
- PDF / 6,549,860 Bytes
- 252 Pages / 461 x 684 pts Page_size
- 57 Downloads / 198 Views
718 Jeanne Ferrante
Charles W. Rackoff
The Computational Complexity of Logical Theories
Springer-Verlag Berlin Heidelberg New York 1979
Authors Jeanne Ferrante Automatic Programming Group IBM T. J. Watson Research Center Box 218 Yorktown Heights, NY 10598 USA Charles W. Rackoff Department of Computer Science University of Toronto Toronto, Ontario Canada M5S 1A?
A M S Subject Classifications (1970) 02 B10, 02F10, 0 2 G 0 5 , 6 9 A 2 0 , 68A40 ISBN 3-540-09501-2 Springer-Verlag Berlin Heidelberg NewYork ISBN 0-38?-09501-2 Springer-Verlag NewYork Heidelberg Berlin Library of Congress Cataloging in Publication Data Ferrante, Jeanne,1949- The computational complexttyof logical theories. (Lecture notes in mathematics ; 718) Bibliography: p. Includes index. 1. Predicate calculus. 2. Computational complexity. I. Rackoff, Charles W., 1948- joint author. II. Title. III. Ser~es: Lecture notes in mathematics (Berlin) ; 718. QA3.L28 no. 718 [QA9.35] 510'.8s [511'.3] 79-15338 This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically those of translation, reprinting, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under § 54 of the German Copyright Law where copies are made for other than private use, a fee is payable to the publisher, the amount of the fee to be determined by agreement with the publishel © by Springer-Verlag Berlin Heidelberg 1979 Printed in Germany Printing and binding: Beltz Offsetdruck, Hemsbach/Bergstr. 2141/3140-543210
PREFACE Since
the early
been i n t e r e s t e d predicate true
in decision
calculus.
about a particular
the first
early of
decision
validity
of
the integers
wasn't
t o have f o r m a l
theory
multiplication
let
until
necessary
order
alone
is
result of the is
concept sets
sets.
notions
integers
or t h e s e t class
in
set of
the
sentences true
of structures.
was L ~ w e n h e i m ' s
for
have
of sentences
One o f
procedure
calculus.
the first-order
has e x i s t e d
for
some t h e o r i e s
thirties
that
time,
it
of computation,
Kleene,
Another theory
It
to
was f i r s t
as p r o v i d e d
Post and T u r i n g .
At the present
be
was p o s s i b l e
famous theorem t h a t
was f e l t it
the difficulty
the sixties
might
by t h e
The f i r s t the first-
of addition
and
t i m e an enormous
results
are
known;
these results.
than that
a long
it
such c o n j e c t u r e s .
and u n d e c i d a b i l i t y
investigating
was i n
that
u n d e r the o p e r a t i o n s
a good s u r v e y o f
of comparing
It
prove,
was G ~ d e l ' s
about a theory
have s t a r t e d
the
not decidable.
For a l o n g stronger
we mean t h e
procedure
such as C h u r c h ,
number o f d e c i d a b i l i t y [ELTT65]
theories
t h e monadic p r e d i c a t e
some p e o p l e f e l t
state,
undecidability
in
logicians
under addition.
it
people
for
procedur~ discovered
ca
Data Loading...
