# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

695 questions
12k 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 ...
7k 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 ...
8k 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 ...
5k 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", "...
3k 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: ...
921 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 ...
565 views

951 views

### Types of Automated Theorem Provers

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Which are the relevant automated theorem provers? I ...
5k views

### Can proof by contradiction work without the law of excluded middle?

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
8k views

### What is an intuitive way to explain and understand De Morgan's Law?

De Morgan's Law is often introduced in an introductory mathematics for computer science course, and I often see it as a way to turn statements from AND to OR by negating terms. Is there a more ...
2k views

### How to read typing rules?

I started reading more and more language research papers. I find it very interesting and a good way to learn more about programming in general. However, there usually comes a section where I always ...
3k views

### Can constraint satisfaction problems be solved with Prolog?

Is "party attendance" type of problems solvable in Prolog? For example: Burdock Muldoon and Carlotta Pinkstone both said they would come if Albus Dumbledore came. Albus Dumbledore and Daisy ...
353 views

### Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
358 views

### Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ACL2,...
113 views

### Methods to evaluate a system of written rules

I was trying to come up with a system that would evaluate bylaws for an organization as to determine their underlying logic. I think a first-order predicate system would work for representing the ...
623 views

### Is there a repository for the hierarchy of proofs?

I am self-learning proof assistants and decided to start on some basic proofs and work my way up. Since proofs are based on other proofs and so form a hierarchy, is there a repository of the hierarchy ...
825 views

### Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
3k views

### Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
575 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 ...
152k views

### How to construct XOR gate using only 4 NAND gate?

xor gate, now I need to construct this gate using only 4 nand gate ...
795 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$ ...
10k 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 ...
12k views

### What's an example of an unsatisfiable 3-CNF formula?

I'm trying to wrap my head around an NP-completeness proof which seem to revolve around SAT/3CNF-SAT. Maybe it's the late hour but I'm afraid I can't think of a 3CNF formula that cannot be satisfied (...
10k views

418 views

### Introductory book on Logic and Computation

Can you give me some suggestions about a good introductory (but comprehensive) bookabout Logic and Computation? Some fuzzy topics that I have in mind are: Presburger artihm., PA, ZF, ZFC, HOL Set ...
3k views

### Example of Soundness & Completeness of Inference

Is the following example correct about whether an inference algorithm is sound and complete? Suppose we have needles a, b, c in a haystack, and have also an inference algorithm that is designed to ...
482 views

### Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: <...
695 views

### Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...