Search

The first collection of Leibniz's key writings on the binary system, newly translated, with many previously unpublished in any language. The polymath Gottfried Wilhelm Leibniz (1646–1716) is known for his independent invention of the calculus in 1675. Another major—although less studied—mathematical contribution by Leibniz is his invention of binary arithmetic, the representational basis for today's digital computing. This book offers the first collection of Leibniz's most important writings on the binary system, all newly translated by the authors with many previously unpublished in any language. Taken together, these thirty-two texts tell the story of binary as Leibniz conceived it, from his first youthful writings on the subject to the mature development and publication of the binary system. As befits a scholarly edition, Strickland and Lewis have not only returned to Leibniz's original manuscripts in preparing their translations, but also provided full critical apparatus. In addition to extensive annotations, each text is accompanied by a detailed introductory “headnote” that explains the context and content. Additional mathematical commentaries offer readers deep dives into Leibniz's mathematical thinking. The texts are prefaced by a lengthy and detailed introductory essay, in which Strickland and Lewis trace Leibniz's development of binary, place it in its historical context, and chart its posthumous influence, most notably on shaping our own computer age.

It is trite but true: We are in the middle of an information revolution. News, gossip, entertainment, lies, and propaganda move over huge distances in the blink of an eye. All of it, from the newspapers of record to juvenile cell phone photos, to what you bought at the supermarket last Th ursday, is archived for parties unknown to retrieve, who knows when in the future. Electronic communication already reaches the majority of the world’s population, and no technological obstacle prevents virtually everyone from having constant access to everything. In parts of the world where connectivity is lagging because cables are few and electricity is scarce, mobile communication is growing exponentially (see, for example, the statistics of the International Telecommunications Union at http:// www .itu .int/ ITU -D/ ict/ statistics/ ict/ ). If the world is not fully connected in twentyfi ve years, it will not be for want of technology or money, but because of politics. Th e question before this human generation is how the power of information ubiquity will be used and how it will be controlled. Th e societies of the world are struggling with the social dilemmas posed by the rapidly evolving technologies. Con ve niences that teenagers take for granted— for example, taking photographs anywhere and sending them instantaneously to anyone on earth— neither science fi ction writers nor engineers quite foresaw. Nor are such innovations socially inevitable, even when widely disseminated, as Ira ni ans discovered in the summer of 2009 when they tried to send images of postelection uprisings out of the country. Such citizen journalism was simply banned, with heavy penalties imposed on transgressors. With every communications invention comes questions of both exploitation and control.

Can the Great American Universities Take Root in Asia?

A description is given of: (1) a finite-state model for asynchronous systems in which the time delays between the scheduling and occurrence of the events that cause state changes are constrained to fall between fixed numerical upper and lower time bounds; (2) a branching-time temporal logic suitable for describing the temporal and logical properties of asynchronous systems, for which the structures of (1) are the natural models; and (3) a functional verification system for asynchronous circuits which generates, from a Boolean circuit with general feedback and specified min/max rise and fall times for the gates, a finite-state structure as in (1), and then exhaustively checks a formal specification of that circuit in the language (2) against that finite-state model. >

An efficient algorithm for displaying 3-D scenes showing a discrete spatially varying surface is described. Given a 2-D map or planar graph composed of polygons where each polygon has a positive real number attribute, a prism is erected on each polygon with height proportional to that attribute. The resulting 3-D scene is plotted with shading and hidden lines removed. Thus the spatial variation of the attribute may be quickly and intuitively grasped by the nontechnical observer. This has applications to areas such as geography if the map is a cartographic map, or to physics if the map diagrams the periodic table. The algorithm takes time O(N*log(N)) where N is the number of edges in the map. Most of the calculations can be done without knowing the prism heights so extra plots with different attributes for the prisms can be produced quickly. This algorithm has been implemented and tested on maps of up to 12000 edges.

We are engaged in teaching technical material, specifically computer science, to a large number of undergraduates (400--500), the majority of whom are non-science majors.Many of these students have trouble learning the course material. We are not here talking about those few students who are affected by such problems as physical handicaps or other specific learning disabilities; non are we concerned with those individuals who exhibit poor study habits or strong preferences for unusual "favored modes of perception" [WEIN]. We are concerned with the significant number of students who, for no apparent reason, have a great deal of difficuly learning elementary computer concepts. Why do some never understand? Why do others, who eventually succeed, take a great deal longer than the majority of our students?This paper is a report on research in progress. Our research at this time is mainly concerned with:(a) Determining, in advance, which students are likely to encounter the severest problems learning computer science;(b) Finding out what there is specifically in the nature of the course material which causes the greatest difficulty for these students; and(c) Developing a methodology for helping students to overcome such learning problems.This paper is organized into 6 major sections.Section I is an introduction to the Natural Sciences 110 course, to the programming language used in this course, and to the major teaching problems we face.Section II is a statement of our goals in this research effort.Section III describes the method by which we are attempting to realize our intended goals.Section IV describes the special recitation sections which are being used to help us monitor the potentially "slower" students.Section V deals with classifying the specific conceptual barriers which we have thus far found to inhibit normal learning in many computer science students.Section VI is 2 statement of the direction which our research will follow in the immediate future.

A Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types. ?0. Introduction. A reduction of one class of quantificational formulas, W,, to another, W2, is an effective mapping 0: W W2 such that (1) for each formula F E W,, Fis satisfiable if and only if 0(F) is satisfiable. If there is a reduction of the class of all formulas to a class W, then W is said to be a reduction class. By Turing's theorem, any reduction class is unsolvable (that is, has a recursively unsolvable decision problem with respect to satisfiability). Now if a reduction 0: W, W2 has the further property that (2) for each formula F E W,, F has a finite model if and only if 0(F) has a finite model, then 0 is said to be a conservative reduction; and W is called a conservative reduction class if there is a conservative reduction of the class of all formulas to W. Trakhtenbrot [Ti] showed that the problem of determining whether an arbitrary quantificational formula has a finite model is unsolvable; it follows that this finite satisfiability problem remains unsolvable for formulas in any conservative reduction class. (Indeed, in [T2] more is proved, namely that the classes of unsatisfiable and finitely satisfiable formulas are recursively inseparable; again it follows immediately that this property remains true of formulas in any conservative reduction class.) In general, when particular classes have been shown to be reduction classes, it has also been possible to show without much further difficulty that they are conservative reduction classes. However, some years ago a case arose which seemed not to be of this type. A Krom formula is one whose matrix is in conjunctive normal Received February 20, 1980. 'The authors thank the "Stiftung Volkswagenwerk" for its financial support of the conference on logic and complexity theory held in Aachen in September 1979, during which this collaborative work was initiated, and also the Institut fur Mathematische Logik und Grundlagenforschung of the University of Munster for its hospitality during the week after the conference. We are also grateful to Warren Goldfarb for his corrections to an earlier draft of this paper. 'Research supported in part by NSF Grants MCS76-09375-AOI and MCS8O05386.

We study the computational complexity of the satisfiability problem for Krom (CNF-2) formulas. Upper and lower bounds are obtained for several decidable classes of formulas determined by quantifier prefix and degree of predicate letters. For example, we show that determining satisfiability of Krom formulas with quantifier prefix of the form ∃…∃∀…∀∃…∃ is complete for deterministic exponential time, but that if the number of universal quantifiers is bounded then polynomial time suffices.

The emptiness problem for stack automata is shown decidable by reducing that problem to a solvable decision problem for the predicate calculus. Similar decision procedures are outlined for classes of weaker automata.

In this paper we consider decision problems for subclasses of Kr, the class of those formulas of pure quantification theory whose matrices are conjunctions of binary disjunctions of signed atomic formulas. If each of Q1, …, Qn is an ∀ or an ∃, then let Q1 … Qn be the class of those closed prenex formulas with prefixes of the form (Q1x1)… (Qnxn). Our results may then be stated as follows:Theorem 1. The decision problem for satisfiability is solvable for the class ∀∃∀ ∩ Kr.Theorem 2. The classes ∀∃∀∀ ∩ Kr and ∀∀∃∀ ∩ Kr are reduction classes for satisfiability.Maslov [11] showed that the class ∃…∃∀…∀∃…∃ ∩ Kr is solvable, while the first author [1, Corollary 4] showed ∃∀∃∀ ∩ Kr and ∀∃∃∀ ∩ Kr to be reduction classes. Thus the only prefix subclass of Kr for which the decision problem remains open is ∀∃∀∃…∃∩ Kr.The class ∀∃∀ ∩ Kr, though solvable, contains formulas whose only models are infinite (e.g., (∀x)(∃u)(∀y)[(Pxy ∨ Pyx) ∧ (¬ Pxy ∨ ¬Pyu)], which can be satisfied over the integers by taking P to be ≥). This is not the case for Maslov's class ∃…∃∀…∀∃…∃ ∩ Kr, which contains no formula whose only models are infinite ([2] [5]).Theorem 1 was announced in [1, Theorem 4], but the proof sketched there is defective: Lemma 4 (p. 17) is incorrectly stated. Theorem 2 was announced in [9].

Let Q be the class of closed quantificational formulas ∀x∃u∀yM without identity such that M is a quantifier-free matrix containing only monadic and dyadic predicate letters and containing no atomic subformula of the form Pyx or Puy for any predicate letter P. In [DKW] Dreben, Kahr, and Wang conjectured that Q is a solvable class for satisfiability and indeed contains no formula having only infinite models. As evidence for this conjecture they noted the solvability of the subclass of Q consisting of those formulas whose atomic subformulas are of only the two forms Pxy, Pyu and the fact that each such formula that has a model has a finite model. Furthermore, it seemed likely that the techniques used to show this subclass solvable could be extended to show the solvability of the full class Q, while the syntax of Q is so restricted that it seemed impossible to express in formulas of Q any unsolvable problem known at that time.In 1966 Aanderaa refuted this conjecture. He first constructed a very complex formula in Q having an infinite model but no finite model, and then, by an extremely intricate argument, showed that Q (in fact, the subclass Q2 defined below) is unsolvable ([Aa1], [Aa2]). In this paper we develop stronger tools in order to simplify and extend the results of [Aa2]. Specifically, we show the unsolvability of an apparently new combinatorial problem, which we shall call the linear sampling problem (defined in §1.2 and §2.3). From the unsolvability of this problem there follows the unsolvability of two proper subclasses of Q, which we now define. For each i ≥ 0, let Pi be a dyadic predicate letter and let Ri be a monadic predicate letter.

Among the earliest and best-known theorems on the decision problem is Skolem's result [7] that the class of all closed formulas with prefixes of the form ∀···∀∃···∃ is a reduction class for satisfiability for the whole of quantification theory. This result can be refined in various ways. If the Skolem prefix alone is considered, the best result [8] is that the ∀∀∀∃ class is a reduction class, for Gödel [3], Kalmár [4], and Schütte [6] showed the ∀∀∃···∃ class to be solvable. The purpose of this paper is to describe the more complex situation that arises when (Skolem) formulas are restricted with respect to the arguments of their atomic subformulas. Before stating our theorem, we must introduce some notation.Let x, y1, y2, be distinct variables (we shall use v1, v2, ··· and w1, w2, ··· as metavariables ranging over these variables), and for each i ≥ 1 let Y(i) be the set {y1, ···, yi}. An atomic formula Pv1 ··· vk will be said to be {v1, ···, vk}-based. For any n ≥ 1, p ≥ 1, and any subsets Y1, ··· Yp of Y(n), let C(n, Y1, ···, Yp) be the class of all those closed formulas with prefix ∀y1 ··· ∀yn∃x such that each atomic subformula not containing the variable x is Yi-based for some i, 1 ≤ i ≤ p.

We analyze the computational complexity of determining whether F is satisfiable when F is a formula of the classical predicate calculus obeying certain syntactic restrictions. For example, for the monadic predicate calculus and the Gödel or 3 … ∃∀∀∃ … 3 prefix class we obtain lower and upper nondeterministic time bounds of the form cn/log n. The lower bounds are established by using acceptance problems for time-bounded Turing machines and alternating pushdown and stack automata.

By theword problemfor some class of algebraic structures we mean the problem of determining, given a finite setEof equations between words (i.e. terms) and an additional equationx=y, whetherx=ymust hold in all structures satisfying each member ofE. In 1947 Post [P] showed the word problem for semigroups to be undecidable. This result was strengthened in 1950 by Turing, who showed the word problem to be undecidable forcancellation semigroups,i.e. semigroups satisfying thecancellation propertyNovikov [N] eventually showed the word problem for groups to be undecidable.(Many flaws in Turing's proof were corrected by Boone [B]. Even after his corrections, at least one problem remains; the sentence on line 16 of p. 502 of [T] does not follow if one relation is principal and the other is a commutation relation. A corrected and somewhat simplified version of Turing's proof can be built on the construction given here.)In 1966 Gurevich [G] showed the word problem to be undecidable forfinitesemigroups. However, this result on finite structures has not been extended to cancellation semigroups or groups; indeed it is easy to see that a finite cancellation semigroup is a group, so both questions are the same. We do not here settle the word problem for finite groups, but we do show that the word problem is undecidable for finite semigroups with zero (that is, having an element 0 such thatx0 = 0x= 0 for allx) satisfying an approximation to the cancellation property (1).

For each fixed set of Boolean connectives, how hard is it to determine satisfiability for formulas with only those connectives? We show that a condition sufficient for NP-completeness is that the functionx Λ ~ y be representable, and that any set of connectives not capable of representing this function has a polynomial-time satisfiability problem.

Consider a family of boolean circuits C~, C2,..., C,,..., constructed by some uniform, effective procedure operating on input n. Such a procedure provides a concise representation of a family of parallel algorithms for computing boolean values. A formula of first-order logic may also be viewed as a concise representation of a family of parallel algorithms for evaluating boolean functions. The parallelism is implicit in the quantification (a formula gx q~(x) is true if and only if each of the formulas q~(a) is true, and all these formulas can be checked simultaneously), and universes of different sizes give rise to boolean functions with different numbers of inputs (the boolean values of the formula's predicates on various combinations of elements of the universe). This note presents an extended first-order logic designed to be exactly equivalent in expressiveness to polynomialsize, constant-depth, unbounded-fan-in circuits constructed by Turing machines of bounded computational complexity. © 1984 Academic Press, Inc.

Culling by the use of external body characters has resulted in two ideas concerning its purpose. The owner of the general farm flock perceives a quick disposal of stock that has, for the time being, ceased to produce. Little thought is given to the annual production of the birds culled. The commercial poultryman, on the other hand, has come to realize that when a bird is weeded from the flock during the summer culling season it should be one that is not likely to return a profit for the entire year, or one that is practically certain not to resume production for several months following the time of culling. Thus a practical application is made of the principle that a positive relationship exists between the individual culling factors and annual production. This report shows that the month of July, the usual time for summer culling to become active, is too . . .

The idea in presenting a paper along the lines designated is not to show the methods which are practiced in New Jersey as an ideal example, or to convey the idea that we have a department which is perfect in all respects. We appreciate, on the other hand, that the New Jersey Department has many shortcomings and can be improved in many ways. We appreciate also that conditions in the various states differ very materially and that one type of organization and one method of administration would not by virtue of local conditions be the best for all institutions. We have, however, been successful in developing, within the last few years, a Department of Poultry Husbandry at the New Jersey State College (Rutgers) which has attained considerable size and importance in relation to the other Agricultural efforts of similar nature in the state. We have learned many things by experience,…

Held at Cornell University, Ithaca, N. Y., July 8th and 9th, 1918 The Annual Meeting of our Association held at Ithaca last July was one of the most successful, helpful and enjoyable sessions of our Convention yet held. The holding of the Convention immediately following the Judging School was an extreme help to all, and was in part responsible for the exceptional attendance. Forty-five members were present during the Convention which was the largest enrollment which has ever been attained. President Phillips presided at all sessions. A highly appreciated and instructive address of welcome was given by Dean Mann of the College of Agriculture, which was appropriately responded to by President Philips. Minutes of the 1915–16 Meeting were read and approved. Th e Secretary's and Treasurer's reports for 1915–16 and 1916–17 were presented, approved and ordered spread on the Minutes. The Auditing Committee reported, showing the Treasurer's …

I. I ntroduction The problem of the inheritance of fecundity in the domestic fowl is one of first rate scientific interest and of great economic importance. That various breeds of poultry differ in their capacity for egg production has been clearly shown by the results of numerous egg-laying contests. In the sense that egg laying capacity is to some extent characteristic of breeds, fecundity is a heritable character. We require, however, to know much more than this concerning the inheritance of egg producing capacity. Within any breed of poultry the record made in any period of time varies greatly from individual to individual. It is important to know whether these variations depend upon the genetic constitution of the parent in such a way that the progeny may show similar, even if not equal, superiority or inferiority. It is impossible in this place to attempt a detailed review of the literature of . . .

The meeting was called to order promptly at 9:30 A. M. on August 15th, with President Kent in the chair. A most interesting and appropriate address of welcome was given by Dean and Director J. G. Lipman of the New Jersey State University. An appropriate response was given by President Kent. The minutes of the 1919–1920 convention were read and approved. The Secretary and Treasurer’s report for 1919–1920 was presented and approved. The Treasurer’s report was audited and found correct. Upon a motion, duly seconded and carried, the courtesy of attending the sessions of the Convention was given to members of the faculty and staff of the State University of the New Jersey College of Agriculture. President Kent appointed the following Resolutions Committee : Prof. Wm. A. Lippincott Prof. J. C. Graham Prof. W. R. Graham Some discussion was entertained regarding the desirability of sectional meetings. A committee . . .

In this paper we consider classes of quantificational formulas specified by restrictions on the number of atomic subformulas appearing in a formula. Little seems to be known about the decision problem for such classes, except that the class whose members contain at most two distinct atomic subformulas is decidable [2]. (We use “decidable” and “undecidable” throughout with respect to satisfiability rather than validity. All undecidable problems to which we refer are of maximal r.e. degree.) The principal result of this paper is the undecidability of the class of those formulas containing five atomic subformulas and with prefixes of the form ∀∃∀…∀. In fact, we show the undecidability of two sub-classes of this class: one (Theorem 1) consists of formulas whose matrices are in disjunctive normal form with two disjuncts; the other (Corollary 1) consists of formulas whose matrices are in conjunctive normal form with three conjuncts. (Theorem 1 sharpens Orevkov's result [8] that the class of formulas in disjunctive normal form with two disjuncts is undecidable.) A second corollary of Theorem 1 shows the undecidability of the class of formulas with prefixes of the form ∀…∀∃, containing six atomic subformulas, and in conjunctive normal form with three conjuncts. These restrictions to prefixes ∀∃∀…∀ and ∀…∀∃ are optimal. For by a result of the first author [5], any class of prenex formulas obtained by restricting both the number of atomic formulas and the number of universal quantifiers is reducible to a finite class of formulas, and so each such class is decidable; and the class of formulas with prefixes ∃…∃∀…∀ is, of course, decidable.

The primary purpose of this paper is to consider the interrelationship of the egg records of various periods during the second laying year of the White Leghorn fowl. It is, therefore, a continuation of earlier investigations in this general field, which have, of necessity, been limited to a consideration of the relationship between the periods of the first or pullet year (Harris and others, 1917–1921). While our primary purpose has been the investigation of the correlations for the second laying year, these interrelationships can be fully understood only when considered in comparison with the like coefficients for the first year. Fortunately the extensive data of the Vineland International Egg Laying and Breeding Contest permits the consideration of the complete first and second year record of 443 individual White Leghorn birds. Our problem is, therefore, to consider all of the more important correlations between the egg records of . . .

In another place (Harris and Lewis, 1921) we have shown that the correlation between the first and second year egg laying record of the White Leghorn fowl is sufficiently high that the mere information as to whether a bird is or is not laying in certain critical months of the first year furnishes some basis for culling for second year production. A detailed biometric treatment of the problem of the correlation between the egg laying activity of the first and the second year is now in press (Harris and Lewis, 1922). In culling the flock either for the purpose of eliminating the birds which will not lay further during the pullet year or for the purpose of selecting the birds which will make the best records during the second year, or be the most suitable for use as breeders the second year, a certain per cent of the flock is . . .

In [7] Manna reduces certain decision problems for program schemata to the problem of determining whether or not a first-order formula is satisfiable. Here we give an improved construction, which yields new positive results and suggests a method that may be useful in further investigations.

This paper is concerned with constructing, for each expression in a given program text, a symbolic expression whose value is equal to the value of the text expression for all executions of the program. A cover is a mapping from text expressions to such symbolic expressions. Covers can be used for constant propagation, code motion, and a variety of other program optimizations. Covers can also be used as an aid in symbolic program execution and for finding loop invariants for program verification. We describe a direct (non-iterative) algorithm for computing a cover. The cover computed by our algorithm is characterized as a minimum of a certain fixed point equation, and is in general a better cover than might be computed by iteration methods (which can compute fixed point covers which are not minimal). Our algorithm is efficient and applicable to all flow graphs. A variant of our algorithm is implemented by Kalman and Kortesoja (IEEE Trans. Software Eng. SE-6 (1980), 512–519) in an optimizing compiler.

A symmetric Turing machine is one such that the “yields” relation between configurations is symmetric. The space complexity classes for such machines are found to be intermediate between the corresponding deterministic and nondeterministic space complexity classes. Certain natural problems are shown to be complete for symmetric space complexity classes, and the relationship of symmetry to determinism and nondeterminism is investigated.

Minutes of the Meeting of the Eastern Section of the American Association of Instructors and Investigators in Poultry Husbandry, held July 27th and 28th, at the Massachusetts Agricultural College, Amherst, Mass. The meeting was called to order by Prof. Graham, at 1:30 P. M., July 27th. The following members of the Association being present: William F. Kirkpatrick, Agricultural College, Storrs, Conn. William S. Dilts, Georgia State College of Agriculture, Athens, Ga. R. V. Mitchell, Delaware College, Newark, Del. H. R. Lewis, Agricultural College, New Brunswick, N. J. H. M. Lamon, U. S. Dept. of Agriculture, Washington, D. C. Edward Brown, London, England. J. C. Graham, Massachusetts Experiment Station, Amherst, Mass. A. G. Lunn, Agricultural Experiment Station, Amherst, Mass. Seth Jones, Dept. of Agriculture, Sussex, New Brunswick, Canada. N. W. Sanborn, Holden, Mass. J. E. Rice, Cornell University, 308 Waite Ave., Ithaca, N. Y. W. G. Krum, Cornell University, Ithaca, N.…