Questions tagged [lo.logic]
Computational and mathematical logic.
521
questions
8
votes
2
answers
396
views
Game semantics for coinductive predicates
Does anyone know of any work on game semantics for coinductive predicates?
A coinductive predicate is one where the predicate itself is called in the body of the predicate, and we are taking the ...
- 16.6k
28
votes
4
answers
6k
views
Church's Theorem and Gödel's Incompleteness Theorems
I have recently been reading up on some of the ideas and history of the ground-breaking work done by various logicians and mathematicians regarding computability. While the individual concepts are ...
- 857
11
votes
1
answer
631
views
Ehrenfeucht-Fraïssé games (Ajtai-Fagin in fact) for regular languages.
Immerman (Descriptive Complexity, 1999) presents the EF games for existential monadic second order (Ajtai-Fagin games) on page 127. As $\exists$MSO on words is equivalent to regular languages, the ...
- 3,916
28
votes
4
answers
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 ...
- 289
15
votes
2
answers
508
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 ...
- 4,306
52
votes
3
answers
6k
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 ...
- 16.6k
111
votes
7
answers
10k
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 ...
- 26.7k
11
votes
2
answers
489
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 ...
- 701
39
votes
5
answers
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 ...
- 18.8k
14
votes
1
answer
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
2
answers
952
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 ...
- 151
5
votes
3
answers
663
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 ...
- 443
19
votes
3
answers
1k
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 ...
- 4,776
21
votes
3
answers
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):
- 2,541
14
votes
1
answer
313
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 ...
- 4,306
29
votes
6
answers
1k
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
3
answers
604
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 ...
- 4,776
30
votes
3
answers
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 ...
- 1,079
21
votes
3
answers
541
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 ...
- 853
19
votes
0
answers
508
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 ...
- 3,916
35
votes
4
answers
989
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, ...
- 863