Now showing items 1-20 of 76

    • 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 ...
    • 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 ...
    • Bioescenarios III. 

      Mora, Juan José; Robayo Rodríguez, Sandra Milena (Asociación Colombiana de Ingenieros de Sistemas (ACIS)Colombia, 2008)
      El uso de las tendencias bioinspiradas en el desarrollo de soluciones informáticas se está imponiendo en el mundo por ser una opción en el tratamiento de problemas complejos. En Colombia se están realizando los primeros ...
    • 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 ...
    • A Graphical Environment for the Semantic Validation of a Plan Execution Language 

      Rocha, Camilo; Muñoz, Cesar; Cadavid, Hector (© Copyright 2021 IEEEUSA., 2009)
      This paper presents PLEXIL5, PLEXIL's formal interacting visual environment, a graphical environment providing an user-friendly interface to the formal operational semantics of PLEXIL. PLEXIL is a synchronous plan execution ...
    • 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 ...
    • 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 ...
    • 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 ...
    • 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 ...
    • 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 ...
    • Bioescenarios IV Inteligencia de enjambres: optimización por cúmulos de partículas 

      Casallas Fonseca, Carlos Eduardo; Vargas Aristizábal, Steven Francisco (Asociación Colombiana de Ingenieros de Sistemas (ACIS)Colombia, 2010)
      Conocer técnicas como las de los algoritmos bioinspirados, que han mostrado simplicidad y eficiencia en la solución de problemas complejos, es útil para los Ingenieros de Sistemas. Bioescenarios IV crea modelos para el ...
    • Comunidades 2.0 

      Díaz Rozo, Mónica Alejandra; Díaz Rozo, María Irma (Asociación Colombiana de Ingenieros de Sistemas (ACIS)Colombia, 2010-10)
      La generación de herramientas llamada Web 2.0 está transformando la manera de comunicarnos, aprender y trabajar. Específicamente ha permitido la conformación de las llamadas Comunidades 2.0 auto organizadas de manera ...
    • Aprendizajes de programación de computadores y resolución de problemas en un ambiente de trabajo en colaboración 

      Castañeda Bermudez, Claudia Patricia (Educación para el siglo XXIColombia., 2011)
      En esta investigación exploro los efectos, en el aprendizaje de programación de computadores de alumnos universitarios, de una estrategia de aprendizaje que integra trabajo en colaboración y resolución de problemas, el ...
    • 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 ...
    • 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 ...
    • 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 ...