# Questions tagged [lo.logic]

Computational and mathematical logic.

457 questions
Filter by
Sorted by
Tagged with
7answers
7k views

### Solid applications of category theory in TCS?

I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all ...
5answers
3k views

3answers
836 views

### What algorithms are known for computing Craig interpolants?

Is there any survey of algorithms for computing interpolants? What about papers on only one algorithm? The case I'm most interested in is $A=\lnot p\land q$ and $C=q$, plus the constraint that the ...
1answer
552 views

### Combinators for the Primitive Recursive Functions

It is well-known that the S and K combinators are Turing Complete. Are there combinators that suffice to yield (only) the primitive recursive functions?
1answer
771 views

### Scott's stochastic lambda calculi

Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
1answer
322 views

### Minor closed properties that are explicitly MSO expressible

Below, MSO denotes the monadic second order logic of graphs with vertex-set and edge-set quantifications. Let $\mathcal{F}$ be a minor closed family of graphs. It follows from Robertson and Seymour'...
3answers
2k views

### Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
4answers
721 views

### Automated theorem proving in linear logic

Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction? Where can I read more about automatic theorem proving in these ...
4answers
3k views

### What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...