New answers tagged

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$, ...
cody's user avatar
  • 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 ...
user1868607's user avatar
  • 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.'s user avatar
  • 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.
J.-E. Pin's user avatar
  • 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 ...
gnasher729's user avatar
  • 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 ...
gnasher729's user avatar
  • 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 ...
Kai's user avatar
  • 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.
Bernardo Subercaseaux's user avatar
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/...
Sam Tobin-Hochstadt's user avatar
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 ...
cody's user avatar
  • 8,114

Top 50 recent answers are included