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

Recent Submissions

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

View more