Hot answers tagged

13 votes
Accepted

Representing binary functions with a finite gate set without exponential blow-up?

No. No matter what representation of functions as circuits/formulas you use, there will exist some functions that require exponential size to represent. This was proven by Shannon in 1949. See ...
D.W.'s user avatar
  • 158k
11 votes

Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

No, it doesn't require that. These are two orthogonal issues. You can easily define a new programming language where you provide fully defined semantics for all operations; yet it can be Turing ...
D.W.'s user avatar
  • 158k
7 votes

Curry-Howard isomorphism and non-constructive logic

I think people sometimes disagree on what exactly Curry-Howard is. But, one way to look at it is an exact correspondence between the syntactic rules for logic and for type theory. For the ...
Dan Doel's user avatar
  • 2,639
6 votes
Accepted

SAT formulation of the condition that an even number of a given set of variables must be set to true

Let $\oplus$ be XOR, then your question is asking for $\bigoplus_{k=1}^n x_k = 0$. We can encode this efficiently without an exponential explosion in clauses by introducing new variables. The basic ...
orlp's user avatar
  • 12.9k
4 votes

Are recursive Horn clauses first order?

Horn clauses in prolog are not recursive definitions. They are logical formulas. For example, times(_, 0, 0). times(x, S(y), w) :- times(x,y,z), plus(x,z,w). is ...
Andrej Bauer's user avatar
  • 30.3k
4 votes

Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

Your intuition is incorrect. The analogies you're trying to draw are not there, even though it's understandable you would expect them. Programming languages can be defined as formal systems, but they ...
Andrej Bauer's user avatar
  • 30.3k
4 votes
Accepted

Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$

What prevents me from treating the bottom part as if it was "$-\varphi \land \Gamma \implies \Delta$"? Nothing prevents you! In fact, this is exactly the right idea. You can think of the ...
Caleb Stanford's user avatar
4 votes
Accepted

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
4 votes

What is practically preventing us from applying set-theoretic types in engineering?

Let me first answer the easy part. The negation sign in the judgement a : ¬ A does not modify : but ...
Andrej Bauer's user avatar
  • 30.3k
3 votes

Curry-Howard isomorphism and non-constructive logic

The Curry-Howard correspondence is not crucial for functioning of a proof assistant. Unforunately, the term "Curry-Howard correspondence" seems to be misused nowadays for all sorts of things....
Andrej Bauer's user avatar
  • 30.3k
3 votes

Curry-Howard isomorphism and non-constructive logic

While proof assistants typically use constructive mathematics, the Curry-Howard-Correspondence does not necessarily require constructivism. The important aspect of the correspondence is that the ...
NaCl's user avatar
  • 131
3 votes
Accepted

Is any 2-CNF has 2-DNF representation?

How about $\phi = (x_1 \vee x_2) \wedge (x_1 \vee x_3) \wedge (x_1 \vee x_4)$? This formula is satisfied iff $x_1$ is true, or $x_2$, $x_3$, and $x_4$ are all true. Suppose that $\phi$ had a $2$-DNF ...
Steven's user avatar
  • 29.3k
3 votes
Accepted

Is finding a Polytime reduction from $L_1$ to $L_2$ equivalent to proving $L_2 \in P \Rightarrow L_1 \in P$

No, this only works one way. If there is a polynomial time reduction from $A$ to $B$, then $B \in P \implies A \in P$. This works irrespective of the what kind of languages $A$ and $B$ are. The ...
1001's user avatar
  • 211
3 votes
Accepted

What is the difference in heap configurations? Separation logic with CVC5 SMT solver

Thanks for the question. The model construction for the separation logic heap in cvc5 was wrong in this case. This will be fixed by https://github.com/cvc5/cvc5/pull/9574.
Andrew Reynolds's user avatar
2 votes
Accepted

Complexity of a Set of Formulas

Yes. You can build a Boolean circuit $\beta_n$ of size $O(n \lg n)$, that is equivalent to $\alpha_n$. It works by counting the number of "true"s among the inputs, compares it to $n$, and ...
D.W.'s user avatar
  • 158k
2 votes

Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

The incompleteness theorem only applies to formal systems that can express a certain amount of arithmetic. In particular, they have to support statements of the form $\forall n\in\mathbb N. P(n)$, ...
benrg's user avatar
  • 2,112
2 votes
Accepted

How to express that a graph has Independent set of size at least $n/2$ in $\exists SO$

One way to see it is to notice that asking for $|X|\ge n/2$ is the same as asking that $X$ is bigger than $V(G)\setminus X$, which can be witnessed by an injection from $V(G)\setminus X$ to $X$. Thus, ...
pasthec's user avatar
  • 291
2 votes
Accepted

Defining 2 inductive propositions relying on each other in Coq

You can use mutually defined inductive types, using the with construct. Here is the standard simple example on how to do that: ...
Meven Lennon-Bertrand's user avatar
2 votes

Is there a 2SAT encoding for a NAND gate

It seems, based on the comments in other answers, that what you are after is a 2-CNF formula $\phi(q, a, b)$ equivalent to $q \iff \overline{a \land b}$. This is indeed not possible; the only possible ...
Bernardo Subercaseaux's user avatar
2 votes
Accepted

how to do incremental construction of the minimal model in logic programming?

this paragraph describes the immediate consequences operator $T_P(I) = \{ a \mid \text{there exists a rule } r \in G(P) \text{ with } head(r)=a \text{ and } body(r) \subseteq I \}$ for some ...
jt0202's user avatar
  • 171
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,154
2 votes

What is "the ability of classical control operators to return multiple times from a single term"?

The control operators in question allow you to capture continuations such that calling the continuation is in some sense equivalent to "returning from" the expression. so, for instance, in (...
Dan Doel's user avatar
  • 2,639
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
  • 158k
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
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,089
1 vote

Is there a 2SAT encoding for a NAND gate

There is no proof that it is impossible, but it is believed that it's unlikely to be possible, because if you could convert every circuit with NAND gates to 2CNF, you would have a proof that P = ...
D.W.'s user avatar
  • 158k
1 vote

Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic

Both Kripke semantics and propositions-as-types interpretation are sound and complete for the intuitionistic propositional calculus. In this sense they are equivalent. However, there are formulas in ...
Andrej Bauer's user avatar
  • 30.3k
1 vote
Accepted

SAT polynomial time

In general, asymptotic complexity concerns itself with the size of the input. In this case, the number of input symbols. SAT is thus not polynomially solvable in the worst case as a function of the ...
ADdV's user avatar
  • 277
1 vote

Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite

This is Exercise 83 in Schöning's book "Logic for Computer Scientists". Similarly, the solution to this problem can be found in the original paper of Robinson. He gives an example with ...
user1868607's user avatar
  • 2,194

Only top scored, non community-wiki answers of a minimum length are eligible