# Tag Info

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 ...
• 162k

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

### 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 ...
• 2,707
Accepted

### Can the minimisation operation be seen from a programming language perspective?

Is there a similar way in which the minimisation operation can be understood? More specifically, does minimisation correspond to some kind of "loop" found in programming languages? Yes, ...
• 246

### P=NP? A reduction of CNF boolean satisfiability to the circulation problem in an undirected graph

Consider the CNF formula $a \wedge \neg a$. This has two clauses, $a$, and $\neg a$. If I understand your scheme correctly this maps to the following flow problem: This clearly has a solution (1 flow ...
• 13.6k
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 ...
• 13.6k

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

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

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

### Can CTL* express every model's behaviour

First of all, for every transition system M, there indeed exists a CTL* formula Φ such that M ⊨ Φ holds, namely the CTL* formula "true". What you may have wanted to express is the question ...
• 2,797

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

### 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 ...
• 131
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, ...
• 301
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: ...

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

For propositional logic, you're probably right. As far as quantifier logic goes: the Curry-Howard correspondence never included quantifiers and there isn't really any consensus or standard treatment ...
• 349

### 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)$, ...
• 2,157

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

### 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,233

### 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 (...
• 2,707
Accepted

### Is there a linear programming method that is polynomial in the number of variables, constraints and bitlength of numbers?

Interior-point methods such as Khachiyan’s and Karmarkar’s are, indeed, polynomial in the size of the input, i.e., in the number of variables, constraints, and the bitlength of the coeficients. This ...
• 1,341

### Can remainder mod 2 be efficiently computed from addition and equality?

I really like this question! Here's a sketchy argument for a negative answer (as expected) which I think works but may need some details filled in: Suppose our putative polytime parity-checking ...
• 2,818
1 vote
Accepted

### MSOL for a vertex-cover enlargement problem

You can use CMSOL which allows cardinality predicates. See 5.2.6 in this report. This is authored by Courcelle himself. You can refer the original paper by Courcelle too, but it is a bit more terse. ...
• 387
1 vote

### Linear Time properties classification

As Wikipedia says, not every property is a safety property or a liveness property (consider "a occurs exactly once") The parenthetical gives an example of a property that is not a safety ...
• 162k
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 ...
• 162k
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 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,169
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 = ...
• 162k

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