# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

66 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
8k 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 ...
262 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 ...
97 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 ...
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 ...
1k 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 ...
811 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$ ...
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 ...
15k 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 (...
652 views

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{\... 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. ... 3answers 831 views ### Polymorphism and Inductive datatypes I'm curious. I've been working on this datatype in OCaml: ... 2answers 647 views ### What is the Curry-Howard analogue for linear logics? As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ... 3answers 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 ... 1answer 144 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 ... 1answer 2k 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 ... 2answers 11k 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 ?... 0answers 226 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 ... 1answer 2k 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 ... 4answers 5k 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. ... 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 ... 3answers 3k 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 ... 1answer 1k 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 ... 2answers 12k 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))\... 2answers 403 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,... 2answers 277 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 ... 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 ... 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... 3answers 4k 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 ... 2answers 5k views ### Understanding DPLL algorithm I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ... 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 ... 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 ... 1answer 705 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: ... 3answers 397 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-... 2answers 69 views ### Equivalence of Krom formulas tractable? Assume I have two Krom formulas \psi_1, \psi_2. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, \... 2answers 2k views ### Language to define perfectly a programming problem Is there any language, which can be used to define all programming problems perfectly? By perfectly, I mean with these two properties: p is the problem. d is the definition in the language. P(d, p): ... 1answer 2k 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 ... 1answer 98 views ### Developing invariants for comparing two strings The following algorithm is supposed to compare two strings S_1 and S_2 ("/\" for empty string): ... 3answers 151 views ### Are regular languages and their regular expressions part of computer science? I am trying to understand if regular languages and their regular expressions are concepts of computer science in general and if these are discovered, or invented, by computer scientists, in particular.... 1answer 320 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 ... 0answers 195 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 ... 1answer 40 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. ... 1answer 569 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 ... 1answer 478 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 ... 1answer 265 views ### Redundancy elimination in the superposition calculus When proving theorems with the superposition calculus, we deal with three kinds of rules: Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. ... 3answers 1k views ### Hoare triple for assignment P{x/E} x:=E {P} I am trying to understand Hoare logic presented at Wikipedia, Hoare logic at Wikipedia Apparently, if I understand correctly, a Hoare triple$$\{P\}~ C ~\{Q\} means if P just before C, then Q ...
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, \...