# Questions tagged [lo.logic]

Computational and mathematical logic.

474 questions
Filter by
Sorted by
Tagged with
386 views

416 views

339 views

163 views

### Using MSOL for solving BIDS problem

From "Linear Time Solvable Optimization Problems on Graphs of Bounded Clique Width" (B. Courcelle et al) we know that any problem that can be written on MSOL (Monadic Second Order Logic) has a linear ...
228 views

### Papers on applying CTL over LTSs

Normally model checking with specifications written in CTL*/CTL is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance ACTL. ...
6k views

### What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
522 views

### What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation. For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
494 views

### Finding a finite model

I know that the question "does a first order formula $\phi$ have a model" is undecidable in general. Could anyone give me a link or a book which give the answer for finite models. If I have a first ...
1k views

1k views

### Results in Theoretical CS independent of ZFC

I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish. QUESTION: Are you aware of any interesting result in CS ...
Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator: $\Diamond A =_{def} \neg A \to A$ (which he ...
Banach's fixed point theorem says that if we have a nonempty complete metric space $A$, then any uniformly contractive function $f : A \to A$ it has a unique fixed point $\mu(f)$. However, the proof ...