<p>I understand the significance of the theory of comptuation, for example NP-hardness of a problem signals us to forget about implementing it's exact solution and rather try approximating it.</p>

<p>In the similar fashion, I am not able to get intuition of how to bridge the theory and practical aspects of the course "Logic in Computer Science". Let's say, some problem does not belong to Predicate or First-order logic, and that can be rather modeled by LTL or CTL. So what does that signify?</p>

<p>Any links or pointers will be helpful. Thanks in advance.</p>

CC BY-SA 3.0
2013-11-23T14:38:16.550Z
Hi and welcome to CSTheory! This site is oriented towards research-level questions. You can consult the [FAQ](http://cstheory.stackexchange.com/about) for more information on what is meant by this and suggestions for sites that might welcome your question. 

In your case, did you use a proof assistant (e.g. Coq) in the lecture? Have you brought this question to the lecturer and perhaps check his group's website to see what other courses are offered?
chazisop
CC BY-SA 3.0
2013-11-23T20:20:51.917Z
Actually, LTL/CTL could be encoded In first-order logic. However, these logics are useful for expressing certain types of problems in a more direct way. Further, problems in CTL/LTL can be decided by an algorithm, which is not the case for first order logic. If you're looking for motivation for temporal logic, see how they apply to model checking.
Mikolas
CC BY-SA 3.0
2013-11-24T09:35:29.893Z
See the section "Logic in Computer Science" by Sam Buss in "[The prospects for mathematical logic in the twenty-first century](http://arxiv.org/abs/cs/0205003)".
Kaveh
<cc.complexity-theory><lo.logic>
Significance of Logic in Computer Science
user2436425
# Significance of Logic in Computer Science

(Asked by: username_0 on 2013-11-23)

I understand the significance of the theory of comptuation, for example NP-hardness of a problem signals us to forget about implementing it's exact solution and rather try approximating it.

In the similar fashion, I am not able to get intuition of how to bridge the theory and practical aspects of the course "Logic in Computer Science". Let's say, some problem does not belong to Predicate or First-order logic, and that can be rather modeled by LTL or CTL. So what does that signify?

Any links or pointers will be helpful. Thanks in advance.

**Tags:** cc.complexity-theory, lo.logic

> **Comments:**
> **username_1**: Hi and welcome to CSTheory! This site is oriented towards research-level questions. You can consult the [FAQ](http://cstheory.stackexchange.com/about) for more information on what is meant by this and suggestions for sites that might welcome your question.   In your case, did you use a proof assistant (e.g. Coq) in the lecture? Have you brought this question to the lecturer and perhaps check his group's website to see what other courses are offered?  
> **username_2**: Actually, LTL/CTL could be encoded In first-order logic. However, these logics are useful for expressing certain types of problems in a more direct way. Further, problems in CTL/LTL can be decided by an algorithm, which is not the case for first order logic. If you're looking for motivation for temporal logic, see how they apply to model checking.  
> **username_3**: See the section "Logic in Computer Science" by Sam Buss in "[The prospects for mathematical logic in the twenty-first century](http://arxiv.org/abs/cs/0205003)".  

---

## 0 answers

