Applied Logic Corporation

Last updated
Applied Logic Corporation
Industry Time-sharing computers
Founded1962;61 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 KL-10 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 impetus 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".

<span class="mw-page-title-main">Theorem</span> In mathematics, a statement that has been proved

In mathematics, a theorem is a statement that has been proved, or can be proved. The proof of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of the axioms and previously proved theorems.

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).

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.

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.

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

<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

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.

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.

Donald W. Loveland is a professor emeritus of computer science at Duke University who specializes in artificial intelligence. He is well known for the Davis–Putnam–Logemann–Loveland algorithm.

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.