Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

71
votes
5answers
11k 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 ...
63
votes
2answers
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 ...
42
votes
6answers
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 ...
35
votes
3answers
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", "...
35
votes
3answers
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: ...
29
votes
2answers
898 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 ...
28
votes
2answers
539 views

Characterization of lambda-terms that have union types

Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping): $$ \dfrac{\...
27
votes
4answers
4k views

Clear, intuitive derivation of the fixed-point combinator (Y combinator)?

The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as: FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. ...
25
votes
1answer
972 views

Is there a typed SKI calculus?

Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the ...
22
votes
7answers
7k views

Why is A implies B true if A is false and B is false?

It seems to me that the 'implies' in English language does not mean the same thing as the logical operator 'implies', in a similar way how 'OR' word in most cases means 'Exclusive OR' in our everyday ...
22
votes
5answers
968 views

$\lambda$-calculus with reflection

I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs. Is there an untyped $\lambda$-calculus extension that ...
22
votes
4answers
1k views

Do undecidable languages exist in constructivist logic?

Constructivist logic is a system which removes the Law of the Excluded Middle, as well as Double Negation, as axioms. It's described on Wikipedia here and here. In particular, the system doesn't ...
21
votes
11answers
4k views

Why is $A \lor (A \land \neg B) \equiv A$?

I would like to know if there is a rule to prove this. For example, if I use the distributive law I will get only $(A \lor A) \land (A \lor \neg B)$.
20
votes
2answers
5k views

Is it possible to write an AND gate using XOR gates?

How could I express an AND gate using only XOR gates ?
20
votes
2answers
2k views

What is beta equivalence?

In the script I am currently reading on the lambda calculus, beta equivalence is defined as this: The $\beta$-equivalence $\equiv_\beta$ is the smallest equivalence that contains $\rightarrow_\beta$...
20
votes
2answers
2k views

Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
19
votes
3answers
1k views

Similarities and differences in major process algebras

To my knowledge, there are three major process algebras that have inspired a vast range of research into formal models of concurrency. These are: CCS and $\pi$-calculus both by Robin Milner CSP by ...
19
votes
2answers
598 views

Are universal types a sub-type, or special case, of existential types?

I would like to know whether a universally-quantified type $T_a$: $$T_a = \forall X: \left\{ a\in X,f:X→\{T, F\} \right\}$$ is a sub-type, or special case, of an existentially-quantified type $T_e$ ...
19
votes
1answer
922 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 ...
18
votes
4answers
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 ...
18
votes
3answers
7k 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 ...
17
votes
3answers
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 ...
17
votes
3answers
2k 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 ...
16
votes
4answers
350 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 ...
16
votes
2answers
354 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,...
16
votes
1answer
112 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 ...
15
votes
2answers
772 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 ...
15
votes
3answers
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. ...
14
votes
4answers
606 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 ...
14
votes
7answers
144k 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 ...
14
votes
2answers
780 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$ ...
14
votes
1answer
559 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 ...
13
votes
1answer
285 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 ...
13
votes
1answer
403 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 ...
12
votes
5answers
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 ...
12
votes
2answers
11k 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 (...
12
votes
5answers
2k 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 ...
12
votes
2answers
1k 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 ...
12
votes
2answers
316 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-...
12
votes
2answers
10k views

“Applicative order” and “Normal order” in lambda-calculus

Applicative order: Always fully evaluate the arguments of a function before evaluating the function itself , like - $(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x. x^2(2+1))\...
12
votes
2answers
1k 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: ...
12
votes
1answer
892 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 ...
12
votes
1answer
1k 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 ...
11
votes
3answers
644 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 ...
11
votes
2answers
198 views

CCS process for a drink dispenser with two different prices

A drink dispenser requires the user to insert a coin ($\bar c$), then press one of three buttons: $\bar d_{\text{tea}}$ requests a cup of tea $e_{\text{tea}}$, ditto for coffee, and $\bar r$ requests ...
11
votes
3answers
378 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 ...
11
votes
1answer
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 ...
11
votes
1answer
453 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: <...
11
votes
1answer
300 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 ...
10
votes
3answers
646 views

Polymorphism and Inductive datatypes

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