The design of digital circuits is entirely based on proposal logic, so much so that its engineers call it "logic design" rather than "circuit design". Even writing a computer program is often thought to involve devising its "logic". (Note that "logic" in the latter sense is an informal idea rather than formal logic, used to refer to the flow on information through the program and whether it is being processed correctly.)
Predicate logic and its mathematical cousin, set theory, are used in a variety of computing languages, e.g., the language SQL for relational database queries. There are also programming languages based on logic, called "logic programming languages".
Knowledge representation, which you have already mentioned, has many formalisms based on logic. Even if it uses non-logical formalisms, many of them still have a logical meaning, and hence are based on logic.
Probabilistic logic, where statements do not have just true/false values, but levels of certainty/uncertainty, is increasingly the foundation for machine learning systems.
If you want to formally state what a program does, i.e., giving a program specification, you will end up using some form of a logical language. Indeed, there are many program specification languages, like Z and B, which are based on predicate logic and set theory. There are also specification languages based on equational logic, such as Larch. Computer Scientists often invent new logics to represent the needs of computer science, e.g., Hoare Logic and Separation Logic, or they pick up and develop various underused forms of traditional logics, such as temporal logic and modal logic, and develop them further.
If you want to verify whether a program does what it is supposed to do, then you end up using not only the language of logic, but the entire machinery of logic: proof theory, model theory and decision procedures. Verification technology is now growing by leaps and bounds and I expect that, in another decade or so, they would be routinely used for almost all software development.
The design of digital circuits is entirely based on proposal logic, so much so that its engineers call it "logic design" rather than "circuit design". Even writing a computer program is often thought to involve devising its "logic". (Note that "logic" in the latter sense is an informal idea rather than formal logic, used to refer to the flow on information through the program and whether it is being processed correctly.)
Predicate logic and its mathematical cousin, set theory, are used in a variety of computing languages, e.g., the language SQL for database queries. There are also programming languages based on logic, called "logic programming languages".
Knowledge representation, which you have already mentioned, has many formalisms based on logic. Even if it uses non-logical formalisms, many of them still have a logical meaning, and hence are based on logic.
Probabilistic logic, where statements do not have just true/false values, but levels of certainty/uncertainty, is increasingly the foundation for machine learning systems.
If you want to formally state what a program does, i.e., giving a program specification, you will end up using some form of a logical language. Indeed, there are many program specification languages, like Z and B, which are based on predicate logic and set theory. There are also specification languages based on equational logic, such as Larch. Computer Scientists often invent new logics to represent the needs of computer science, e.g., Hoare Logic and Separation Logic, or they pick up and develop various underused forms of traditional logics, such as temporal logic and modal logic, and develop them further.
If you want to verify whether a program does what it is supposed to do, then you end up using not only the language of logic, but the entire machinery of logic: proof theory, model theory and decision procedures. Verification technology is now growing by leaps and bounds and I expect that, in another decade or so, they would be routinely used for almost all software development.
The design of digital circuits is entirely based on proposal logic, so much so that its engineers call it "logic design" rather than "circuit design". Even writing a computer program is often thought to involve devising its "logic". (Note that "logic" in the latter sense is an informal idea rather than formal logic, used to refer to the flow on information through the program and whether it is being processed correctly.)
Predicate logic and its mathematical cousin, set theory, are used in a variety of computing languages, e.g., the language SQL for relational database queries. There are also programming languages based on logic, called "logic programming languages".
Knowledge representation, which you have already mentioned, has many formalisms based on logic. Even if it uses non-logical formalisms, many of them still have a logical meaning, and hence are based on logic.
Probabilistic logic, where statements do not have just true/false values, but levels of certainty/uncertainty, is increasingly the foundation for machine learning systems.
If you want to formally state what a program does, i.e., giving a program specification, you will end up using some form of a logical language. Indeed, there are many program specification languages, like Z and B, which are based on predicate logic and set theory. There are also specification languages based on equational logic, such as Larch. Computer Scientists often invent new logics to represent the needs of computer science, e.g., Hoare Logic and Separation Logic, or they pick up and develop various underused forms of traditional logics, such as temporal logic and modal logic, and develop them further.
If you want to verify whether a program does what it is supposed to do, then you end up using not only the language of logic, but the entire machinery of logic: proof theory, model theory and decision procedures. Verification technology is now growing by leaps and bounds and I expect that, in another decade or so, they would be routinely used for almost all software development.
There are extremely deep and pervasive connections between logic and computer science. In understanding what they might be, keep in mind that computer science is also called "information technology" or "informatics", meaning that computer systems capture, process and deliver information. Well, logic is a similar thing. It studies how information is captured in sentences and how it is possible for one statement to be a consequence of another, i.e., how its information content is already present in another statement (or collection of statements). In that sense, logic and computer science are essentially the same discipline, focusing on different aspects. Logicians (Church, Kleene, Turing, Post and their students and colleagues) created the discipline of Computer Science, and many logicians continue to make contributions to Computer Science, most notably Jean-Yves Girard and his students.
Here are some standard applications of logic in Computer Science:
The design of digital circuits is entirely based on proposal logic, so much so that its engineers call it "logic design" rather than "circuit design". Even writing a computer program is often thought to involve devising its "logic". (Note that "logic" in the latter sense is an informal idea rather than formal logic, used to refer to the flow on information through the program and whether it is being processed correctly.)
Predicate logic and its mathematical cousin, set theory, are used in a variety of computing languages, e.g., the language SQL for database queries. There are also programming languages based on logic, called "logic programming languages".
Knowledge representation, which you have already mentioned, has many formalisms based on logic. Even if it uses non-logical formalisms, many of them still have a logical meaning, and hence are based on logic.
Probabilistic logic, where statements do not have just true/false values, but levels of certainty/uncertainty, is increasingly the foundation for machine learning systems.
If you want to formally state what a program does, i.e., giving a program specification, you will end up using some form of a logical language. Indeed, there are many program specification languages, like Z and B, which are based on predicate logic and set theory. There are also specification languages based on equational logic, such as Larch. Computer Scientists often invent new logics to represent the needs of computer science, e.g., Hoare Logic and Separation Logic, or they pick up and develop various underused forms of traditional logics, such as temporal logic and modal logic, and develop them further.
If you want to verify whether a program does what it is supposed to do, then you end up using not only the language of logic, but the entire machinery of logic: proof theory, model theory and decision procedures. Verification technology is now growing by leaps and bounds and I expect that, in another decade or so, they would be routinely used for almost all software development.
In fact, the connections between logic and computer science are so deep and pervasive that I would say it is a hard to be a good computer scientist without a thorough understanding of logic.
The reason some AI scientists underrate logic at this time is that some of the early developers of AI had proposed off-the-shelf logic as a tool rather than a foundation. AI, by its very nature, promises to deliver magic. We don't have to do the hard job of programming systems to deliver results. They would be able to figure out on their own how to produce solutions because they would be "intelligent". Logic seemed to point the way because if computer systems understood logic and knew how to process information using the rules of logic, they would be able to deliver magic. That kind of faith in logic was, in retrospect, misplaced. In the first place, off-the-shelf logic is too strong and too weak at the same time. It is too strong in the sense that the rules of logic are too general to devise effective procedures. It is also too weak because it is the logic devised by mathematicians for the needs of mathematics and it doesn't have the vocabulary needed to deal with a lot of other kinds of real-world information that AI systems must handle (such as uncertainty, contextual information like time, change, knowledge, agency and so forth). So, AI is currently undergoing a backlash against logic. But I think that, when they get over that backlash, AI scientists will realize that all the newer methods are still based on logic, broadly construed.