Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
26
votes
4answers
2k views

Why do we need formal semantics for predicate logic?

Consider this question solved. I will not pick a best answer as all of them have contributed to my understanding of the topic. Im unsure what benefit we have by formally defining the semantics of ...
15
votes
2answers
477 views

Are there intermediate eta theories for the lambda calculus?

There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory. Do these two theories have an in-between, a kind of intermediate eta ...
49
votes
3answers
4k views

Shallow versus Deep Embeddings

When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written ...
105
votes
7answers
8k 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 ...
11
votes
2answers
466 views

Does the System F with pairs have the strong normalisation and subject reduction properties?

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
39
votes
5answers
1k views

Is there a logic without induction that captures much of P?

The Immerman-Vardi theorem states that PTIME (or P) is precisely the class of languages that can be described by a sentence of First-Order Logic together with a fixed-point operator, over the class of ...
14
votes
1answer
2k views

What are the classic papers from the recursion theoretic area of complexity theory?

Two papers I would include are: D. Kozen, "Indexing of subrecursive classes", STOC, 1978. R. Ladner, "On the Structure of Polynomial Time Reducibility", JACM, 1975.
5
votes
2answers
916 views

Handbook of Logic in Computer Science - is it worth it?

I just found the first volume of Handbook of Logic in Computer Science in a library, but unfortunately I won't be able to use it here. It seems like a great resource, but it's insanely expensive to ...
5
votes
3answers
425 views

Definition for MSO2 for arbitrary structures

I am not able to find a rigorous definition of MSO_2 logic for arbitrary structures (which I can cite). MSO_2 for graphs is often used and defined, i.e. in On the Parameterised Intractability of ...
19
votes
3answers
885 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 ...
19
votes
3answers
2k views

Why can Lambda Calculus not represent some combinators?

This paper suggests that there are combinators (representing symbolic computations) that can not be represented by the Lambda calculus (if I understand things correctly):
14
votes
1answer
294 views

Characterising invisible equivalences by confluent rewrite rules

In response to another question, Extensions of beta theory of lambda calculus, Evgenij offered the answer: beta + the rule {s = t | s and t are closed unsolvable terms} where a term M is solvable if ...
28
votes
6answers
996 views

Well known classes of boolean formulas that require exponentially long resolution proofs

You might often find cutting plane methods, variable propagation, branch and bound, clause learning, intelligent backtracking or even handwoven human heuristics in SAT solvers. Yet for decades the ...
14
votes
3answers
566 views

How hard is it to reduce termination to partial correctness?

If you are familiar with program verification you are likely to prefer reading the Question before the Background. If you are not familiar with program verification then you may still be able to ...
26
votes
3answers
2k views

Translating SAT to HornSAT

Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT seems to imply that it is, but I have not been able to chase down ...
20
votes
3answers
515 views

Are recursive forms of Godel's statement possible?

The self-referentiality of the P/NP problem has sometimes been highlighted as a barrier to its resolution, see, for instance, Scott Aaronson's paper, is P vs. NP formally independent? One of the many ...
19
votes
0answers
472 views

To what extent MSO = WS1S, when adding relations?

[This question has been asked on MathOverflow with no luck a month ago.] Let me first clarify my definitions. For a word $w \in \Sigma^*$, with $\Sigma =\{a_1, \ldots, a_n\}$, I define two ...
34
votes
4answers
911 views

Correspondence between complexity classes and logic

I took a class once on Computability and Logic. The material included a correlation between complexity / computability classes (R, RE, co-RE, P, NP, Logspace, ...) and Logics (Predicate calculus, ...

1
6 7 8 9
10