New answers tagged logic
0
votes
Accepted
(Co)-induction, fixpoints and inference systems
Intuitively, you can see that $F_\Phi(X)$ is monotone in $X$ by carefully looking at the body of the definition
$$ \exists (H, c)\in \Psi,\ H\subseteq X$$
If there is an $H, c$ with $H\subseteq X$, ...
- 8,114
0
votes
Accepted
Complexity of satisfiability for relational logic on the booleans
In NP I could guess the disjunctive normal form of the formulas, that would look like
$\bigwedge_i R_i(x_1^i, \ldots, x_{n(i)}^i) \land \bigwedge_j \lnot R_j(x_1^j, \ldots, x_{m(j)}^j)$
The question ...
- 2,184
1
vote
Complexity of satisfiability for relational logic on the booleans
Nothing much changes. Every relation $R(x_1,\dots,x_n)$ is equivalent to $\exists t_1,\dots,t_m . \varphi(x_1,\dots,x_n,t_1,\dots,t_m)$ for some fresh variables $t_1,\dots,t_m$ (see the Tseitin ...
D.W.♦
- 156k
1
vote
DFA for even concatenation of strings from a language
The language you are considering is $(W^2)^*$, so you could combine standard constructions for the concatenation and the star operation.
- 6,014
0
votes
Is there an algorithm to detect race conditions in logic circuits?
Let’s say somewhere in your circuit there is a logical AND calculating a AND b. Now as you change the inputs that change will move through your circuit and change things.
a and b start with a certain ...
- 28.3k
0
votes
3 bit binary multiplier?
For an n-bit by n-bit multiplier you use $n^2$ ANDs which each give a single bit in some bit position. For example in a 64 bit multiplier $x_{52} and $y_{22} would be a bit in position 74.
You arrange ...
- 28.3k
0
votes
Is there a model for the given logical formula, and if not, why?
Be lazy: encode your problem in the input language of your favourite SAT solver and feed the resultung term to it. If it answers "SAT" it'll also provide a model. If not, then there's no ...
- 663
1
vote
Accepted
Is there a model for the given logical formula, and if not, why?
Set all variables to false, that way each implication has a false left-hand-side and thus it's satisfied.
- 1,188
4
votes
What is practically preventing us from applying set-theoretic types in engineering?
Negation is certainly possible in these systems. It's discussed in the best introductory materials, in particular:
https://www.irif.fr/~gc/papers/covcon-again.pdf
https://pnwamk.github.io/sst-tutorial/...
2
votes
What is practically preventing us from applying set-theoretic types in engineering?
Generally, and to build upon this discussion, there is plenty of work which describes types exactly as you'd like, that is as a collection of "values" of a certain shape, with natural set ...
- 8,114
Top 50 recent answers are included