Computational and mathematical logic.
13
votes
4answers
399 views
When does (or should) Theoretical CS care about intuitionistic proofs?
From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the ...
-4
votes
0answers
45 views
Start using SAT Solvers [migrated]
What i actually want to do is to turn a math problem ,i have to solve,to a Boolean Satisfiability problem and solve it using a SAT Solver.
I wonder if someone knows any manual,guide or anything that ...
-1
votes
1answer
40 views
Constructing automata with the same traces, but where a CTL-formula is not equally satisfied
Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of Principles of Model Checking by Baier and Katoen. You're supposed to prove that there does not ...
-2
votes
0answers
84 views
What is a Closure (hull) operator? [closed]
Simply the question stated.
I'd appreciate examples so i may further understand the its roles and significance.
edited to remove confusion
6
votes
3answers
111 views
Complexity one-alternation SMT
I'm looking for the complexity of satisfiability of a formula $\forall y_1, \dots,y_n, \exists x_1,\dots,x_m, \phi$ or of a formula $ \exists x_1,\dots,x_m \forall y_1, \dots,y_n,\phi$ where $\phi$ is ...
7
votes
1answer
147 views
What is the categorical semantics of subtyping?
Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type ...
1
vote
0answers
86 views
Proofs for Implementation Statements
I've been struggling with understanding of the proofs showing that implementation statements are extensional.
Basically I am referring to material described in Abstraction Classes in Software Design ...
0
votes
0answers
88 views
Proofs for Design Statements
I've been struggling with understanding of the proofs showing that tactical design statements are intensional and local.
Basically I am referring to this material:
Abstraction Classes in Software ...
1
vote
1answer
65 views
Implied Clause and Resolvent
(I posted this question on MathSE first, no answer, that is the reason why I come here.)
Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ ...
16
votes
3answers
356 views
Constructively efficient algorithms without efficient correctness and efficiency proof
I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t.
their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but
no proof using ...
7
votes
1answer
215 views
Proofs in $S_{2}^{1}$
In a talk by Razborov, a curious little statement is posted.
If FACTORING is hard, then Fermat’s little theorem is not provable in $S_{2}^{1}$.
What is $S_{2}^{1}$ and why are current proofs not ...
6
votes
1answer
114 views
Measurable language which is not $\omega$-regular
Let $\Sigma$ be a finite alphabet and let $\Sigma^\omega$ be the set of all infinite words over $\Sigma$. Consider
$$
d(x,y):=2^{-\min(n \in \Bbb N_0:x_n\neq y_n)}
$$
to be the metric on ...
18
votes
2answers
2k views
What is the logarithm or root operation in type-space?
I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types ...
2
votes
1answer
213 views
Most important topics for a short introduction to Prolog
Suppose you were teaching an introductory course on logic as part of a TCS curriculum. Furthermore, suppose that you had one week (= two 90 minute lectures) to spare for introducing Prolog on the ...
12
votes
3answers
322 views
funsplit and polarity of Pi-types
In a recent thread on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark.
My understanding is that $\eta$ laws come with negative
...
8
votes
1answer
820 views
About Inverse 3-SAT
Context: Kavvadias and Sideri have shown that the Inverse 3-SAT problem is coNP Complete:
Given $\phi$ a set of models on $n$ variables, is there a 3-CNF formula such that $\phi$ is its exact set of ...
3
votes
1answer
106 views
About Closure under Resolution
The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. ...
10
votes
1answer
208 views
A 3-CNF formula that requires resolution width $5$
Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. For every $w$, there are unsatisfiable formulas $F$ in ...
6
votes
1answer
121 views
What is the benefit of Krivine's notation?
I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
4
votes
1answer
122 views
Explanation of 1-generic to prove undecidability of halting problem
This question is about an answer in question
Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ?
Bjørn Kjos-Hanssen ...
8
votes
1answer
248 views
logic in the presence of doubt, uncertainty, lies
I was reading Harry Frankfurt's On Bulls*t, a 1986 philosophical essay about this blurry notion between truth and falsity.
This is not a gratuitous exercise. This may have applications to computer ...
2
votes
1answer
166 views
What is a commutative transitive closure operator?
When reading about descriptive complexity theory, I have read about a "commutative transitive closure operator". I understand transitive closure operators, but what is a commutative transitive closure ...
7
votes
2answers
652 views
How can we express “$P=PSPACE$” as a first-order formula? [closed]
How can we express "$P=PSPACE$" as a first-order formula?
Which level of the arithmetic hierarchy contains this formula (and what is the currently known minimum level of the hierarchy that contains ...
8
votes
2answers
287 views
Is propositional resolution a complete proof system?
This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution".
This question is something extremely basic but it has been bothering me ...
2
votes
1answer
109 views
Relation between interval temporal logic and linear temporal logic
I am trying to understand the relation between interval temporal logic and linear temporal logic. Do the two form of expressing temporal constraints have the same expressive power, or is one of the ...
8
votes
1answer
159 views
Schaefer's theorem and CSPs of unbounded width
Schaefer's dichotomy theorem shows that each CSP problem over $\{0,1\}$ is either solvable in polynomial time or is NP-complete. This applies only for CSP problems of bounded width, excluding SAT and ...
0
votes
1answer
110 views
How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example)
I am looking for a preferably simple property that is expressible in ECTL* but not in CTL* and not in Büchi, with a citable reference to the proof.
Details of what I've tried:
I've tried a ...
8
votes
1answer
181 views
CTL* and mu-calculus
it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the ...
15
votes
5answers
570 views
How should I think about proof nets?
In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of ...
5
votes
1answer
89 views
CNF Rule hierarchy discovery
This is bothering me for some time. Consider that I have a set of CNF formulae:
$F_1 = \left( A \lor B \lor C \right) \land \left( C \lor D \lor E \right) \land \left( B \lor F \lor G \right)$
$F_2 ...
3
votes
2answers
184 views
Inductive definition of ECTL*: how are recursive formulas forbidden?
In [1], the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi ...
13
votes
7answers
487 views
Pointers for CS applications of logic
I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set ...
9
votes
1answer
134 views
Combinators for the Primitive Recursive Functions
It is well-known that the S and K combinators are Turing Complete. Are there combinators that suffice to yield (only) the primitive recursive functions?
7
votes
2answers
463 views
Free theorems, where?
I've found this webapp which lets you generate a free theorem for a given type.
The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of ...
13
votes
1answer
232 views
Is MALL + unrestricted recursive types Turing-complete?
If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator:
$$
\begin{array}{lcl}
\omega & = & (\lambda x.\,x\;x)\;(\lambda ...
7
votes
0answers
118 views
Boolean formula balancing in $\mathsf{AC^0}$
I am looking for references about the complexity of Boolean formula balancing problem. In particular,
Was it known that Boolean formulas can be balanced in $\mathsf{AC^0}$?
Is there a simple proof ...
3
votes
1answer
187 views
How to formally model the “hesitation” in the hat-guessing puzzle and prove it by mathematical induction?
The following question was first presented in MATHEMATICS of StackExchange. With a simple description at first sight, it has far-reaching consequences on plenty of recent and advanced theories, such ...
6
votes
2answers
152 views
Fragments of the mu calculus
I would like to know if somebody has studied the following very simple fragment of the modal mu-calculus:
$$F::= X \;| \; p \; | \; F \wedge G \; | \; [a]F \; | \; \nu X.F$$
where p ranges over ...
7
votes
1answer
129 views
Trying understand a move in Cohen's proof of the independence of the continuum hypothesis
I've read a few different presentations of Cohen's proof. All of them (that I've seen) eventually make a move where a Cartesian product (call it CP) between the (M-form of) $\aleph_2$ and $\aleph_0$ ...
8
votes
2answers
468 views
The relation of Gödel's Incompleteness Theorems to the Church-Turing Thesis
This may be a naive question, but here goes. (Edit -- it is not getting upvotes, but nobody has offered a response either; perhaps the question is more difficult, obscure, or unclear than I thought?)
...
10
votes
3answers
306 views
How is duality of types defined?
In Wadler's Recursive Types for Free! [1], he demonstrated two types, $\forall X . (F(X) \rightarrow X) \rightarrow X$ and $\exists X . (X \rightarrow F(X)) \times X$, and claimed they are dual. In ...
6
votes
1answer
151 views
Why is combinational logic called so?
What is the significance of the word "combinational" in combinational logic?
1
vote
0answers
80 views
Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$
A least-fixed point (LFP) formula is $\leq m$-invariant iff f.a. structrues $\mathcal{A}$ with $|A| \leq m$ and all orderings $<_1,<_2$ on $A$
$$(\mathcal{A},<_1) \models_{LFP} \varphi ...
6
votes
3answers
192 views
“Guarded” negative occurrences in definition of inductive types, always bad?
I know how some negative occurrences can definitively be bad:
...
8
votes
0answers
130 views
Sum-of-squares proof system
Recently I have seen several articles on arxiv that refer to a proof system called sum-of-squares.
Can someone explain what is a sum-of-squares proof and why such proofs are important/interesting? (It ...
9
votes
1answer
109 views
A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?
Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
6
votes
1answer
256 views
Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?
This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory.
The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
1
vote
1answer
91 views
How to generalize a map of type for many operators?
I am formalizing the type system for a small language, and thus writing inference rules.
Taking unary - operator for example, its entry may be a number as well as ...
2
votes
1answer
87 views
How to auto-derivate sequential iterative programs from a mathematical specification?
I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.
First, write down the formal specification as a Hoare triple and figure ...
5
votes
2answers
327 views
Understanding least-fixed point logic
To better understand a paper I'm trying to get a brief understanding of least-fixed point logic. There are a few points where I am stuck.
If $G = (V,E)$ is a graph and
$$ \Phi(P) = \{(a,b) \mid G ...
