Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
2 votes
0 answers
93 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
142 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
  • 619
2 votes
0 answers
42 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
208 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
  • 619
0 votes
0 answers
114 views

Counterexample in Sistla and Clarke's paper

I'm reading Sistla and Clarke's paper "The Complexity of Propositional Linear Temporal Logics". In section 4 they start with the following set up: Let $S=(s, \xi), T=(t, \pi)$ be structures ...
user1868607's user avatar
2 votes
0 answers
149 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
56 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
  • 900
0 votes
0 answers
46 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
96 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
95 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
  • 279
4 votes
2 answers
248 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
86 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
40 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
57 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
  • 177
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
  • 803
1 vote
1 answer
148 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
111 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
  • 279
3 votes
0 answers
66 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
73 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
75 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
82 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
116 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
42 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
11 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
257 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
191 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
5 votes
0 answers
150 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 ...
user1868607's user avatar
0 votes
1 answer
67 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
6 votes
1 answer
207 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
286 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
37 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
75 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
210 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.7k
3 votes
1 answer
185 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
170 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 vote
0 answers
81 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
106 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
149 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
94 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
82 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
151 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
0 votes
1 answer
59 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 ...
Ioachim Drugus's user avatar
9 votes
0 answers
407 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 ...
Emre Yolcu's user avatar
6 votes
0 answers
230 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: \{...
Steven Schaefer's user avatar
1 vote
1 answer
208 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 ...
Ene's user avatar
  • 11
8 votes
3 answers
741 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 ...
paulotorrens's user avatar
9 votes
1 answer
150 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 ...
Reijo Jaakkola's user avatar
2 votes
0 answers
101 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 ...
ShyPerson's user avatar
  • 424
0 votes
1 answer
86 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 ...
Ajax's user avatar
  • 109
1 vote
0 answers
105 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 ...
Joshua Crotts's user avatar

1
2 3 4 5
11