Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [lo.logic]

Computational and mathematical logic.

9
votes
1answer
664 views

Hyperdoctrines and Monadic Second Order Logic

This question is essentially the question I asked on Mathoverflow. Monadic Second Order (MSO) logic is second order logic with quantification over unary predicates. That is, quantification over sets. ...
10
votes
3answers
2k views

Symbolic Execution is a case of Abstract Interpretation?

This is written in the wiki entry of Symbolic Execution, but I can't find any reference for it. Can anyone show me a pointer? Thank you.
2
votes
2answers
407 views

Questions about special types of partial assignments

Considering the definition "2-SAT: Given a CNF formula whose clauses have exactly 2 literals, does there exist an assignment of $\mathsf{TRUE}$ or $\mathsf{FALSE}$ to the variables that will ...
3
votes
2answers
361 views

Derivation of cut rule in sequent calculus

I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived. I found this paper but it uses implication elimination rule which I cannot ...
3
votes
1answer
110 views

Program transformation using partial functions which preserve partial correctness

Much work has been done demonstrating that certain program transformations preserve particular properties. That is, for any program $P$ which has property $\alpha$, show that $P$ transformed under ...
1
vote
2answers
214 views

Using partial functions to prove correctness

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given: $P$ is a family of programs, parameterized by a function $f$. Write $...
12
votes
4answers
864 views

Start learning proof complexity

I recently started to read a lot about proof complexity and have been really enjoying what I have been reading. I would really like to learn more about this, but I am having difficulty finding some ...
5
votes
1answer
205 views

Lower bounds for formulae sizes for addition

I am interested in the conversion of $\sum_{i=1}^n x_i = y$ to 3-CNF. Here $x_i$ is a binary 0/1 variable and $y$ is some positive integer. There are a number of practical methods for doing this, ...
3
votes
2answers
216 views

All literals implied by a set of horn clauses

What is the name of this problem: given a set of Horn clauses (in fact just definite clauses and facts), find the set of literals which can be deduced from it. E.g. given $\{a, a \Rightarrow b, b \...
6
votes
1answer
279 views

Bounded computation and incompleteness

Is there a complete theory T over a logical language L such that bounded computation may be encoded in it? Computational questions can be framed as arithmetical ones by interpreting them over natural ...
13
votes
1answer
331 views

Good reference about approximate methods for solving logic problems

It is known that many logic problems (e.g. satisfiability problems of several modal logics) are not decidable. There are also many undecidable problems in algorithm theory, e.g. in combinatorial ...
1
vote
1answer
276 views

Logic, language, semantics and more

I am working on a project that requires me to learn about logic (specially first order and second order). Looking for a good book or online reference that can help me with questions such as: A. What ...
5
votes
1answer
186 views

Typing relations terminology – how do I read typing relations?

I am currently trying to read up on type theory and have some quick questions on terminology. In the following rule, $$ \frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2} $$ How ...
2
votes
0answers
93 views

Satisfaction and synthesis of models in logics

It is well known that for propositional logic, the problem of constructing a model of a given formula is equivalent to deciding whether the formula has a model. Satisfiability is NP-complete, and ...
1
vote
1answer
223 views

What is resolution ((in FOL))? [closed]

I'm searching for an authoritative definition of resolution (logic resolution). Preferably on a reference freely available on the Internet (so I can read it right now). If this is too broad then ...
7
votes
1answer
222 views

Measurability of an $\omega$-regular language

It the previous question of mine I put a reference which shows that any $\omega$-regular language over the alphabet $\Sigma$ is a Borel subset of $\Sigma^\omega$. I am not sure whether the reference I ...
11
votes
2answers
1k views

Enumerate all solutions of a SAT problem

All the #SAT solvers I know, e.g RelSat, C2D, only return the number of satisfiable instances. But I want to know each of those instances? Is there such a #SAT solver or how I should modify an ...
3
votes
0answers
105 views

When can an inner existential quantifier be eliminated in favour of a function relating terms?

I have a question which somehow relates to the great answer by Bauer in the question Techniques for Reversing the Order of Quantifiers, where he discusses how the possibility of quantifier reversing ...
7
votes
4answers
222 views

What is the state of the art in theory of “Software transformations preserving behavior”?

I am interested in the field that could perhaps be referred to as "Automated Refactory" or "Preservation of Software Properties" after a transformation/change/refactory. Saying we have an instruction/...
2
votes
1answer
88 views

What can we say about a fixed point for a provability predicate in deductively defined theory that satisfies diagonalisation lemma

I am wondering whether this is the right site to ask this question, but since it involves proof and diagonalisation, hopefully it is the right place. I am curious and trying to reason about what ...
23
votes
4answers
2k 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 ...
-1
votes
1answer
98 views

Constructing automata with the same traces, but where a CTL-formula is not equally satisfied [closed]

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 ...
9
votes
3answers
143 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 ...
16
votes
1answer
479 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
109 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 ...
1
vote
1answer
113 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$ ...
17
votes
3answers
497 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 only ...
10
votes
1answer
389 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 ...
7
votes
1answer
311 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 $\Sigma^\...
27
votes
2answers
4k 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 ...
6
votes
1answer
639 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 ...
18
votes
3answers
848 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 ...
10
votes
2answers
1k 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 ...
4
votes
1answer
179 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. ...
13
votes
1answer
421 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 3-...
8
votes
1answer
211 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
176 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 answer ...
8
votes
1answer
360 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
281 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 ...
9
votes
2answers
899 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 it)...
15
votes
2answers
2k 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 ...
4
votes
2answers
279 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 ...
12
votes
1answer
241 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 ...
1
vote
1answer
364 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 ...
9
votes
1answer
861 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 $\mu$-...
23
votes
6answers
2k 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
158 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 =...
4
votes
2answers
291 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 ...
17
votes
7answers
921 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 theory....
19
votes
1answer
535 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?