# Questions tagged [lo.logic]

Computational and mathematical logic.

448 questions
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. ...
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.
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 ...
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 ...
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 ...
214 views

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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 Quantiﬁers, where he discusses how the possibility of quantifier reversing ...
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/...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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$ ...
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 ...
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 ...
311 views

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 ...