Questions tagged [lo.logic]
Computational and mathematical logic.
518
questions
1
vote
0
answers
67
views
To what extent supervised learning ERM learn first-order knowledge
Suppose I have a collection of (hidden) first-order rules:
$$
\mathcal{R}: \{ Q_i(x) => P_i(x) \}_{i=1}^{k}
$$
all defined over $x \in \mathcal{X}$.
I can use these rules and (automatically) ...
- 749
3
votes
0
answers
117
views
Decomposition of rectangular relations
Let $\alpha$ be a binary relation from $\gamma$ to $\chi$ and $\beta$ a binary relation from $\chi$ to $\rho$. If both $\alpha$ and $\beta$ are rectangular, i.e., they satisfy $\alpha \alpha^{-1} \...
- 748
4
votes
0
answers
146
views
Formalization of proofs and CC paradox? - Part II
This was the second part of my previous question. It is very similar, and probably it has a similar answer (as Emil said in a comment), but I thought it was worth to separate it and ask it as a new ...
- 22.4k
7
votes
1
answer
426
views
Formalization of proofs and computational complexity paradox?
While reading some articles on formal proofs (see also my previous question on cstheory about the length of ZFC proofs versus human written proofs), I came up with this apparent paradox.
Let $M_{...
- 22.4k
5
votes
0
answers
264
views
Is Agda sound as a proof system? [closed]
I've asked the same question on CSSE but with no luck (https://cs.stackexchange.com/questions/89611/is-agda-sound-as-a-proof-system). Therefore I ask it again here in cstheory and hope that more ...
- 251
9
votes
1
answer
1k
views
Sparsification Lemma for k-SAT and Exponential Time Hypothesis
According to R. Impagliazzo, R. Paturi and F. Zane, 2001 an instance of $k$-SAT is called sparse if $m = O(n)$ where $m$ denotes the number of clauses and $n$ the number of variables. The ...
- 1,977
2
votes
1
answer
154
views
Is Eulerian Path (or Eulerian Cycle) definable in Monadic Second Order Logic?
Does there exist a monadic second order logic formula which is satisfied by a graph if and only if it has an Eulerian path (or Eulerian cycle).
I am looking for properties of graphs which are ...
6
votes
0
answers
279
views
Fischer and Rabin's theorem (1974) for theories of "additive" structures
Fischer and Rabin's Super-Exponential Complexity of Presburger Arithmetic (1974) has the following theorem.
(Theorem 12) Let $U$ be any class of additive structures, so if $A = (A, +) \in U$,
...
- 885
2
votes
0
answers
56
views
Is there a complete and finite axiom scheme for conditional independence? (Graphoids)
Note: This is a better-written version of an unanswered question asked before on MathOverflow.
Question: Is there a complete and finite axiom scheme for conditional probability?
If so, is there a ...
- 503
3
votes
1
answer
159
views
Connection between algebraic logic and computational complexity of logics?
I'm learning a bit about algebraic logic and I was wondering how knowing the algebraic semantics of a given logic might help the study of the logic itself from a computational point of view.
In ...
- 1,406
8
votes
1
answer
484
views
Complexity of modal logic IK5
What is the complexity of local satisfiability problem for modal logic $\mathit{IK5}$? Herein we denote by $IK5$ the modal logic over euclidean frames extended with inverse modality. Could you provide ...
- 1,165
3
votes
4
answers
367
views
Philosophy behind monotonicity requirement for inductive types
Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions? According to my understanding of the Bishop/...
- 247
0
votes
1
answer
53
views
Head variables of terms after application
We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\...
- 259
6
votes
2
answers
950
views
Efficiently modeling Turing machines in Peano Arithmetic
The (undecidable) Peano Arithmetic (PA) is powerful enough to model Turing machines.
Consider a standard first order axiomatization of Peano Arithmetic and a standard Hilbert-style proof system $\...
- 22.4k
3
votes
0
answers
129
views
Family of formulas for which Gabbay's separation algorithm explodes nonelementarily
It is repeated throughout the literature that Gabbay's algorithm for
separation of LTL with Since and Until can produce nonelementary blow-up
of the size of the formula, but I have never seen a proof ...
6
votes
1
answer
284
views
Normal forms for intuitionistic formulas?
It is well-known that DNFs/CNFs and prenex normal forms generally do not exist for intuitionistic logic.
Are there any nice results about formula normalization for IL? I've tried googling this but ...
- 247
1
vote
0
answers
86
views
On collapsing the Exponential time hierarchy
Define $\Sigma^E_0 = \Pi^E_0=E$,
for every $n>0$, define $\Sigma^E_n=NE^{\Sigma^p_{n-1}}$,
for every $n>0$, define $\Pi^E_n=CoNE^{\Sigma^p_{n-1}}$.
Define the Exponential time hierarchy by $EH=\...
- 322
11
votes
2
answers
449
views
State of the Art for the Monadic Class?
Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete.
...
- 2,764
6
votes
1
answer
262
views
Algebraic account of Gaussian elimination?
For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting
question about the interpretation of double-negation-...
- 32.1k
13
votes
1
answer
235
views
Conclusions from reverse mathematical strength of graph minor theorem
Say we have a graph property which can be checked in nondeterministic polynomial time, and a proof in a weak formal system (say RCA0) that the property is minor closed. Can we say anything about the ...
- 3,013
1
vote
0
answers
83
views
What logic(s) exist for attributing belief?
I'm looking for an appropriate formalism to represent "traceability" in claims, especially connecting conclusions to source materials in a rigorous way. For example, I'd like to be able to represent ...
- 111
2
votes
2
answers
405
views
Automated proving that a program doesn't halt
If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)...
- 145
10
votes
1
answer
261
views
Equilibrium in a Halting Game
Consider the following 2-player game:
Nature randomly picks a program
Each player plays a number in [0, infinity] inclusive in response to nature's move
Take the minimum of the players’ numbers, and ...
- 103
1
vote
2
answers
120
views
Determine if a structure is a model of an inductively defined predicate
My setting is first-order logic. As an example, consider an inductive definition of a linked list:
$List(l)$ = $Null(l)$ $\vee~(Node(l) \wedge \exists sublist. List(sublist) \wedge next(l,...
- 712
1
vote
0
answers
180
views
Definitions of strongest postconditions [closed]
The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer
$X ~\mapsto \neg G \wedge ...
- 81
11
votes
2
answers
200
views
Does the first order theory of a finite structure have bounded quantifier rank?
Let $\mathfrak{A} $ be any finite structure.
Does its first order theory $ \mathfrak{T} := \mathfrak{TH}(\mathfrak{A}) $ have bounded quantifier rank, in the sense that there is a $ q\in\mathbb{N} $ ...
- 207
5
votes
1
answer
163
views
Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups
This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that ...
- 889
3
votes
2
answers
276
views
Languages that lack contraction, weakening or exchange
When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange?
...
- 2,511
1
vote
0
answers
86
views
Question on Turings Dissertation *Systems of Logic based on Ordinals*, Axiomatic Properties [closed]
I have a question on Alan Turing's Dissertation Systems of Logic Based on Ordinals, a scanned copy you can find here, or rewritten in LaTeX here, and also a copy of the published version here (but in ...
- 1,977
11
votes
1
answer
630
views
What is the intuition behind linear logic?
I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means $A$ is ...
- 221
4
votes
0
answers
65
views
Finite intersection property of polymorphic type families
Let $\Phi$ be a type functor definable in polymorphic lambda calculus:
$$ \alpha : * \vdash \Phi(\alpha) : * $$
$$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$
Suppose further ...
- 601
3
votes
0
answers
152
views
Efficiently computing the union of all minimal unsatisfiable constraint sets in a first-order unification problem
Suppose we are given a standard first-order unification problem, represented as a set $D$ of term equality constraints, such that the system $D$ as a whole is unsatisfiable. Consider the minimal ...
- 236
6
votes
0
answers
203
views
Relationship between Pataraia's theorem and inductive-recursive definitions?
Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
- 32.1k
3
votes
1
answer
443
views
How to generate Skolem function in practice
Context: Skolemization is the process of removing the existential quantifiers in a first-order formula. The existential bounded variables are replaced with existential quantified function.
Questions: ...
- 133
4
votes
0
answers
96
views
Coherence spaces and full completeness for the implicative fragment of linear logic
Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$.
I ...
- 433
1
vote
2
answers
73
views
Algorithms to synthesize optimal plans satisfying temporal logic constraints
I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online.
I am ...
- 111
3
votes
2
answers
138
views
Construct proof systems for common algorithmic task, like equivalence of regular expressions
A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto.
For $y \in L$ ...
- 1,977
5
votes
0
answers
141
views
Salomaa's axiomatisation of regular languages and the use of regular expression in it
I am reading the classical article of A. Salomaa where he gives two axiom systems for regular sets and proofs consistency and completeness.
As I have understood it, an axiomatic system in some logic (...
- 1,977
6
votes
1
answer
159
views
How to mechanically derive the recursor of a type from its constructors?
In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the ...
- 777
18
votes
1
answer
933
views
Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?
Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. -...
- 36.3k
11
votes
1
answer
875
views
Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?
So I've been wondering if the Law of Excluded Middle (LEM) implies the so-called Axiom K in Martin-Löf's Intensional Type Theory. The Axiom K states that
$$\Pi_{A : Type} \Pi_{x : A} \Pi_{p : \text{Id}...
- 777
4
votes
0
answers
114
views
Transferring results on coalgebras in one category to another
Let $F$ and $G$ be endofunctors over categories $C$ and $ D$, respectively. Suppose that there is a forgetful functor $C \to D$ that has a left adjoint. Can we infer properties of $F$-coalgebras ...
- 885
11
votes
1
answer
279
views
Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)
The first term is used by Hilbert in his 1928 work, but in Gödel's later work, the same thing is referred to as Unvollständigkeitssatz ("incompleteness theorem"). For today's German CS researchers, it ...
- 213
6
votes
2
answers
351
views
Is there an algorithm which gets incrementally "smarter" as it runs?
Mind the following program:
n = 0
best = 0
while (true):
if (hash(n) > best):
best = hash(n)
++n
If you leave this program running for 10 years, when ...
- 3,035
12
votes
0
answers
253
views
Categorical semantics for S5 modal logic?
Does anyone know where I can look to find out what the generally categorical semantics of S5 is?
For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving ...
- 32.1k
7
votes
1
answer
170
views
Intuitionistic fragments of classical logic
For what conditions on P and Q, does P ⊢ Q in classical logic imply ...
- 255
8
votes
1
answer
145
views
About the origin of the names "immune" and "simple"
I have been wondering for a while about the origin of the names "immune"
and "simple". I also posed the same question to Andrea Sorbi, who in turn
involved a few more colleagues in the discussion.
...
- 621
2
votes
0
answers
58
views
Decidability of the monadic second-order theory of a class of finite structures
Let $L$ be the set of sentences in some logic. I am interested in cases where $L$ is the set of sentences in monadic second-order logic, or it is its $\Pi^1_1$ fragment. Let $K$ be a class of finite ...
- 885
2
votes
0
answers
121
views
Applications of the monoidal closed structure in LTL?
A simple model of temporal logic is via time-indexed truth
functions. This lets us model the Boolean connectives, as well as the
next-step operator and modal always operator:
$$
\begin{array}{lclll}
...
- 32.1k
10
votes
1
answer
228
views
Typo in the calculus of constructions paper?
In the classic the calculus of constructions paper there is a rule that states
(page 7 of the pdf, page 101 of the original document)
This rule would mean that any context is reducible to a member ...
- 546