Browse by

By Issue Date Authors Titles Subjects Resource Type

El grupo de investigación CTG-informática es un grupo interdisciplinario que se interesa en la ciencia, gestión e innovación en informática. Con especial interés en resolver y apoyar con tecnología que aumente la productividad a las organizaciones en su estrategia de negocio, contribuyendo así al desarrollo del país en la sociedad del conocimiento.

News

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Recent Submissions

Mediation System for cooperative activities: knowledge system design

Ospina-Becerra, Victoria Eugenia; Fougères, Alain-Jérôme (WSEAS, 2008)

In this article we present the use the knowledge for a Mediation System, developed to give support to mechanical system designer activities. The use of cooperative systems must contain a sufficient level of assistance to ...
Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

Bohórquez, Jaime (University of Notre Dame, 2008)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert’s style of proof and Gentzen’s deductive systems. In this context we call it CED ...
AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS

Fougères, Alain-Jérôme; Ospina-Becerra, Victoria Eugenia (In CognitoFrance, 2009)

Nous présentons, dans cet article, deux concepts pour améliorer l'assistance à la coopération en conception de systèmes mécaniques : 1) le concept de micro-outils développé pour assister l'activité elle-même des concepteurs ...
Agent-Based Mediation System to Facilitate Cooperation in Distributed Design

Ospina-Becerra, Victoria Eugenia; Fougères, Alain-Jérôme (WSEASE.E.U.U., 2009)

In this article we present the use of knowledge for a Mediation System, developed to give support to participants in mechanical-system-designer activities. To use a cooperative system sufficient assistance is needed to ...
La inteligencia de negocios, un concepto informático

Oramas, Joaquin (ACISColombia, 2009)

Diferente a lo que podría esperarse, el concepto de Business Intelligence no es un resultado de desarrollos en el mundo de las Ciencias Administrativas, sino que es un producto del progreso de la Informática o de ...
An Inductive Theorem on the Correctness of General Recursive Programs

Bohórquez, Jaime (Oxford University Press, 2007)

We prove a relatively simple inductive theorem (analogous to Floyd and Dijkstra's Invariance Theorem for iterative programs) to verify the correctness of an ample class of non-deterministic general recursive programs. This ...
Theorem Proving Modulo Based on Boolean Equational Procedures

Rocha, Camilo; Meseguer, José (Springer, 2008)

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean ...
An elementary and unified approach to program correctness

Bohórquez, Jaime (Springer, 2009)

We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra’s iterative style of programming ...
Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas

Cadavid Rengifo, Héctor Fabio; Gómez Perdomo, Jonatan (ScieloColombia, 2009)

En este artículo se describe un sistema desarrollado para la extracción de grandes cuerpos de texto de Internet, teniendo como motivación el valor que ofrecen los ejemplos de lenguaje natural disponibles en la red para ...
Rewriting Logic Semantics of a Plan Execution Language

Dowek, Gilles; Muñoz, César; Rocha, Camilo (E.E.U.U., 2010)

The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a ...
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Rocha, Camilo; Meseguer, José (SpringerBerlín, 2010)

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite ...
A formal library of set relations and its application to synchronous languages

Rocha, Camilo; Muñoz, César; Dowek, Gilles (Elsevier B.V., 2011)

Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and ...
Simulation and Verification of Synchronous Set Relations in Rewriting Logic

Rocha, Camilo; Múñoz, César (NASA Langley Research CenterHampton, Virginia., 2011)

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract ...
Towards a Maude Formal Environment

Durán, Francisco; Rocha, Camilo; Álvarez, José María (SpringerBerlín, 2011)

Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in ...
Intellifilter: sistema de filtrado parental soportado por aprendizaje maquinal supervisado

Cadavid Rengifo, Héctor Fabio; Cely Higuera, Jorge Humberto; García Segura, Juan Pablo (REDISColombia, 2011)

En este artículo se presenta la herramienta Intellifilter para el filtrado de contenidos de internet no aptos para niños, basada en un conjunto de técnicas de aprendizaje supervisado1 para clasificación de texto e imágenes, ...
Tool Interoperability in the Maude Formal Environment

Durán, Francisco; Rocha, Camilo; Álvarez, José María (SpringerBerlín, 2011)

We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the ...
Proving Safety Properties of Rewrite Theories

Rocha, Camilo; Meseguer, José (SpringerBerlín, 2011)

Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive ...
MUNDOS VIRTUALES INMERSIVOS PARA EDUCACIÓN, TRABAJO COLABORATIVO Y SIMULACIÓN

Álvarez Piñeiro, Claudia Patricia (ACOFIColombia, 2013)

Being able to observe the customs of teenagers and young adults known as ``digital natives'' has helped in understanding how they enjoy playing in simulated worlds. During the virtual gatherings, they are ...
Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

Rocha, Camilo; Meseguer, José (Springer., 2014)

The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a ...
The Formal System of Dijkstra and Scholten

Rocha, Camilo (Springer.Springer, Cham., 2015)

The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding ...

Envíos recientes

AD - CTG – Informática
...
|

Clasificación B- Convocatoria 2018

LEER
Mediation System for cooperative activities: knowledge system design
...
Ospina-Becerra, Victoria Eugenia | 2008

In this article we present the use the knowledge for a Mediation System, developed to give support to mechanical system designer activities. The use of cooperative systems must contain a sufficient level of assistance to facilitate and coordinate the actor’s activities. To accomplish this goal we introduce an artificial actor: the Mediator. To illustrate our approach we will present the specification of the knowledge of the Mediation System.

LEER
Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
...
Bohórquez, Jaime | 2008

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert’s style of proof and Gentzen’s deductive systems. In this context we call it CED (Calculus of Equational Deduction). This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations (in Dijkstra’s words, “letting the symbols do the work”) have led to the “calculational style,” an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system (I-CED), we prove Leibniz’s principle for intuitionistic logic and also prove that any (intuitionistic) valid formula of predicate logic can be proved in I-CED.

LEER
AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS
...
Fougères, Alain-Jérôme | 2009

Nous présentons, dans cet article, deux concepts pour améliorer l'assistance à la coopération en conception de systèmes mécaniques : 1) le concept de micro-outils développé pour assister l'activité elle-même des concepteurs et 2) le concept de système de médiation introduit pour faciliter la coopération des concepteurs. Un micro-outil est destiné à une tâche bien identifiée, dont il va faciliter ou améliorer l'exécution, tout en laissant à son utilisateur toute latitude dans l'organisation de son activité à une échelle plus globale. Pour supporter l'usage des micro-outils nous avons développé une plate-forme agent (PLACID : Plate-forme Logiciel d'Aide à la Conception Innovante et Distribuée). Celle-ci apporte une assistance au travail de co-conception, guidé ou non par des processus complexes de type workflow. L'utilisation de systèmes coopératifs doit comporter un niveau suffisant d'assistance pour faciliter et coordonner l'activité des acteurs (réalisation de tâches et résolution collective de problèmes). Pour cela nous introduisons dans les interrelations coopératives des acteurs un acteur artificiel, le Médiateur (ou système de médiation), dont le rôle est de servir d'intermédiaire de coopération. Ce rôle s'avère des plus pertinents lorsque les acteurs sont engagés dans des situations de travail coopératif distantes. Dans l'intention d'illustrer notre approche nous présentons la conception des micro-outils et du système de médiation que nous avons intégrés dans un atelier coopératif d'analyse fonctionnelle technique (l'atelier MO-AFT).

LEER
Agent-Based Mediation System to Facilitate Cooperation in Distributed Design
...
Ospina-Becerra, Victoria Eugenia | 2009

In this article we present the use of knowledge for a Mediation System, developed to give support to participants in mechanical-system-designer activities. To use a cooperative system sufficient assistance is needed to facilitate and coordinate actors’ activities. To accomplish this goal we introduce an artificial actor: Mediator.The Mediator forms part of the group of collaborative, with the specific role of facilitating the cooperative activity. This role of assistance, differentiate the Mediator from other actors. This one is endowed with specific skills of cooperation (communication; awareness, coordination, co-memorization), requiring some acquired knowledge, which allow them to give assistance to the human actors. We will define the types of knowledge defined for our proposed Mediation System. Then we will illustrate the use of memorized knowledge by the Mediator during an activity of technical functional analysis.

LEER
La inteligencia de negocios, un concepto informático
...
Oramas, Joaquin | 2009

Diferente a lo que podría esperarse, el concepto de Business Intelligence no es un resultado de desarrollos en el mundo de las Ciencias Administrativas, sino que es un producto del progreso de la Informática o de la recientemente denominada “infotecnología”.

LEER
An Inductive Theorem on the Correctness of General Recursive Programs
...
Bohórquez, Jaime | 2007

We prove a relatively simple inductive theorem (analogous to Floyd and Dijkstra's Invariance Theorem for iterative programs) to verify the correctness of an ample class of non-deterministic general recursive programs. This result is based on Hoare and Jifeng's relational semantics. By considering the structure of its code and specification, we propose regularity conditions on the predicate transformer associated to the fixed-point equation of a general (non deterministic) recursive program to prove it correct by induction on a well founded ordering of a covering of the domain of its corresponding input-output relation. All fixed point solutions associated to a predicate transformer satisfying these regularity conditions coincide when restricted to the domain of its least fixed point solution. We find these conditions non unduly restrictive, since continuous operators defining deterministic programs as their corresponding least fixed-point solutions must fulfill them. We couch deterministic programs (viewed as least solutions of fixed-point equations) in a restriction of Hoare and Jifeng's P programming language of (partial) finitary relations into the greatest solutions of fixed-point equations expressed in terms of “total finitary” relations of an adequate restriction of their D language

LEER
Theorem Proving Modulo Based on Boolean Equational Procedures
...
Rocha, Camilo | 2008

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.

LEER
An elementary and unified approach to program correctness
...
Bohórquez, Jaime | 2009

We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra’s iterative style of programming with Hehner’s recursive predicative programming theory, getting the “best of the two worlds” and without having to recur in any way to higher-order approaches such as predicate transformers, Hoare logic, fixed-point or relational theory.

LEER
Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas
...
Cadavid Rengifo, Héctor Fabio | 2009

En este artículo se describe un sistema desarrollado para la extracción de grandes cuerpos de texto de Internet, teniendo como motivación el valor que ofrecen los ejemplos de lenguaje natural disponibles en la red para las tareas de aprendizaje no supervisado de dichos naturales, dado por características como su enorme volumen, permanente actualización respecto de las alteraciones del lenguaje, y bajo costo, en tiempo y recursos, en cuanto a los mecanismos tradicionales de construcción de corpus para esas tareas de aprendizaje. Se presentan las estrategias incorporadas al sistema con el fin de maximizar el aprovechamiento de los recursos de hardware y así reducir los tiempos de extracción, al igual que se presentan las características de extensibilidad para los formatos soportados, y adaptabilidad respecto a la manera como el sistema limpia los contenidos para obtener muestras de lenguaje natural puras. Al final del artículo se presentan los resultados experimentales obtenidos con uno de los dominios de contenido en español más grande de Internet: es.wikipedia.org, a través de los cuales se concluye sobre la validez y aplicabilidad de un corpus extraído directamente de la Internet para un eventual proceso de aprendizaje de morfología o sintaxis.

LEER
Rewriting Logic Semantics of a Plan Execution Language
...
Dowek, Gilles | 2010

The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.

LEER
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
...
Rocha, Camilo | 2010

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.

LEER
A formal library of set relations and its application to synchronous languages
...
Rocha, Camilo | 2011

Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.

LEER
Simulation and Verification of Synchronous Set Relations in Rewriting Logic
...
Rocha, Camilo | 2011

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm verification techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the verification of temporal properties of a synchronous system.

LEER
Towards a Maude Formal Environment
...
Durán, Francisco | 2011

Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in the development of formal analysis tools for checking specific properties of Maude specifications. This includes tools for checking termination, confluence, and inductive properties of rewrite theories. Nevertheless, most of these tools have been designed to work in isolation, making it difficult, for instance, to exchange data between them and inconvenient to switch between their environments. This paper presents the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can interact with tools to mechanically verify properties of Maude specifications. One important aspect of this work is that the MFE has been designed to be easily extended with tools having highly heterogeneous designs whilst creating synergy among them. As a proof of concept, we report on the integration of five commonly used formal analysis tools for Maude specifications into MFE and illustrate their interoperability with an example.

LEER
Intellifilter: sistema de filtrado parental soportado por aprendizaje maquinal supervisado
...
Cadavid Rengifo, Héctor Fabio | 2011

En este artículo se presenta la herramienta Intellifilter para el filtrado de contenidos de internet no aptos para niños, basada en un conjunto de técnicas de aprendizaje supervisado1 para clasificación de texto e imágenes, junto con una infraestructura de interceptación de peticiones HTTP basada en software. Cuando Intellifilter esté habilitado en un equipo o red en particular, todos los contenidos solicitados mediante el protocolo HTTP serán evaluados por un conjunto de clasificadores previamente entrenados y, de acuerdo con el resultado de dicha categorización, se aceptará o no su entrega al destinatario original. Aunque la herramienta aún se encuentra en una fase ‘beta’, los resultados experimentales obtenidos con las técnicas utilizadas muestran resultados promisorios que indican que éste puede ser un buen punto de partida para el desarrollo de mecanismos de control de los contenidos de internet.

LEER
Tool Interoperability in the Maude Formal Environment
...
Durán, Francisco | 2011

We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the Church-Rosser Checker, the Coherence Checker, and the Maude Inductive Theorem Prover. We explain the high-level design decisions behind MFE, give a summarized account of its main features, and illustrate with an example the interoperation of the tools available in its current release.

LEER
Proving Safety Properties of Rewrite Theories
...
Rocha, Camilo | 2011

Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive approach for verifying safety properties of rewrite theories in which all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used in our inference system to further simplify the equational proof obligations to which all proofs of safety formulas are ultimately reduced. In this way, existing equational reasoning techniques and tools can be directly applied to verify safety properties of concurrent systems. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention.

LEER
MUNDOS VIRTUALES INMERSIVOS PARA EDUCACIÓN, TRABAJO COLABORATIVO Y SIMULACIÓN
...
Álvarez Piñeiro, Claudia Patricia | 2013

Being able to observe the customs of teenagers and young adults known as ``digital natives'' has helped in understanding how they enjoy playing in simulated worlds. During the virtual gatherings, they are able to connect with strangers while collaborating, generating strategies and employing a significant amount of time towards common goals. Consequently, the software industry works in building platforms for virtual worlds and the education industry has begun to analyze how to take advantage of these platforms for education purposes. These worlds, materialized as multi-user software, enable each participant, represented by an avatar, to be part of a 3D environment in which the interaction takes place by text or voice chat. In these worlds, it is possible to develop learning, socializing, simulation and immersion activities in situations pedagogically developed, so that each user can observe, interact, and make decisions virtually.This paper illustrates three case studies about virtual worlds with educational purposes. The first case study is about learning activities regarding the international humanitarian law; for this case study, the paper illustrates how the instructional design was carefully done.During the instructional design and the development of the learning experience, the need for tools supporting collaborative construction in the virtual world was identified, giving birth to a new project, which makes the second case study of the paper. The goal of this project was to develop tools for building concept maps and notes board virtually. The third case study is about using virtual worlds for simulating natural disasters situations such as, for instance, earthquakes.

LEER
Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
...
Rocha, Camilo | 2014

The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a formula to inductive properties of the underlying equational theory by means of the application of a few inference rules. Through the combination of various techniques such as unification, narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation, verifying automatically many proof obligations. Maude Inductive Theorem Prover (ITP) can be used to discharge the remaining obligations which are not automatically verified by InvA. Verification of the reliable communication ensured by the Alternating Bit Protocol (ABP) is used as a case study to explain the use of the InvA tool, and to illustrate its effectiveness and degree of automation in a concrete way.

LEER
The Formal System of Dijkstra and Scholten
...
Rocha, Camilo | 2015

The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding this logic to the point in which, for some time, it was not considered a logic, as logicians use the word. The main objections arise from the fact that: (i) symbolic manipulations seem to be based on the meaning of the terms involved, and (ii) some notation and the proof style of the logic are different, to some extent, from those found in the traditional use of logic. This paper presents the Dijkstra-Scholten logic as a formal system, and explains its proof-theoretic foundations as a formal system, thus avoiding any confusion regarding term manipulation, notation, and proof style. The formal system is shown to be sound and complete, mainly, by using rewriting and narrowing based decision and semi-decision procedures for, respectively, propositional and first-order logic previously developed by C. Rocha and J. Meseguer.

LEER

AD - CTG – Informática

Browse by

News

Recent Submissions

Mediation System for cooperative activities: knowledge system design ﻿

Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction ﻿

AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS ﻿

Agent-Based Mediation System to Facilitate Cooperation in Distributed Design ﻿

La inteligencia de negocios, un concepto informático ﻿

An Inductive Theorem on the Correctness of General Recursive Programs ﻿

Theorem Proving Modulo Based on Boolean Equational Procedures ﻿

An elementary and unified approach to program correctness ﻿

Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas ﻿

Rewriting Logic Semantics of a Plan Execution Language ﻿

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories ﻿

A formal library of set relations and its application to synchronous languages ﻿

Simulation and Verification of Synchronous Set Relations in Rewriting Logic ﻿

Towards a Maude Formal Environment ﻿

Intellifilter: sistema de filtrado parental soportado por aprendizaje maquinal supervisado ﻿

Tool Interoperability in the Maude Formal Environment ﻿

Proving Safety Properties of Rewrite Theories ﻿

MUNDOS VIRTUALES INMERSIVOS PARA EDUCACIÓN, TRABAJO COLABORATIVO Y SIMULACIÓN ﻿

Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool ﻿

The Formal System of Dijkstra and Scholten ﻿

Envíos recientes

AD - CTG – Informática

Mediation System for cooperative activities: knowledge system design

Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS

Agent-Based Mediation System to Facilitate Cooperation in Distributed Design

La inteligencia de negocios, un concepto informático

An Inductive Theorem on the Correctness of General Recursive Programs

Theorem Proving Modulo Based on Boolean Equational Procedures

An elementary and unified approach to program correctness

Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas

Rewriting Logic Semantics of a Plan Execution Language

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

A formal library of set relations and its application to synchronous languages

Simulation and Verification of Synchronous Set Relations in Rewriting Logic

Towards a Maude Formal Environment

Intellifilter: sistema de filtrado parental soportado por aprendizaje maquinal supervisado

Tool Interoperability in the Maude Formal Environment

Proving Safety Properties of Rewrite Theories

MUNDOS VIRTUALES INMERSIVOS PARA EDUCACIÓN, TRABAJO COLABORATIVO Y SIMULACIÓN

Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

The Formal System of Dijkstra and Scholten