logic in computer science for the academic conference lics see ieee symposium on logic in computer science diagrammatic representation of computer logic gates 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 in addition some other major areas of theoretical overlap between logic and computer science are gdels 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 the frame problem is a basic problem that must be overcome when using firstorder logic to represent the goals and state of an artificial intelligence agent the curryhoward correspondence is a relation between logical systems and software this theory established a precise correspondence between proofs and programs in particular it showed that terms in the simplytyped lambdacalculus correspond to proofs of intuitionistic propositional logic category theory represents a view of mathematics that emphasizes the relations between structures it is intimately tied to many aspects of computer science type systems for programming languages the theory of transition systems models of programming languages and the theory of programming language semantics computers to assist logicians one of the first applications to use the term artificial intelligence was the logic theorist system developed by allen newell jc 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 a logical system that states 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 the 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 logical theorems and proofs logic applications for computers there has always been a strong influence from mathematical logic on the field of artificial 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 described firstorder logic fol as the metric by which all ai knowledge representation formalisms should be evaluated there is no more general or powerful known method for describing and analyzing information than fol the reason fol itself is simply not used as a computer language is that it is actually too expressive 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 and computability the more expressive the language is the closer it is to fol the more likely it is to be slower and prone to an infinite loop 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 highperformance computation especially if they take advantage of optimization algorithms and compilation another major area of research for logical theory was software engineering research projects such as the knowledgebased software assistant and programmers apprentice programs applied logical theory to validate the correctness of software specifications they also used them to transform the specifications into efficient code on diverse platforms and to prove the equivalence between the implementation and the specification another important application of logic to computer technology has been in the area of frame languages and automatic classifiers frame languages such ais klone have a rigid semantics definitions in klone can be directly mapped to set theory and the predicate calculus this allows specialized theorem provers called classifiers to analyze the various declarations between sets subsets and relations 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 the web ontology language to allow a logical semantic level on to the existing internet this layer of is called the semantic web temporal logic is used for reasoning in concurrent systems automated reasoning computational logic logic programming augusto luis m 2017 logical consequences theory and applications an introduction london college publications isbn9781848902367 benari mordechai 2003 mathematical logic for computer science 2nd ed springerverlag isbn1852333197 huth michael ryan mark 2004 logic in computer science modelling and reasoning about systems 2nd ed cambridge university press isbn052154310x burris stanley n 1997 logic for mathematics and computer science prentice hall isbn0132859742 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 vtelogic outline history fields argumentation theory axiology critical thinking logic in computer science mathematical logic metalogic metamathematics nonclassical logic philosophical logic philosophy of logic set theory foundations abduction analytic and synthetic propositions antinomy a priori and a posteriori deduction definition description induction inference logical form logical consequence logical truth name necessity and sufficiency meaning paradox possible world presupposition probability reason reference semantics statement strict implication substitution syntax truth validity liststopics mathematical logic boolean algebra set theory other logicians rules of inference paradoxes fallacies logic symbols portal category wikiprojecttalk changes 