Explore our questions

2 votes
0 answers
105 views

Extended Resolution refutation for the clique-coloring formulas

0 votes
0 answers
88 views

On the polynomial-size Frege proof of the propositional pigeonhole principle

1 vote
1 answer
318 views

Sparsification and critical clauses in SAT

0 votes
0 answers
45 views

Is hypergraph reachability definable in MSO?

2 votes
1 answer
136 views

Power of existential types

7 votes
2 answers
466 views

Concatenative binary lambda calculus/combinatory logic

21 votes
3 answers
2k views

Smallest possible universal combinator

10 votes
1 answer
865 views

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

2 votes
0 answers
85 views

Variable opening in locally-nameless representation

3 votes
0 answers
140 views

Is it possible to recover the set of derivation trees of a fact from its semiring provenance in Datalog?

4 votes
1 answer
172 views

Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

10 votes
0 answers
263 views

Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?

2 votes
0 answers
151 views

Deciding Satisfiability of a "Universal" Second-Order Logic Formula

1 vote
0 answers
61 views

Primitive recursion relative to a logical system

Browse more Questions