Displaying similar documents to “Inf-datalog, Modal Logic and Complexities”

On Core XPath with Inflationary Fixed Points

Loredana Afanasiev, Balder Ten Cate (2013)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

We prove the undecidability of Core XPath 1.0 (CXP) [G. Gottlob and C. Koch, in IEEE CS Press (2002) 189–202.] extended with an operator. More specifically, we prove that the satisfiability problem of this language is undecidable. In fact, the fragment of CXP+IFP containing only the and axes is already undecidable.

Denotational aspects of untyped normalization by evaluation

Andrzej Filinski, Henning Korsholm Rohde (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We show that the standard normalization-by-evaluation construction for the simply-typed -calculus has a natural counterpart for the untyped -calculus, with the central type-indexed logical relation replaced by a “recursively defined” , in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...

A Note on Negative Tagging for Least Fixed-Point Formulae

Dilian Gurov, Bruce Kapron (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

Proof systems with sequents of the form ⊢ Φ for proving validity of a propositional modal -calculus formula Φ over a set of states in a given model usually handle fixed-point formulae through unfolding, thus allowing such formulae to reappear in a proof. Tagging is a technique originated by Winskel for annotating fixed-point formulae with information about the proof states at which these are unfolded. This information is used later in the proof to avoid unnecessary unfolding,...

Regularity of languages defined by formal series with isolated cut point

Alberto Bertoni, Maria Paola Bianchi, Flavi D’Alessandro (2012)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

Let  = { ∈  | ()  } be the language recognized by a formal series :  → ℝ with isolated cut point . We provide new conditions that guarantee the regularity of the language in the case that is rational or is a Hadamard quotient of rational series. Moreover the decidability property of such conditions is investigated.

Integers in number systems with positive and negative quadratic Pisot base

Z. Masáková, T. Vávra (2014)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

We consider numeration systems with base and − , for quadratic Pisot numbers and focus on comparing the combinatorial structure of the sets Z and Z of numbers with integer expansion in base , resp. − . Our main result is the comparison of languages of infinite words and coding the ordering of distances between consecutive - and (− )-integers. It turns out that for a class of roots of − − , the languages coincide, while for other...

Closure properties of hyper-minimized automata

Andrzej Szepietowski (2011)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

Two deterministic finite automata are almost equivalent if they disagree in acceptance only for finitely many inputs. An automaton is hyper-minimized if no automaton with fewer states is almost equivalent to . A regular language is canonical if the minimal automaton accepting is hyper-minimized. The asymptotic state complexity () of a regular language is the number of states of a hyper-minimized automaton for a language finitely different from . In this paper we show...

Topologies, Continuity and Bisimulations

J. M. Davoren (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

The notion of a is of basic importance in many areas of computation theory and logic. Of late, it has come to take a particular significance in work on the formal analysis and verification of , where system properties are expressible by formulas of the modal -calculus or weaker temporal logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag conditions are suggestive of some form of continuity. We give a topological...

Closure properties of hyper-minimized automata

Andrzej Szepietowski (2012)

RAIRO - Theoretical Informatics and Applications

Similarity:

Two deterministic finite automata are almost equivalent if they disagree in acceptance only for finitely many inputs. An automaton is hyper-minimized if no automaton with fewer states is almost equivalent to . A regular language is canonical if the minimal automaton accepting is hyper-minimized. The asymptotic state complexity () of a regular language is the number of states of a hyper-minimized automaton...

Idealized coinductive type systems for imperative object-oriented programs

Davide Ancona, Giovanni Lagorio (2011)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of intermediate form programs into Horn formulas, where functions correspond to union...

Solving multi-agent scheduling problems on parallel machines with a global objective function

F. Sadi, A. Soukhal, J.-C. Billaut (2014)

RAIRO - Operations Research - Recherche Opérationnelle

Similarity:

In this study, we consider a scheduling environment with ( ≥ 1) parallel machines. The set of jobs to schedule is divided into disjoint subsets. Each subset of jobs is associated with one agent. The agents compete to perform their jobs on common resources. The objective is to find a schedule that minimizes a global objective function , while maintaining the regular objective function of each agent, , at a level no greater than a fixed value, ...

Encoding FIX in Object Calculi

Roy L. Crole (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We show that the type theory introduced by Crole and Pitts [3] can be encoded in variants of Abadi and Cardelli's object calculi. More precisely, we show that the type theory presented with judgements of both equality and operational reduction can be translated into object calculi, and the translation proved sound. The translations we give can be seen as using object calculi as a metalanguge within which can be represented; an analogy can be drawn with Martin Löf's Theory of Arities...

A note on constructing infinite binary words with polynomial subword complexity

Francine Blanchet-Sadri, Bob Chen, Sinziana Munteanu (2013)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

Most of the constructions of infinite words having polynomial subword complexity are quite complicated, , sequences of Toeplitz, sequences defined by billiards in the cube, etc. In this paper, we describe a simple method for constructing infinite words over a binary alphabet  {  }  with polynomial subword complexity . Assuming contains an infinite number of ’s, our method is based on the gap function which gives the distances between consecutive ’s. It is known that...

Equality sets for recursively enumerable languages

Vesa Halava, Tero Harju, Hendrik Jan Hoogeboom, Michel Latteux (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We consider shifted equality sets of the form , where and are nonerasing morphisms and is a letter. We are interested in the family consisting of the languages , where is a coding and is a shifted equality set. We prove several closure properties for this family. Moreover, we show that every recursively enumerable language is a projection of a shifted equality set, that is, for some (nonerasing) morphisms and and...