Logic in computer science covers the overlap between the field oflogic and that ofcomputer science. The topic can essentially be divided into three main areas:
Logic plays a fundamental role in computer science. Some of the key areas of logic that are particularly significant arecomputability theory (formerly called recursion theory),modal logic andcategory theory. Thetheory of computation is based on concepts defined by logicians and mathematicians such asAlonzo Church andAlan Turing.[1][2] Church first showed the existence ofalgorithmically unsolvable problems using his notion of lambda-definability. Turing gave the first compelling analysis of what can be called a mechanical procedure andKurt 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:
One of the first applications to use the termartificial intelligence was theLogic Theorist system developed byAllen Newell,Cliff Shaw, andHerbert 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 ofBertrand Russell andAlfred North Whitehead in their influential work on mathematical logic calledPrincipia Mathematica. In addition, subsequent systems have been utilized by logicians to validate and discover new mathematical theorems and proofs.[7]
There has always been a strong influence from mathematical logic on the field ofartificial intelligence (AI). From the beginning of the field it was realized that technology to automate logical inferences could have great potential to solve problems and draw conclusions from facts.Ron Brachman has describedfirst-order logic (FOL) as the metric by which all AIknowledge representation formalisms should be evaluated. First-order logic is a general and powerful method for describing and analyzing information. The reason FOL itself is simply not used as a computer language is that it is actually tooexpressive, in the sense that FOL can easily express statements that no computer, no matter how powerful, could ever solve. For this reason every form of knowledge representation is in some sense a trade off between expressivity andcomputability. A widely held belief maintains that the more expressive the language is (i.e. the closer it is to FOL), the more likely it is to be slower and prone to an infinite loop.[8] However, in a recent work[9] by Heng Zhang et al., this belief has been rigorously challenged. Their findings establish that all universal knowledge representation formalisms arerecursively isomorphic. Furthermore, their proof demonstrates that FOL can be translated into a pure procedural knowledge representation formalism defined by Turing machines with computationally feasible overhead, specifically within deterministic polynomial time or even at lower complexity.[9]
For example, IF–THEN rules used inexpert 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 asmodus ponens. As a result,rule-based systems can support high-performance computation, especially if they take advantage of optimization algorithms and compilation.[10]
On the other hand,logic programming, which combines theHorn clause subset of first-order logic with anon-monotonic form ofnegation, has both high expressive power and efficientimplementations. In particular, the logic programming languageProlog is aTuring complete programming language.Datalog extends therelational database model with recursive relations, whileanswer set programming is a form of logic programming oriented towards difficult (primarilyNP-hard)search problems.
Another major area of research for logical theory issoftware engineering. Research projects such as theKnowledge Based Software Assistant and Programmer's Apprentice programs have applied logical theory to validate the correctness ofsoftware specifications. They have also used logical tools to transform the specifications into efficient code on diverse platforms and to prove the equivalence between the implementation and the specification.[11] This formal transformation-driven approach is often far more effortful than traditional software development. However, in specific domains with appropriate formalisms and reusable templates the approach has proven viable for commercial products. The appropriate domains are usually those such as weapons systems, security systems, and real-time financial systems where failure of the system has excessively high human or financial cost. An example of such a domain isVery Large Scale Integrated (VLSI) design—the process for designing the chips used for the CPUs and other critical components of digital devices. An error in a chip can be catastrophic. Unlike software, chips can't be patched or updated. As a result, there is commercial justification for usingformal methods to prove that the implementation corresponds to the specification.[12]
Another important application of logic to computer technology has been in the area offrame languages and automatic classifiers.Frame languages such asKL-ONE can be directly mapped toset theory and first-order logic. This allows specializedtheorem provers called classifiers to analyze the various declarations betweensets,subsets, andrelations in a given model. In this way the model can be validated and any inconsistent definitions flagged. The classifier can also infer new information, for example define new sets based on existing information and change the definition of existing sets based on new data. The level of flexibility is ideal for handling the ever changing world of the Internet. Classifier technology is built on top of languages such as theWeb Ontology Language to allow a logical semantic level on top of the existing Internet. This layer is called theSemantic Web.[13][14]
Temporal logic is used for reasoning inconcurrent systems.[15]
{{cite book}}:ISBN / Date incompatibility (help)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.
| Major fields |
| ||||
|---|---|---|---|---|---|
| Foundations | |||||
| Lists |
| ||||
