All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Previous Page 3 Next

Displaying 41 – 60 of 105

Showing per page

FSP and FLTL framework for specification and verification of middle-agents

Amelia Bădică, Costin Bădică (2011)

International Journal of Applied Mathematics and Computer Science

Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers....

Induction and decision procedures.

Deepak Kapur, Jürgen Giesl, Mahadevan Subramaniam (2004)

RACSAM

Mechanization of inductive reasoning is an exciting research area in artificial intelligence and automated reasoning with many challenges. An overview of our work on mechanizing inductive reasoning based on the cover set method for generating induction schemes from terminating recursive function definitions and using decision procedures is presented. This paper particularly focuses on the recent work on integrating induction into decision procedures without compromising their automation.

Inf-datalog, modal logic and complexities

Eugénie Foustoucos, Irène Guessarian (2009)

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

Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [16]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity...

Inf-datalog, Modal Logic and Complexities

Eugénie Foustoucos, Irène Guessarian (2007)

RAIRO - Theoretical Informatics and Applications

Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [CITE]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity...

Les I -types du système ℱ

K. Nour (2001)

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

Nous démontrons dans ce papier que les types du système ℱ habités uniquement par des λ I -termes (les I -types) sont à quantificateur positif. Nous présentons ensuite des conséquenses de ce résultat et quelques exemples.

Les I-types du système ℱ

K. Nour (2010)

RAIRO - Theoretical Informatics and Applications

We prove in this paper that the types of system ℱ inhabited uniquely by λI-terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.

Les types de données syntaxiques du système ℱ

Samir Farkh, Karim Nour (2001)

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

Nous présentons dans ce papier une définition purement syntaxique des types entrées et des types sorties du système ℱ . Nous définissons les types de données syntaxiques comme étant des types entrées et sorties. Nous démontrons que les types à quantificateurs positifs sont des types de données syntaxiques et qu’un type entrée est un type sortie. Nous imposons des restrictions sur la règle d’élimination des quantificateurs pour démontrer qu’un type sortie est un type entrée.

Les types de données syntaxiques du système ℱ

Samir Farkh, Karim Nour (2010)

RAIRO - Theoretical Informatics and Applications

We give in this paper a purely syntactical definition of input and output types of system ℱ . We define the syntactical data types as input and output types. We show that any type with positive quantifiers is a syntactical data type and that an input type is an output type. We give some restrictions on the ∀-elimination rule in order to prove that an output type is an input type.

Modeling of distributed objects computing design pattern combinations using a formal specification language

Toufik Taibi, David Ngo (2003)

International Journal of Applied Mathematics and Computer Science

Design patterns help us to respond to the challenges faced while developing Distributed Object Computing (DOC) applications by shifting developers' focus to high-level design concerns, rather than platform specific details. However, due to the inherent ambiguity of the existing textual and graphical descriptions of the design patterns, users are faced with difficulties in understanding when and how to use them. Since design patterns are seldom used in isolation but are usually combined to solve...

Object oriented institutions to specify symbolic computation systems

César Domínguez, Laureano Lambán, Julio Rubio (2007)

RAIRO - Theoretical Informatics and Applications

The specification of the data structures used in EAT, a software system for symbolic computation in algebraic topology, is based on an operation that defines a link among different specification frameworks like hidden algebras and coalgebras. In this paper, this operation is extended using the notion of institution, giving rise to three institution encodings. These morphisms define a commutative diagram which shows three possible views of the same construction, placing it in an equational algebraic...

On characteristic formulae for Event-Recording Automata

Omer Landry Nguena Timo, Pierre-Alain Reynier (2013)

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

A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that...

Currently displaying 41 – 60 of 105