New answers tagged propositional-logic
3
Let me explain what is going on here by way of an example:
$$
\psi(p_0,p_1,p) = p \leftrightarrow (p_0 \land p_1).
$$
That is, $\psi(p_0,p_1,p)$ is true iff $p = p_0 \land p_1$.
If you define
$$
\phi(p_0,p_1) = p_0 \land p_1,
$$
then we indeed have
$$
\psi(p_0,p_1,p) \to (\phi(p_0,p_1) \leftrightarrow p),
$$
which means that if $\psi(p_0,p_1,p)$ holds then $...
1
This problem sounds quite abstract and I'll sketch a proof below. To prove the final material conditional is a tautology, we only need to prove $\psi(p_0, \ldots p_n, p) \wedge \psi(p_0, \ldots p_n, q) \land \lnot (p \leftrightarrow q)$ is unsatisfiable, which means it can never be the case that $p,q$ can have opposite truth values while both $\psi(p_0, \...
0
I'll add some steps to make it very clear. You want to prove q.
You can take any statement s, then say "either s or not s is true", and then prove "if s is true then q is true" and "if not s is true then q is true". That happens actually quite often; you might have the statement "x ≤ 1" and you can prove that if x ≤ 1 ...
2
There is no problem with assuming $ \neg q$ towards a contradiction and showing that this implies $q$.
Here is an example, adapted from Euclid's proof that there are infinitely many primes.
Let $p$ be a prime number and suppose we want to prove "there exists a prime number larger than $p$".
We proceed by contradiction, i.e., we assume that "...
1
We like conjunctive normal form because all circuits can be transformed into conjunctive normal from in linear time via the Tseitin Transformation. It's a clean, normalized data structure for solver implementation. CNF conversion without Tseitin variables may lead to exponential expansion.
That's the standard answer, but, as you see, there are nuances. ...
6
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 appears in a follow-up work of Davis, Logemann, and Loveland, and is the basis of all modern SAT solvers). They explain that one key property of CNF is that any ...
4
It's because this is close to how real-world problems tend to be expressed.
SAT has a lot of practical applications, from controlling power grids to integrated circuit layout. In pretty much every case, the problem is that you have a bunch of complex constraints that all need to be satisfied.
However you express each constraint, they ultimately get joined ...
2
First of all in your above 3 "recursive definitions" linking $\Sigma$ with $\Sigma_2$, clearly the function $g$ in $\Sigma_2$ doesn't have any role in defining the values of $f(t)$ in $\Sigma$, the values of $f(t)$ should be already defined in language $\Sigma$.
To check your 3 "recursive definitions" more deeply, it seems here the map ...
Top 50 recent answers are included