Skip to main content
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
  • 162k
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
  • 162k
8 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,707
6 votes
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, ...
confusedcius's user avatar
6 votes

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 ...
orlp's user avatar
  • 13.6k
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
  • 13.6k
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.9k
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.9k
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.9k
3 votes
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 ...
DCTLib's user avatar
  • 2,797
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.9k
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
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
  • 301
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

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 ...
NinjaDarth's user avatar
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,157
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
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
  • 162k
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,233
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,707
2 votes
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 ...
Emil Jeřábek's user avatar
2 votes

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 ...
Noah Schweber's user avatar
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. ...
Sriram's user avatar
  • 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 ...
D.W.'s user avatar
  • 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 ...
D.W.'s user avatar
  • 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.
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,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 = ...
D.W.'s user avatar
  • 162k

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