# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

828 questions
Filter by
Sorted by
Tagged with
14k views

### Is there any concrete relation between Gödel's incompleteness theorem, the halting problem and universal Turing machines?

I've always thought vaguely that the answer to the above question was affirmative along the following lines. Gödel's incompleteness theorem and the undecidability of the halting problem both being ...
9k views

### What is coinduction?

I've heard of (structural) induction. It allows you to build up finite structures from smaller ones and gives you proof principles for reasoning about such structures. The idea is clear enough. But ...
9k views

### Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...
6k views

### What exactly is a logic?

An apology might be in due for asking another question about prerequisites, but I was confused about the starting points. I have come across various terms such as "Modal Logic", "Temporal logic", "...
4k views

### Intro to Martin-Löf type theory

What would be the best introduction to Per Martin-Löfs ideas about type theory? I've looked at some lectures from the Oregon PL summer school, but I'm still sort of puzzled by the following question: ...
1k views

### Equivalence of Büchi automata and linear $\mu$-calculus

It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
5k views

395 views

### “Famous logicians have made embarrassing errors here,” a line from SICP. What is this referring to?

Here is the context (Structure and Interpretation of Computer Programs, section 1.1.8, under heading "Local names"): A formal parameter of a procedure has a very special role in the procedure ...
679 views

### Type inference with product types

I’m working on a compiler for a concatenative language and would like to add type inference support. I understand Hindley–Milner, but I’ve been learning the type theory as I go, so I’m unsure of how ...
11k views

### Reason to learn propositional & predicate logic

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

### Confluence proof for a simple rewriting system

Assume we have a simple language that consists of the terms: $\mathtt{true}$ $\mathtt{false}$ if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ ...
965 views

### Monadic Second Order Logic for Dummies

I am programmer with a grip on automata, but not on logic. I read in papers that the two are very tightly related. Deterministic Finite Automata (DFA), Tree Automata and Visibly Pushdown Automata are ...
423 views

### What do we gain by having “dependent types”?

I thought I understood dependent typing (DT) properly, but the answer to this question: https://cstheory.stackexchange.com/questions/30651/why-was-there-a-need-for-martin-l%C3%B6f-to-create-...
7k views

### Intuition behind the Hadamard gate

I'm trying to teach myself about quantum computing, and I have a decent-ish understanding of linear algebra. I got through the NOT gate, which wasn't too bad, but then I got to the Hadamard gate. ...
922 views

### Testing whether an arbitrary proof is circular?

I was thinking about proofs and ran into an interesting observation. So proofs are equivalent to programs via the Curry-Howard Isomorphism, and circular proofs correspond to infinite recursion. But we ...
3k views

### Is this a generic way to convert any recursive procedure to tail-recursion?

It seems that I've found a generic way to convert any recursive procedure to tail-recursion: Define a helper sub-procedure with an extra "result" parameter. Apply what would be applied to the ...
3k views

### Why does soundness imply consistency?

I was reading the question Consistency and completeness imply soundness? and the first statement in it says: I understand that soundness implies consistency. Which I was quite puzzled about ...
2k views

### What is a “contradiction” in constructive logic?

In Practical Foundations for Programming Languages, Robert Harper says If for a proposition to be true means to have a proof of it, what does it mean for a proposition to be false? It means that we ...
2k views

### Proving tautology with coq

Currently I have to learn Coq and don't know how to deal with an or : As an example, as simple as it is, I don't see how to prove: ...
540 views

### The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
804 views

### Is there a difference between $\lambda xy.xy$ and $\lambda x.\lambda y.xy$?

I am currently learning the lambda calculus and was wondering about the following two different kinds of writing a lambda term. $\lambda xy.xy$ $\lambda x.\lambda y.xy$ Is there any difference in ...
850 views

### Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
### Why use $\mu$-calculus and not LTL,CTL,CTL*?
It is known that the temporal logics LTL,CTL,CTL* can be translated/embedded into the $\mu$-calculus. In other words, the (modal) $\mu$-calculus subsumes these logics, (i.e. it is more expressive.) ...