Questions tagged [lo.logic]
Computational and mathematical logic.
518
questions
3
votes
0
answers
35
views
Can you compute Shannon expansion of a Boolean formula more efficiently by using a QBF solver?
Maybe this is not enough research level, but I've been scratching my head on it for a while...
I'm interested in the Shannon expansion of an existentially quantified Boolean formula of the form:
$$ \...
- 1,406
10
votes
12
answers
4k
views
Theoretical Computer Science vs other Sciences?
So I‘m in my third semester studying Computer Science at a German university, so I‘ve only scratched the surface of Theoretical Computer Science, namely Logic, Formal Languages, Automata Theory, ...
- 117
1
vote
3
answers
211
views
Turing Machines and Logic
It is well known that Monadic Second Order Logic (over words) and finite automata can express the same set of languages.
Is there a logic over words (perhaps a nth order logic) such that it and turing ...
- 123
4
votes
1
answer
147
views
Shortest path property and monadic second order logic
I know that induced paths and Hamiltonian cycles can be expressed with monadic second-order logic ($MS_2$).
Is it possible to express the shortest path in $MS_2$?
- 45
5
votes
0
answers
123
views
Arithmetization of finite automata
Is there any standard way to encode the language accepted by a finite automaton by an arithmetic formula?
A particular way of doing this would be to extend the language of existential integer linear ...
- 889
0
votes
1
answer
49
views
Resources for first-order and second-order monadic logics with a model-checking objective
What are some good books and surveys for learning about first-order logic and monadic second-order logic?
I'm a graduate student in computer science with a focus on algorithms. For model-checking on ...
- 45
5
votes
1
answer
157
views
Stronger "induction" principles than induction-recursion
Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-...
6
votes
1
answer
285
views
Concrete family of propositional formulas
Let $k,n \in \mathbb{N}$, where $k$ can be thought of as being fixed constant. For each $1 \leq \ell \leq k$ and $1 \leq i \leq n$ we have a proposition symbol $p_{(\ell,i)}$ (so in total we have $nk$-...
- 869
0
votes
0
answers
34
views
Making primary keys explicit in a Boolean relation
Suppose we have a Boolean formula $\phi(X,Y)$ over the sets of Boolean variables $X$ and $Y$, representing a binary relation. There are in general many tuples in this relation.
Is there a way to ...
- 1,406
4
votes
0
answers
73
views
Lower bound on the size of Skolem functions
Consider a quantified Boolean formula $f$. We can convert it into Skolem Normal Form formula $f^*$ such that $f$ is satisfiable iff $f^*$ is satisfiable, by replacing variables that are existentially ...
5
votes
1
answer
203
views
Can you define recursive predicates in 2nd order intuitionistic logic?
This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here.
Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) ...
- 13.4k
3
votes
1
answer
149
views
How far is the distance between Mahlo Universe and Mahlo Cardinal?
There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.
More explicitly, I would ...
- 51
1
vote
1
answer
167
views
Complexity of "discrete-time" SAT
I'm interested in the complexity of deciding satisfiability of the following family of formulae:
$\exists j. I[j(0)] \land \forall t. S[j(t),j(t+1)]$
where:
$j:\mathbb{N} \to \{0,1\}^n$ has finite ...
- 889
1
vote
0
answers
70
views
On completeness of LTL
I am reading the seminal paper "On the temporal analysis of fairness" by Gabbay, Pnueli, Shelah, Stavi, available at
shelah.logic.at/papers/134/
In Section 3, completeness of a set of axioms ...
- 11
1
vote
0
answers
84
views
Gurevich's theorem on primitive recursive functions being logspace-computable
I recently came across the following result attributed to Gurevich, according to which I understood that the class of problems solvable by primitive recursive functions is precisely the class L of ...
- 557
1
vote
0
answers
133
views
What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?
The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
- 81
6
votes
0
answers
81
views
Relationship between natural deduction refutation and tableaux for propositional logic
Which kind of relationship is there between natural deduction refutations of a set f propositional logic assumptions, and the corresponding tableaux?
For example, consider the unsatisfiable set $\...
- 1,406
4
votes
0
answers
76
views
Are there classes for that FO-model checking is FPT on hypergraphs?
For graphs, there are many classes that admit FPT-algorithms for model checking of first order logic, e.g. the class of nowhere dense graphs by Grohe et. al.
Are there similar results for ($k$-uniform)...
- 41
3
votes
1
answer
120
views
Efficient transformation into CNF preserving entailment
Suppose you have two propositional formulas $\varphi$ and $\psi$, not necessarily in CNF. I want to convert them to 3CNF efficiently (hence introducing auxiliary variables) in such a way that $\varphi ...
- 557
0
votes
1
answer
58
views
Are there logical devices similar to "existential variables" or "blank nodes" of Semantic Web?
In Semantic Web, alongside permanent names of things also "temporary names" named "existential variables" or "blank nodes" denoted as "_:label" are used. All ...
- 101
9
votes
0
answers
387
views
Examples of simulations in proof complexity that are not p-simulations
I am writing a paper on the complexity of some unorthodox proof systems, where I have two systems $P$ and $Q$ such that $P$ simulates $Q$ in the sense of it being possible to translate a $Q$-proof ...
- 191
5
votes
0
answers
212
views
Satisfiability and a Galois Theory Analog
Let $v(a, b)$ be a binary predicate, and define $\phi$ as follows:
$$\phi: v(a_1, b_1) \land v(a_1, b_2) \land (a_1, b_3)$$
where our universe consists of two sorts $A: \{a_1, a_2, a_3\}$ and $B: \{...
1
vote
1
answer
143
views
Defining functions on non-inductive types using LEM in Coq
I'm trying to prove statements about homomorphisms in Coq. Specifically, about in which cases the existence of some set of homomorphisms implies the existence of a specific other homomorphism. I'm ...
- 11
8
votes
3
answers
686
views
What's the logical counterpart to jumps with arguments on CPS terms?
It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
- 293
9
votes
1
answer
141
views
Validity problem of intuitionistic two-variable logic
The two-variable fragment $\mathrm{FO}^2$ consist of those sentences of first-order logic $\mathrm{FO}$ in which precisely two variables occur (e.g. $\exists x \exists y \exists z R(x,y,z)$ is not a ...
- 869
2
votes
0
answers
94
views
Recovering the inputs to Boolean circuits after partial evaluation
This question discusses Boolean Circuits and Boolean functions from $n>1$ inputs to one Boolean output. Notation: $\textit{arity}(\mathcal{C})=n$ if $\mathcal{C}$ takes $n$ inputs, similarly for ...
- 414
0
votes
1
answer
79
views
Is there a fundamental link between Nash's equilibrium and Turing's halting problem?
Since Nash equilibrium exists, is there a computational analogue of this equilibrium point? I am trying to approach Nash equilibrium from computational point of view to see if the equilibrium point ...
- 109
1
vote
0
answers
99
views
Where does "Quine's Method" in propositional logic originate?
Hein (407-408) states that Quine's method "...uses these (14) properties together with basic equivalences to determine whether a wff is a tautology, a contradiction, or a contingency." The ...
3
votes
0
answers
59
views
Is relativization statement-dependent or proof-dependent?
I'm relearning some computability theory, and have encountered the idea of relativization of results to arbitrary subsets of $\omega$ and the subtlety of figuring out what the correct relativized ...
- 139
9
votes
0
answers
192
views
Constructive Strong Normalization of the Extended Calculus of Constructions
The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
- 375
2
votes
1
answer
219
views
Alternatives to Normalization by Evaluation
Reading about lambda calculus I got the impression that normalization is evaluation.
So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel).
...
- 29
-2
votes
1
answer
66
views
Linear Integer Arithmetic Satisfiability with Three Literals [closed]
I'm stuck on trying to find an unsatisfiable conjunction of the form $a \wedge b \wedge c$ where:
$a \wedge b$ is satisfiable
$a \wedge c$ is satisfiable
$b \wedge c$ is satisfiable
$a, b, c$ are ...
- 99
3
votes
0
answers
92
views
Boltzmann sampling for containers/dependent polynomials?
I’d like to randomly sample from dependently-typed data structures.
Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
- 32.1k
3
votes
1
answer
284
views
Proof and computational complexity
I couldn't find documents elaborating on this: if the Curry Howard correspondence is to be interpreted as establishing a strong relation between proofs and programs, should there not be a strong ...
- 889
2
votes
1
answer
110
views
How long does it take at most for $k$ boolean variables to map back to themselves with a positive disjunctive update rule?
I have a vector of boolean variables $v=(x_1,\dots,x_k)$. In each step each variable is updated according to a positive disjunction like so:
$x_1 \leftarrow x_i \vee \dots \vee x_j$
$\dots$
$x_k \...
- 123
3
votes
2
answers
147
views
Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals [closed]
Looking for some lecture videos (introductory level) on logic, models of computation as well as computational complexity/ other theoretical computer science fundamentals
- 227
1
vote
1
answer
86
views
Variable wire weights in DLOGTIME-uniform circuits
The definition of a $DLOGTIME$-uniform circuit family is based on a Turing machine that accepts the language $\langle t, a, b \rangle$, where gate $a$ is of type $t$ and has gate $b$ as a child, ...
- 1,015
1
vote
0
answers
79
views
Complexity class name for the class of languages that are $\Sigma^1_1$-definable over finite domains
Let ${\cal L}=\{Y_1,..., Y_k, X\}$ be a finite relational language such that $X$ is a unary relation name. Let $\phi(X,\bar{Y})\in{\cal L}$ be a first-order formula (the formula can have the equality ...
- 322
21
votes
2
answers
1k
views
Decidability of diophantine equations over {=, +, gcd}
It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $\{=, +, \cdot, 1\}$ (of equality, addition, ...
- 852
9
votes
1
answer
131
views
Proof of $DLOGTIME-CC^0 = MOD[<,bit]$
Let $CC^0[m]$ be the class of constant-depth, polynomial-sized circuits consisting entirely of $MOD_m$ gates, which put out $1$ iff the sum of their inputs $\equiv 0~(\textrm{mod}~m)$. In the same way ...
- 1,015
1
vote
0
answers
120
views
$\mathit{FO}[+,\times]$ seems more powerful than $\mathit{DLOGTIME}$-uniform $\mathit{AC}^0$?
I’ve been reading up on the connection between first order logic and small circuit complexity classes, and specifically Barrington, Immerman, and Straubing’s paper “On Uniformity Within $\mathit{NC}^1$...
- 1,015
1
vote
1
answer
84
views
Is every countable, finite-branching LTS bisimilar to a tree?
Let $L$ be a finite set of labels, and let $\mathcal{C}$ be the set of finitely-branching transition systems labeled by $L$ and with a countable set of states. Let $\sim$ denote the bisimulation ...
2
votes
1
answer
217
views
Is modal $\mu$-calculus "equivalent" to bisimulation?
I know that propositional modal $\mu$-calculus $L\mu$ is bisimulation-invariant. However, I'm curious to what degree it captures bisimulation.
Q1: Given two labeled transition systems $T_1$, $T_2$ ...
4
votes
0
answers
170
views
Alternative exponential definition of Kolmogorov complexity
In Kikuchi's paper Kolmogorov complexity and the second incompleteness theorem the Kolmogorov Complexity (KC) of $x$ is defined as
$$ K(x) = \mu e (\varphi_e(0) \simeq x) \, , $$
the smallest $e$ such ...
- 41
1
vote
0
answers
111
views
λProlog vs HiLog
λProlog is a well-known higher-order logic programming language.
On the other hand, HiLog is described as a logic programming language with higher-order syntax, but first-order model theory.
Do I ...
- 231
2
votes
2
answers
310
views
Uncountability in intuitionistic logic
I've read snippets here and there that inside intuitionistic logic, uncountable can be a subset of the naturals ?
What is the correct intuition to think about this? Andrej Bauer replied above, saying ...
- 585
2
votes
0
answers
167
views
Order-invariant conjunctive queries are FO-definable without the order
I'm looking for a reference for Exercise 6.11 from Libkin's FMT book:
Prove that an order-invariant conjunctive query is FO-definable without the order relation.
All help is appreciated.
- 1,165
2
votes
1
answer
176
views
Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?
As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $\mathrm{FO^2}$, In order to do this they use Scott's reduction. Which is the ...
- 706
5
votes
1
answer
141
views
Does focused proof search ever have to backtrack across the choice of focus formula?
There are a lot of different "focused" sequent calculi for lots of different logics, but my understanding is that many or most of them have the following flavor. First one divides the ...
- 667
3
votes
1
answer
170
views
Normal forms for counting quantifiers?
In the paper by [Erich Grädel and Martin Otto], the authors state that any formula in First Order Logic with two variables with counting quantifiers can be reduced to a formula of the form
$$ \forall ...
- 706