# 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 ...
• 276k

### 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 ...
• 158k

### 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 ...
• 276k
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,396
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.7k
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.7k

### 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 ...
• 276k
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,282
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

### 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 ...
• 158k
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.5k

### 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.5k
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 ...
• 276k
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,071
Accepted

### Can this set of propositions be represented and proved in Haskell?

Your Haskell encoding fails to capture proofs in propositional calculus (which is what the book you referred to does). The failure is not due to your using Haskell, but because of your encoding ...
• 30.3k