Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
1 vote
2 answers
24 views

Why is order/choice an issue for a logic for PTIME

As I'm reading on the question of a logic for PTIME and in particular about CPT and its variants, whilst things make sense and I follow along, I came to realise that I don't fundamentally understand ...
Matei Chesa's user avatar
-3 votes
0 answers
56 views

Is there a generalized SAT problem for many-valued logics?

Is there a generalized SAT problem for many-valued logics? related: "Is there a generalized SAT problem for higher-order logics?"
Geremia's user avatar
  • 105
0 votes
1 answer
91 views

Is there a generalized SAT problem for higher-order logics?

The SAT problem is based upon Boolean expressions, but is there a generalized SAT problem based upon higher order logics?
Geremia's user avatar
  • 105
8 votes
1 answer
335 views

In logic programming, what would a language with second-order model theory gain?

HiLog is described as a logic programming language with higher-order syntax, but first-order model theory. For example, it allows you to define a map over lists: ...
MWB's user avatar
  • 259
1 vote
0 answers
64 views

Why is the model-checking problem for MSO $\textsf{PSPACE}$-complete?

I am currently reading "Parameterized Complexity Theory" by J. Flum and M. Grohe. In Chapter 10.3 they state in the first paragraph: Let us remind the reader that the model-checking problem ...
user11718766's user avatar
7 votes
0 answers
94 views

Original formulation of Spira's Lemma

I'm currently reading the book "Proof Complexity" by Jan Krajíček (2019), where Spira's Lemma is mentioned: Let $T$ be a finite $k$-ary tree and $|T| > 1$. Then there is a node $a \in T$ ...
user11718766's user avatar
0 votes
0 answers
94 views

On the polynomial-size Frege proof of the propositional pigeonhole principle

I'm reading a lecture note on the proof of PHP, which mentioned that a "basic fact" $$ \left(\sum\limits_{i=1}^{s-1} A_i\ge a\right) \land A_s \to \sum\limits_{i=1}^s A_i\ge a $$ is ...
Soha's user avatar
  • 187
1 vote
1 answer
321 views

Sparsification and critical clauses in SAT

I have been studying the Exponential-Time Hypothesis, ETH, from this paper, there defined $s_k = \inf\{\delta \geq 0 | k\text{-}SAT \in RTIME[2^{\delta n}]\}$. But in that paper's page number 10, I ...
S. M.'s user avatar
  • 109
0 votes
0 answers
47 views

Is hypergraph reachability definable in MSO?

Let $(A,E)$ be a directed 2-uniform hypergraph and $E$ the corresponding binary relation such that $(X,Y) \in E$ iff there is a hyperedge from $X$ to $Y$. We say that there is a path from $X_1$ to $...
user7680141's user avatar
2 votes
1 answer
163 views

Power of existential types

It is well known that simply typed lambda calculus becomes much more expressive if you allow universal types, as in Girards system F. Thus, for example, you can encode the booleans as forall a. a ->...
manu fava's user avatar
  • 123
10 votes
1 answer
886 views

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

Reading Barendregt's chapter “Lambda Calculi with Types” in the Handbook of Logic in Computer Science (vol. 2: Computational Structures) (Abramsky, Gabbay & Maibaum eds., 1992) I learned (op. cit. ...
Gro-Tsen's user avatar
  • 841
3 votes
0 answers
152 views

Is it possible to recover the set of derivation trees of a fact from its semiring provenance in Datalog?

Background: In the context of Datalog, Green et. al (2007) introduce the notion of the Datalog provenance semiring, a generalization of why-provenance as well as bag and probabilistic database ...
Justin Lubin's user avatar
4 votes
1 answer
178 views

Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

What is the precise connection between: strong normalization of the simply typed $\lambda$-calculus, and cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent ...
Gro-Tsen's user avatar
  • 841
2 votes
0 answers
87 views

Variable opening in locally-nameless representation

Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
phdstudent's user avatar
10 votes
0 answers
274 views

Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?

I am lost in a maze of twisty little type theories, all different. There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the ...
Gro-Tsen's user avatar
  • 841
2 votes
0 answers
153 views

Deciding Satisfiability of a "Universal" Second-Order Logic Formula

Consider the following decision problem: Input: a second-order logic formula $\psi$ of the form $\forall X_1 . \ldots . \forall X_n . \phi$ where $X_1, \ldots, X_n$ are a second-order variables and $\...
David Carral's user avatar
1 vote
0 answers
62 views

Primitive recursion relative to a logical system

In various places I have read that the normally considered non-primitive recursive Ackermann function is primitive recursive in higher-order logic. It's claimed to be due to "Reynolds, 1985",...
Ilk's user avatar
  • 920
0 votes
0 answers
47 views

Using Simplex for Difference Logic

I'm interested in what happens when using the Simplex algorithm on Difference logic, inspired by problem 5.4 in Kroening and Strichman's Decision Procedures. Clearly, in this case, all constraints of ...
Jova's user avatar
  • 161
1 vote
2 answers
122 views

Do realizable systems always have some non-well-founded sets?

Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following: LEM is not realized (e.g. this MSE answer) The traditional ...
Corbin's user avatar
  • 271
2 votes
1 answer
100 views

Are MSO formulae on graphs expressible with bounded quantifier alternation?

Is there some $k$ such that, given any formula $\varphi$ in the monadic second order theory of graphs (this question applies for either MSO with sets of vertices and edges or just MSO with sets of ...
TomKern's user avatar
  • 429
4 votes
2 answers
255 views

Are MSO formulae expressible as existential SO formulae over arbitrary structures?

Given an MSO formulae φ, which may contain arbitrary quantifier alternation, is there always an ESO formula ψ, such that φ and ψ have the same (finite) models? (This statement holds when the models we ...
Florian Zuleger's user avatar
0 votes
1 answer
102 views

Probabilistic Logic Programming vs Stochastic Logic Programming

I'm reading the paper DeepStochLog: Neural Stochastic Logic Programming. The authors differentiate between Probabilistic Logic Programming (PLP) and Stochastic Logic Programming (SLP), but I can't ...
Pav's user avatar
  • 3
1 vote
0 answers
43 views

What are the applications of Belief Revision?

In my Computer Science graduation, I came across this concept of Belief Revision, which focus on knowledge representation and the possible operations that can be done with the facts that a "...
Jonas's user avatar
  • 111
1 vote
0 answers
62 views

Automatizability of Extended Resolution

According to Krajícek, Jan and Pavel Pudlák. “Some Consequences of Cryptographical Conjectures for S12 and EF.” Inf. Comput. 140 (1998): 82-94., the extended Frege proof system is not automatizable ...
Soha's user avatar
  • 187
14 votes
4 answers
2k views

Where is the model theory in programming language theory?

I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
Siddharth's user avatar
  • 823
1 vote
1 answer
163 views

Which are the rules for minimal logic in both sequent calculus and natural deduction styles?

Are there any references I could use which explictly contain the rules for minimal logic, both as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!) To give ...
paulotorrens's user avatar
5 votes
1 answer
116 views

Logical Equivalents of Finite State Transducers

There's a notion of "regular" function on words in automata theory that corresponds nicely to functions in WS1S/Büchi Arithmetic/the logic of words with a prefix and equal-length relation. ...
TomKern's user avatar
  • 429
3 votes
0 answers
75 views

What's the difference between "modular" and "compositional"?

When talking about reducing complexity in a software system, we often talk about making it "modular" by breaking it up into multiple modules that are all linked together to form the overall ...
Jonathan Schuster's user avatar
1 vote
0 answers
75 views

Do soundness and completeness need to be exact converses of eachother?

This question concerns the derivational soundness and completeness of the first-order proof system LK (without equality) as presented in Logical Foundations of Proof Complexity by Cook and Nguyen. In ...
Johnny's user avatar
  • 201
1 vote
1 answer
78 views

Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?

The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained I've ...
Johnny's user avatar
  • 201
1 vote
1 answer
92 views

Intuition behind UTT's internal logic

The "internal logic" of type theory UTT is defined in LF as follows: What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
user175254's user avatar
1 vote
1 answer
139 views

Formulation of Tarski-style universes in LF

Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well. I'm looking at this note ...
user175254's user avatar
3 votes
0 answers
45 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: $$ \...
Nicola Gigante's user avatar
13 votes
12 answers
5k views

Theoretical Computer Science vs other Sciences?

So I‘m in my fifth 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, ...
voltas1231's user avatar
1 vote
3 answers
274 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 ...
whoisit's user avatar
  • 125
4 votes
1 answer
206 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$?
fva's user avatar
  • 45
0 votes
1 answer
71 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 ...
fva's user avatar
  • 45
7 votes
1 answer
239 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-...
technosentience's user avatar
6 votes
1 answer
287 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$-...
Reijo Jaakkola's user avatar
0 votes
0 answers
38 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 ...
Nicola Gigante's user avatar
4 votes
0 answers
77 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 ...
veryinteresting's user avatar
5 votes
1 answer
215 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) ...
cody's user avatar
  • 13.9k
3 votes
1 answer
197 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 ...
Ember Edison's user avatar
1 vote
1 answer
175 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 ...
user1868607's user avatar
  • 1,017
1 vote
0 answers
90 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 ...
sbarra's user avatar
  • 11
2 votes
0 answers
117 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 ...
Noel Arteche's user avatar
1 vote
0 answers
155 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 ...
jpt4's user avatar
  • 81
6 votes
0 answers
101 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 $\...
Nicola Gigante's user avatar
4 votes
0 answers
84 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)...
embie27's user avatar
  • 41
3 votes
1 answer
171 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 ...
Noel Arteche's user avatar

1
2 3 4 5
11