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

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 ...
10
votes
1answer
5k views

DNF to CNF conversion: Easy or Hard

In relation to the thread Proving that the conversion from CNF to DNF is NP-Hard (and a related Math thread): How about the other direction, from DNF to CNF? Is it easy or hard? On Page 2 of this ...
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 ...
4
votes
2answers
225 views

Creating a logical circuit

Task: Design a 2 bit comparator. Input: 2x 2 bit (I take it as 2 2-bit values, let them be unsigned for simplicity) Output: 1 if result input1>input2 is true, 0 otherwise Develop truth table and ...
4
votes
1answer
90 views

First Order interpretation of arbitrary structures as a graph

I am currently trying to get some intuition on the concept of First Order reductions, and have come across this exercise question by Immerman, dubbed "Everything is a Graph". Given some arbitrary ...
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 ...
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 ...
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{\...
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 (...
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. ...
10
votes
3answers
646 views

Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
2
votes
1answer
100 views

What is the set of all minimal 3CNF formulas?

Definition: A minimal 3CNF formula is an unsatisfiable 3CNF formula with minimum clauses connected by conjunctions, where each clause is disjunction of 3 literals, that is if any of it's clauses is ...
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 ...
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 ...
1
vote
2answers
8k views

Operator precedence in propositional logic

there is some kind of priorities for the elements in propositional logic ? for example : p ∧¬q → r , given this ,we there may be two options (p ∧¬q) → r OR p ∧ (¬q → r) , which one is the correct ?...
2
votes
0answers
193 views

Difference between fully-reduced BDD and quasi-reduced BDD

I am trying to figure out difference between fully- and quasi-reduced BDDs. I have read a lot of material but still it is not very clear. As I am trying to figure out the quasi reduced version for ...
2
votes
1answer
1k views

Negation of nested quantifiers

The problem is: $$\exists x \forall y (x \ge y)$$ With a domain of all real positive integers. The negation is: $$\forall x \exists y (x < y)$$ so, if $y = x + 1$, the negation is true. That ...
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. ...
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 ...
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 ...
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))\...
8
votes
2answers
704 views

Why doesn't Godel's Second Incompleteness Theorem rule out a formalizable proof of P!=NP?

I'm sure there must be something wrong with the following reasoning because otherwise a lot of P vs. NP research would be curtailed but I cannot determine my error: For any fixed integer $k>0$ ...
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 ...
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,...
6
votes
2answers
176 views

Is there a relationship between “sound and complete” in logic and “type safety” in PLs?

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are ...
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 ...
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$...
6
votes
2answers
4k views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
4
votes
1answer
2k views

Consistency and completeness imply soundness?

I understand that soundness implies consistency. Also, I understand that consistency alone does not imply soundness. But shouldn't consistency + completeness imply soundness? Scott Aaronson in his ...
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 ...
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 ...
7
votes
1answer
476 views

Algorithm for deciding alpha-equivalence of terms in languages with bindings

I am interested in the alpha equivalence relation in languages with variable bindings, such as: ...
6
votes
3answers
3k views

Is resolution complete or only refutation-complete?

Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77. There it is mentioned that "the procedure is also complete". I think this ...
7
votes
3answers
358 views

What is wrong with this seeming contradiction with a paper about AND-compression of SAT?

Got a simple construction seemingly contradicting a paper assuming plausible conjecture. Since it is unlikely the conjecture to be false, what is wrong with the argument? From a paper An AND-...
4
votes
1answer
1k views

Propositional formula in DNF can be decided in polynomial time?

For a given propositional formula f in DNF, one can decide in polynomial time, if the formula is satisfiable: Just walk through all subformulas (l_1 and ... and l_k) and check, wheter it has NO ...
4
votes
1answer
86 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
2
votes
1answer
250 views

Normal order sequencing vs applicative order sequencing

I'm trying to understand this lecture, section 2.7. Why would the normal order sequencing print out "hello" "world" and not ...
2
votes
0answers
122 views

Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
1
vote
1answer
32 views

What is the largest possible minimal 3CNF formula as function of the number of variables?

I have already defined here what is minimal 3CNF formula. In the answer to the question, D.W. answered: What you are thinking is wrong. A minimal, unsatisfiable formula can have more than 8 clauses. ...
1
vote
1answer
325 views

Is this possible to solve boolean satisfiablility by using karnaugh maps to simplify the whole given boolean formula by simplifying subformulas?

Building karnaugh map for the whole given boolean formula always costs Θ(2n) both time and space complexities, where $n$ is the number of boolean variables in the given boolean formula. It is ...
0
votes
1answer
251 views

Convert conjunctive normal form to equivalent boolean formula with only NAND gates

Let $\varphi$ be a boolean formula in 3-CNF form (conjunctive normal form with three literals at most per clause). I want to convert it to an equivalent boolean formula that uses only NAND gates with ...
3
votes
2answers
102 views

What does “refuting random 3CNF” formulas mean?

Intuitively, recall what 3CNF formulas mean: Its a boolean formula with conjunctive normal form (i.e. formula of ANDs of clauses with ORs) with no more than three variables per conjunct. I was ...
3
votes
0answers
113 views

Higher order verification in a complete logic

I'd like to design a language that is able to reason over itseslf, means, able to get as input a code in that language (that might have went through some external redundant preprocessing, or "...
3
votes
1answer
67 views

Can a propositional threshold connective be expressed by standard connectives?

We are given a finite set of propositional atoms $\{x_1, \dots, x_n\}$ and an integer $k$. Can we capture through a propositional formula $\varphi$ (built from the standard connectives $\neg, \wedge, \...
2
votes
2answers
163 views

Someone explain the venn diagram for the logic equation A*(B+C)

So, I am studying logic circuits and how to prove them with Venn diagrams. When drawing a Venn diagram for the equation A*(B+C) I figured it would look something like this: But according to the ...
2
votes
1answer
362 views

Transition systems that satisfy LTL but not CTL, and vice versa

I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...
2
votes
0answers
153 views

on `On the cruelty of really teaching computing science' [closed]

Dijkstra, in his essay On the cruelty of really teaching computing science, makes the following proposal for an introductory programming course: On the one hand, we teach what looks like the ...
1
vote
0answers
104 views

Logical formula in DIMACS, SAT, Schaefer's dichotomy theorem and software to test it

I have a very complicated formula logical (CNF) in the file DIMACS. The question is as follows. The formula has hundreds of millions of clauses (assume billion) and a lot of variables. It is a ...
1
vote
1answer
4k views

Drawing an implication graph for 2-SAT clauses

I am trying to convert the following 2-sat clauses to implications and then draw the implication graph. The clauses are: ...