Share Your Experience: Take the 2024 Developer Survey

# Tag Info

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

I find pictures are great for anything simple enough to use them, which this is. Remember: AND means the area taken up by both things. So the middle one is what is taken up outside B, but also ...
• 511

• 203
Accepted

### Does mutual exclusion hold in this case?

Your friend is correct. In your context, mutual exclusion holds if at most one process is at a critical section at any given time. You state that you feel that this interpretation is wrong, but you ...
• 278k
Accepted

### Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

Proofs in Haskell? Okay, first let's talk about the Curry-Howard correspondence. This says that one can view theorems as types and proofs as programs. However, it says nothing about which specific ...
• 29.8k

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

I think your question boils down to "when doing formal verification with some sort of formal logic, what sort of guarantee do I have that the logic is consistent?". And the answer is: none. That's ...
• 161k

### I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false

A phrase like "it is not possible to encode product types in the simply-typed $\lambda$-calculus (without product types)" means: it is not true that for every type $A$ and type $B$, there ...
• 661

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

Let's take an example. Suppose that we want to express that $a$ is the only element of the set $S$ that satisfies property $P$. Then we can write $$\forall x \in S \;\; P(x) \Rightarrow x = a$$ This ...
• 278k
Accepted

### Deciding which logical proposition is stronger

The notion of strength of a proposition comes from its power to constrain the model. For instance the proposition $P1 : x = 2$ is stronger than $P2 : x \geq 2$ in Arithmetic. And in propositional ...
• 1,409
Accepted

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

"arbitrary chosen" in a NP problem where the followup results in a P algorithm typically means that the choice matters a lot and trying them all and backtracking over bad choices looking for the ...
• 4,426
Accepted

### Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?

The fact of the matter is, if a proof exists, then a Curry-Howard version of the program exists too. That doesn't mean that it's easy to find, though. Undecidability still holds for Curry-Howard: if ...
• 29.8k

### Why is SAT based on the CNF?

Conjunctive normal form first appears, in this context, in Davis and Putnam's A computing procedure for quantification theory, in which they describe a primitive form of the DPLL algorithm (which ...
• 278k
Accepted

### Why is learning DNF harder than learning CNF?

It's important to distinguish between $k$-CNF and CNF. A $k$-CNF formula is a CNF formula where every clauses has at most $k$ literals; a CNF formula has no limit on the number of literals in each ...
• 161k
Accepted

### How to find a minimum set of axioms within a set of propositions?

Determining whether a proposition follows from a set of axioms is an NP-Complete problem. Finding a minimal set of axioms from a set of propositions naturally invokes this problem many times as a ...
• 4,312
Accepted

### Contingent sentences can always be true

In mathematical logic - the discipline of logic that has interested computer scientists the most - there is a difference between proof-theoretic truth and model-theoretic truth. Beyond metaphor (of ...
• 3,276
Accepted

### "Implied atomic propositions" in propositional boolean formula

Suppose we had a TM $M$ which, given $F$ and some atomic $A$ occurring in $F$ it can efficiently (PTIME) decide whether all models of $F$ make $A$ true, i.e. whether $F \models A$. Then we can ...
• 14.6k

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

Note that, when we know that $C$ implies $D$, we have $C \lor D = D$. This is analogous to taking the union of a set (corresponding to $D$) and one of its subsets ($C$): we get the largest set ($D$) ...
• 14.6k
Accepted

### What is the connection between combinatorial circuits and finite state automata?

You can associate with a combinatorial circuit with $n$ inputs and a single output the language consisting of the $n$-bit strings on which the circuit outputs $1$. This language is finite and so, in ...
• 278k
Accepted

### Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?

There is a preprocessing method called vivification$^1$ that can be used to detect subsumed clauses. It relies on unit propagation to work. To vivify a clause, make a partial variable assignment ...
• 8,091