Reason to learn propositional & predicate logic

Question

I can understand the importance that computer scientists or any software development related engineers should have understood the study of basic logics as a basis.

But is there any tasks/jobs that explicitly require the knowledge about these, other than the tasks that require any kind of knowledge representation using Knowledge Base? I want to hear the types of tasks, rather than conceptual responses.

The reason I ask this is just from my curiosity. While CS students have to spend certain amount of time on this subject, some practicality-intensive courses (e.g. AI-Class) skipped this topic entirely. And I just wonder that for example knowing predicate logic might help drawing ER diagram but might not be a requirement.

---

Update 5/27/2012) Thanks for answers. Now I think I totally understand & agree with the importance of logicin CS with its vast amount of application. I just picked the best answer truly from the impressiveness that I got by the solution for Windows' blue screen issue.

Answer 1

I tend to like Unification and anything related to it. If you don't know propositional & predicate logic, then you are skipping the basics of logic. If you have an interest in anything listed, then it would be like having an interest in math and skipping addition and multiplication. Logic is not just for AI.

As a practical answer, remember the Intel floating point problem and how you never see them anymore? Thanks to the use of theorem provers they are a thing of the past. Remember the Microsoft blue screen of death. Thanks to SAT solvers, model checking and other logic based solution, they are an endangered species.

Answer 2

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

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.

Answer 3

Logic is fundamental to all theoretical computer science. Without learning these, you won't be able to properly grasp programming language semantics, Turing machines, logic programming, computability, and so on. Even reasoning about your programs will be more difficult without it. Certainly, trying to do a mathematical proof of some CS concept with be virtually impossible.

Or maybe you are asking about uses in industry. Learning logic forms the basis for learning how to reason clearly and see holes in other people's arguments. Logic is fundamental, whether you use the formal symbols or not.

Answer 4

One of the repeating tasks CS practitioners and theorists face is gaining confidence in the correctness of their code.

There are two main approaches:

1. Proof: Devise a logical proof that part of a system has certain properties, possibly aided by preconditions, design-by-contract, code checkers.
2. Testing: Test that certain properties hold for a variety of inputs and then induce that that property holds for other inputs.

The first, based on logical methods, is often the only option when

1. There is no typical input. For example, when testing security properties, it is the atypical inputs that you have to worry about so unless you can logically reason about which inputs are atypical, you are unlikely to get good coverage.
2. The configuration space is very large, so you have to decompose it into parts by logically reasoning about which parts can affect which other parts before testing locally.
3. You have only documentation describing edge-case behavior of systems outside your control. You might be able to simulate them but can't test what happens when an external dependency fails because you are not capable of causing it to fail for legal or ethical reasons.

Empirical testing in the absence of a proof is basically a substitute for proof. When you're designing a system to be testable, you are building up a proof sketch where you fill in parts of the proof with "test X,Y, and Z here." The ability to reason logically is essential to be able to architect a testable system. If the system is not testable or provable then its designer/architect has no business saying it is fit for its intended use.

Answer 5

Two most important fields that logic plays vital role are:

1. Formal Language specification and verification.
2. Fixed parameter tractable classes.

---

Seems needs some clarification, in formal languages you need to extremely work on logic, for clarification take a look at: 1. Formal language. 2. Introduction to $Z$.

In short: 1. Definition of language needs logic, 2: Justice of it's procedures needs logic, 3. verification procedures need logic.

I should mention that this is different from compiler design or ..., This is "Formal" definition of languages, main reason to do this is proving correctness of language or model, also having a formal proof. This can be used in verification of software models, finding errors before implementing, finding deadlocks again before implementing, ...., For software which simulate this you can take a look at NModel.

Now why in Fixed parameter tractable problems you need to work with logic, You can divide classes of Fixed parameter tractability with different levels of logic, they can be converted to each other : logic to automata, automata to graph, and vice verse, But if you be an expert in logic you can divide and decide on them simply, most important theorem (after Robertson and Seymour theorem), in this field is Courcelle's theorem. for more information read Meta Algorithmic Theorem survey.