Logic in computer science
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:
- Theoretical foundations and analysis
- Use of computer technology to aid logicians
- Use of concepts from logic for computer applications
Theoretical foundations and analysis
Logic plays a fundamental role in computer science. Some of the key areas of logic that are particularly significant are computability theory (formerly called recursion theory), modal logic and category theory. The theory of computation is based on concepts defined by logicians and mathematicians such as Alonzo Church and Alan Turing.[1][2] Church first showed the existence of algorithmically unsolvable problems using his notion of lambda-definability. Turing gave the first compelling analysis of what can be called a mechanical procedure and Kurt Gödel asserted that he found Turing's analysis "perfect."[3]. In addition some other major areas of theoretical overlap between logic and computer science are:
- Gödel's incompleteness theorem proves that any logical system powerful enough to characterize arithmetic will contain statements that can neither be proved nor disproved within that system. This has direct application to theoretical issues relating to the feasibility of proving the completeness and correctness of software.[4]
- The frame problem is a basic problem that must be overcome when using first-order logic to represent the goals of an artificial intelligence agent and the state of its environment.[5]
- The Curry–Howard correspondence is a relation between logical systems and programming languages. This theory established a precise correspondence between proofs and programs. In particular it showed that terms in the simply typed lambda calculus correspond to proofs of intuitionistic propositional logic.
- programming language semantics.[6]
- knowledge representation paradigm that is based on formal logic. A logic program is a set of sentences about some problem domain. Computation is performed by applying logical reasoning to solve problems in the domain. Major logic programming language families include Prolog, Answer Set Programming (ASP) and Datalog.
Computers to assist logicians
One of the first applications to use the term artificial intelligence was the Logic Theorist system developed by Allen Newell, Cliff Shaw, and Herbert Simon in 1956. One of the things that a logician does is to take a set of statements in logic and deduce the conclusions (additional statements) that must be true by the laws of logic. For example, if given the statements "All humans are mortal" and "Socrates is human" a valid conclusion is "Socrates is mortal". Of course this is a trivial example. In actual logical systems the statements can be numerous and complex. It was realized early on that this kind of analysis could be significantly aided by the use of computers. Logic Theorist validated the theoretical work of Bertrand Russell and Alfred North Whitehead in their influential work on mathematical logic called Principia Mathematica. In addition, subsequent systems have been utilized by logicians to validate and discover new mathematical theorems and proofs.[7]
Logic applications for computers
There has always been a strong influence from mathematical logic on the field of
For example, IF–THEN rules used in expert systems approximate to a very limited subset of FOL. Rather than arbitrary formulas with the full range of logical operators the starting point is simply what logicians refer to as modus ponens. As a result, rule-based systems can support high-performance computation, especially if they take advantage of optimization algorithms and compilation.[9]
On the other hand,
Another major area of research for logical theory is
Another important application of logic to computer technology has been in the area of
See also
References
- ^ Lewis, Harry R. (1981). Elements of the Theory of Computation. Prentice Hall.
- ISBN 9783211826379. Retrieved 26 December 2013.
- ISBN 9781107002661. Retrieved 17 August 2015.
- ISBN 978-0465026562.
- ^ McCarthy, John; P.J. Hayes (1969). "Some philosophical problems from the standpoint of artificial intelligence" (PDF). Machine Intelligence. 4: 463–502.
- ^ Barr, Michael; Charles Wells (1998). Category Theory for Computing Science (PDF). Centre de Recherches Mathématiques.
- ISBN 978-0262560924.
- ISBN 0-934613-01-X.
The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable.
- doi:10.1016/0004-3702(82)90020-0. Archived from the original(PDF) on 2013-12-27. Retrieved 25 December 2013.
- ^ Rich, Charles; Richard C. Waters (November 1987). "The Programmer's Apprentice Project: A Research Overview" (PDF). IEEE Expert. Archived from the original (PDF) on 2017-07-06. Retrieved 26 December 2013.
- ISBN 0-521-443369. Retrieved 26 December 2013.
- S2CID 29575443.
- doi:10.1038/scientificamerican0501-34. Archived from the originalon April 24, 2013.
- ISBN 0-19-853761-1.
Further reading
- ISBN 978-1447141280.
- Harrison, John (2009). Handbook of Practical Logic and Automated Reasoning (1st ed.). Cambridge University Press. ISBN 978-0521899574.
- Huth, Michael; Ryan, Mark (2004). Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed.). Cambridge University Press. ISBN 978-0521543101.
- Burris, Stanley N. (1997). Logic for Mathematics and Computer Science (1st ed.). Prentice Hall. ISBN 978-0132859745.
External links
- Article on Logic and Artificial Intelligence at the Stanford Encyclopedia of Philosophy.
- IEEE Symposium on Logic in Computer Science (LICS)
- Alwen Tiu, Introduction to logic video recording of a lecture at ANU Logic Summer School '09 (aimed mostly at computer scientists)