Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.

Sign up to join this community

Anybody can ask a question

Anybody can answer

The best answers are voted up and rise to the top

Explore our Questions

Ask Question

more tags

Active Hot Week Month

15

votes

2

answers

662

views

Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

reference-request lo.logic coq proof-assistants

modified Mar 13 at 13:49 Hermann Gruber 4,369

2

votes

1

answer

56

views

FO(TC) lower bounding games?

cc.complexity-theory lo.logic finite-model-theory

answered Mar 5 at 15:10 Will Asness 41

15

votes

3

answers

1k

views

Checking formulas with two quantifiers ($\forall \exists$) - 2QBF

ds.algorithms lo.logic sat boolean-functions

modified Jan 1 at 18:42 Pushpa 209

9

votes

1

answer

158

views

What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

cc.complexity-theory lo.logic sat boolean-functions

answered Dec 13 '19 at 16:06 Emil Jeřábek 11.4k

9

votes

1

answer

385

views

Measurable language which is not $\omega$-regular

lo.logic fl.formal-languages automata-theory omega-language

modified Dec 12 '19 at 22:34 Hermann Gruber 4,369

2

votes

0

answers

181

views

How do computers check if two functions are the same?

lo.logic functional-programming proof-assistants

asked Nov 11 '19 at 13:18 Student 129

11

votes

0

answers

307

views

Is unary $\Pi_2$-SUBSETSUM coNP-complete?

cc.complexity-theory np-hardness complexity-classes lo.logic

modified Oct 31 '19 at 13:14 Alexey Milovanov 1,509

17

votes

2

answers

1k

views

Smallest possible universal combinator

lo.logic computability lambda-calculus universal-computation combinatory-logic

modified Oct 20 '19 at 23:24 user76284 378

0

votes

0

answers

98

views

Fagin's Theorem implications

lo.logic np

asked Oct 13 '19 at 13:49 gifa 21

1

vote

0

answers

79

views

Cover set of Boolean formulas with conjunctions

lo.logic boolean-functions boolean-formulas covering-problems

asked Oct 10 '19 at 1:11 madbeebop 19

10

votes

0

answers

187

views

On Courcelle's question about Monadic second-order logic with cardinality predicates

cc.complexity-theory complexity-classes lo.logic polynomial-time

asked Oct 9 '19 at 9:38 Alexey Milovanov 1,509

5

votes

0

answers

78

views

Are there languages require many variables to achieve $\Sigma_n^0$ completeness?

lo.logic computability

modified Sep 17 '19 at 18:35 Stella Biderman 996

18

votes

1

answer

3k

views

Prove proof irrelevance in Coq?

lo.logic type-theory proof-assistants coq

modified Aug 26 '19 at 15:40 arvidj 103

5

votes

2

answers

465

views

Good description of Calculus of Inductive Construction

lo.logic dependent-type

modified Aug 26 '19 at 8:40 Steven Shaw 474

Browse more Questions

Theoretical Computer Science Stack Exchange works best with JavaScript enabled