Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
11
votes
2answers
432 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 ...
38
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
914 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
386 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
843 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 ...
18
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
272 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 ...
27
votes
6answers
949 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
541 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
494 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 ...
18
votes
0answers
465 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 ...
33
votes
4answers
860 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, ...