Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
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, ...
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 ...
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$-...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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?
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 ...
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 ...
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, ...
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 ...
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.
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 ...
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

1
2 3 4 5
11