Applied Logic Corporation

Last updated
Applied Logic Corporation
Industry Time-sharing computers
Founded1962;62 years ago (1962) in Princeton, New Jersey
Defunct1975 (1975)
FateBankruptcy
Key people
Richard M. Colgate (president)

Applied Logic Corporation (AL/COM) was a time-sharing company in the 1960s and 70s.

Headquartered in Princeton, New Jersey, AL/COM started in 1962 working on "mathematical techniques and their applications to problem-solving." [1]

Seeing the need for in-house time sharing the company bought a Digital Equipment Corporation (DEC) PDP-6 and developed its time sharing service, which came on-line in 1966. [1] [2] In 1968 the company began development of "Mathematics Park" in Montgomery Township, New Jersey, "designed to provide tenants with a computer-serviced and mathematically-oriented environment," adjacent to the Princeton Airport. [3] Also in 1968 the company registered AL/COM as a trademark for its service. [4]

The system involved both custom software and custom hardware, and the service was marketed nationally by a network of associates. [5]

Under the AL-COM Distributor Plan, local computer service firms such as service bureaus, programming, and software firms will be designated as the local AL-COM distributor. The AL-COM distributor will purchase AL-COM computing power at a discount from the Applied Logic Corp., and then in turn sell it at a mark-up. [6]

In the late 1960s, the company developed a system called SAM (Semi-Automated Mathematics) for proving mathematical theories without human intervention. [7] A theorem proved by the system, "SAM's lemma", was "widely hailed as the first contribution of automated reasoning systems to mathematics." [8] The SAM series was one of the first interactive theorem provers and had an influence on subsequent theorem provers. [9]

In 1965 Applied logic acquired a DEC PDP-6 computer system, [10] which became operation in January 1966. [1] By 1969 the company had four DEC PDP-10 dual systems with plans for a fifth, and had expanded nationwide with offices in San Jose, San Diego, and San Francisco. [11] The company also planned to market its time sharing systems in addition to providing services. [12] The company reported sales of $1,200,995, with an operational loss of $63,456. [13]

By 1972 AL/COM had local dial-up facilities in ten cities: Boston, Massachusetts, Buffalo, New York, Chicago, Illinois, Indianapolis, Indiana, Montclair, New Jersey, New York, New York, Philadelphia, Pennsylvania, Princeton, New Jersey, Washington, DC, and Wilmington, Delaware. [1] The computer center was located in Mathematics Park in Princeton. [12]

By late 1969 AL/COM had definite plans for CIT Leasing to leaseback $2.73 million USD of their equipment at Mathematics Park and was considering an additional $7.5 million more. [14] By 1970 the company was in financial difficulty and negotiated an agreement to defer $1,300,000 of debt. [15] [16] Applied Logic filed for Chapter XI bankruptcy in 1975.

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major motivating factor for the development of computer science.

<span class="mw-page-title-main">Digital Equipment Corporation</span> U.S. computer manufacturer (1957–1998)

Digital Equipment Corporation, using the trademark Digital, was a major American company in the computer industry from the 1960s to the 1990s. The company was co-founded by Ken Olsen and Harlan Anderson in 1957. Olsen was president until he was forced to resign in 1992, after the company had gone into precipitous decline.

<span class="mw-page-title-main">Discrete mathematics</span> Study of discrete mathematical structures

Discrete mathematics is the study of mathematical structures that can be considered "discrete" rather than "continuous". Objects studied in discrete mathematics include integers, graphs, and statements in logic. By contrast, discrete mathematics excludes topics in "continuous mathematics" such as real numbers, calculus or Euclidean geometry. Discrete objects can often be enumerated by integers; more formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics".

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

Planner is a programming language designed by Carl Hewitt at MIT, and first published in 1969. First, subsets such as Micro-Planner and Pico-Planner were implemented, and then essentially the whole language was implemented as Popler by Julian Davies at the University of Edinburgh in the POP-2 programming language. Derivations such as QA4, Conniver, QLISP and Ether were important tools in artificial intelligence research in the 1970s, which influenced commercial developments such as Knowledge Engineering Environment (KEE) and Automated Reasoning Tool (ART).

A computer algebra system (CAS) or symbolic algebra system (SAS) is any mathematical software with the ability to manipulate mathematical expressions in a way similar to the traditional manual computations of mathematicians and scientists. The development of the computer algebra systems in the second half of the 20th century is part of the discipline of "computer algebra" or "symbolic computation", which has spurred work in algorithms over mathematical objects such as polynomials.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

<span class="mw-page-title-main">Mathematical proof</span> Reasoning for mathematical statements

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. A proposition that has not been proved but is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.

Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.

<span class="mw-page-title-main">Coq (software)</span> Proof assistant

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human–machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

<span class="mw-page-title-main">Peter B. Andrews</span> American mathematician (born 1937)

Peter Bruce Andrews (born 1937) is an American mathematician and Professor of Mathematics, Emeritus at Carnegie Mellon University in Pittsburgh, Pennsylvania, and the creator of the mathematical logic Q0. He received his Ph.D. from Princeton University in 1964 under the tutelage of Alonzo Church. He received the Herbrand Award in 2003. His research group designed the TPS automated theorem prover. A subsystem ETPS (Educational Theorem Proving System) of TPS is used to help students learn logic by interactively constructing natural deduction proofs.

<span class="mw-page-title-main">John Alan Robinson</span> American computer scientist

John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.

The progression of both the nature of mathematics and individual mathematical problems into the future is a widely debated topic; many past predictions about modern mathematics have been misplaced or completely false, so there is reason to believe that many predictions today will follow a similar path. However, the subject still carries an important weight and has been written about by many notable mathematicians. Typically, they are motivated by a desire to set a research agenda to direct efforts to specific problems, or a wish to clarify, update and extrapolate the way that subdisciplines relate to the general discipline of mathematics and its possibilities. Examples of agendas pushing for progress in specific areas in the future, historical and recent, include Felix Klein's Erlangen program, Hilbert's problems, Langlands program, and the Millennium Prize Problems. In the Mathematics Subject Classification section 01Axx History of mathematics and mathematicians, subsection 01A67 is titled Future prospectives.

In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.

<span class="mw-page-title-main">Joseph Sgro</span> American mathematician

Joseph A. Sgro is an American mathematician, neurologist / neurophysiologist, and an engineering technologist / entrepreneur in the field of frame grabbers, high-speed cameras, smart cameras, image processors, computer vision, and machine vision and learning technologies.

References

  1. 1 2 3 4 Auerbach Publishers (1972). Auerbach Guide to Time Sharing (PDF). Philadelphia, PA. p. 86.{{cite book}}: CS1 maint: location missing publisher (link)
  2. ↑ "Center Offers Shared Use of Computer" . The Central New Jersey Home News. 12 Jan 1966. Retrieved Dec 21, 2021.
  3. ↑ "Construction Underway for Mathematics Park" . The Central New Jersey Home News. 27 Jan 1969. Retrieved Dec 21, 2021.
  4. ↑ "Legal Force Trademarkia" . Retrieved May 25, 2013.
  5. ↑ "Time Sharing Users: What's an AL/COM (advertisement)". Hartford Courant. 16 Mar 1969. Retrieved Dec 21, 2021.
  6. ↑ "New Computer Plan Unveiled". The Central New Jersey Home News. 2 May 1968.
  7. ↑ Krantz, Steven G. (2011). The Proof is in the Pudding: The Changing Nature of Mathematical Proof. Springer Science & Business Media. p. 122. ISBN   978-0-387-48908-7 . Retrieved Jan 9, 2020.
  8. ↑ MacKenzie, Donald A. (2004). Mechanizing Proof: Computing, Risk, and Trust. MIT Press. p. 89. ISBN   0-262-13393-8 . Retrieved Jan 9, 2020.
  9. ↑ Harrison, John (2007). "A Short Survey of Automated Reasoning". Algebraic Biology. Lecture Notes in Computer Science. Vol. LNCS 4545. Springer. pp. 334–349. doi:10.1007/978-3-540-73433-8_24. ISBN   978-3-540-73432-1 . Retrieved 24 January 2020.
  10. ↑ "Decuscope" (PDF). Decuscope. 4 (1). January 1965. Retrieved Jan 9, 2020.
  11. ↑ "First Dual AL-10 Activated in AL/Com's T/S Network". ComputerWorld. September 10, 1969. Retrieved March 31, 2022.
  12. 1 2 "APPLIED LOGIC EXPANDS". Town Topics. November 20, 1969. Retrieved March 31, 2022.
  13. ↑ "EARNINGS REPORTED". Town Topics. June 12, 1969. Retrieved March 31, 2022.
  14. ↑ "Lease Arrangement Set By C.I.T. and Applied Logic". Town Topics. November 13, 1969. Retrieved March 31, 2022.
  15. ↑ "Applied Logic Lays Off 40% of Workers, All in R&D". Computer World. May 13, 1970. Retrieved March 31, 2022.
  16. ↑ "In re APPLIED LOGIC CORPORATION, Bankrupt. NEW JERSEY NATIONAL BANK, Plaintiff-Appellant, v. Daniel GUTTERMAN, as Trustee of Applied Logic Corporation, Bankrupt, Defendant-Appellee". April 27, 1978. Archived from the original on May 14, 2010. Retrieved May 25, 2013.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.