AD - CTG – InformáticaClasificación B- Convocatoria 2018https://repositorio.escuelaing.edu.co/handle/001/10712024-03-29T11:28:23Z2024-03-29T11:28:23ZAn Inductive Theorem on the Correctness of General Recursive ProgramsBohórquez, Jaimehttps://repositorio.escuelaing.edu.co/handle/001/19132023-06-07T19:27:24Z2007-01-01T00:00:00ZAn Inductive Theorem on the Correctness of General Recursive Programs
Bohórquez, Jaime
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; Probamos un teorema inductivo relativamente simple (análogo al teorema de invariancia de Floyd y Dijkstra para programas iterativos) para verificar la corrección de una amplia clase de programas recursivos generales no deterministas. Este resultado se basa en la semántica relacional de Hoare y Jifeng. Al considerar la estructura de su código y especificación, proponemos condiciones de regularidad sobre el predicado transformador asociado a la ecuación de punto fijo de un programa recursivo general (no determinista) para demostrar que es correcto por inducción sobre una ordenación bien fundamentada de una cobertura del dominio de su correspondiente relación input-output. Todas las soluciones de punto fijo asociadas a un transformador predicado que satisfacen estas condiciones de regularidad coinciden cuando se restringen al dominio de su solución de punto fijo mínimo. Encontramos estas condiciones no indebidamente restrictivas, ya que los operadores continuos que definen programas deterministas como sus correspondientes soluciones de punto fijo mínimo deben cumplirlas. Presentamos programas deterministas (considerados como soluciones mínimas de ecuaciones de punto fijo) en una restricción del lenguaje de programación P de Hoare y Jifeng de relaciones finitas (parciales) en las soluciones máximas de ecuaciones de punto fijo expresadas en términos de relaciones "totales finitarias" de una restricción adecuada de su lenguaje D
2007-01-01T00:00:00ZTheorem Proving Modulo Based on Boolean Equational ProceduresRocha, CamiloMeseguer, Joséhttps://repositorio.escuelaing.edu.co/handle/001/19122022-11-22T08:00:54Z2008-01-01T00:00:00ZTheorem Proving Modulo Based on Boolean Equational Procedures
Rocha, Camilo; Meseguer, José
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.; Deducción con reglas de inferencia Las reglas de cálculo del módulo juegan un papel importante en la deducción automatizada como un método eficaz para escalar. Presentamos cuatro teorías ecuacionales que son isomorfas a la teoría booleana tradicional y mostramos que cada una de ellas da lugar a un procedimiento de decisión booleano basado en un sistema canónico de reescritura módulo asociatividad y conmutatividad. Luego, presentamos dos extensiones modulares de nuestro procedimiento de decisión para la lógica proposicional de Dijkstra-Scholten al Cálculo Secuente para Lógica de Primer Orden ya la Lógica Silogística con Complementos de L. Moss. Estas extensiones toman la forma de teorías de reescritura que son sólidas y completas para realizar la deducción módulo de sus partes ecuacionales y exhiben buenas propiedades de mecanización. Ilustramos la utilidad práctica de este enfoque mediante una implementación directa de una de estas teorías en Maude, reescribiendo el lenguaje lógico y demostrando automáticamente un punto de referencia de desafío en la demostración de teoremas.
2008-01-01T00:00:00ZMediation System for cooperative activities: knowledge system designOspina-Becerra, Victoria EugeniaFougères, Alain-Jérômehttps://repositorio.escuelaing.edu.co/handle/001/19112022-07-01T14:54:34Z2008-01-01T00:00:00ZMediation System for cooperative activities: knowledge system design
Ospina-Becerra, Victoria Eugenia; Fougères, Alain-Jérôme
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.; En este artículo presentamos el uso del conocimiento para un Sistema de Mediación, desarrollado para dar soporte a las actividades del diseñador de sistemas mecánicos. El uso de sistemas cooperativos debe contener un nivel de asistencia suficiente para facilitar y coordinar las actividades de los actores. Para lograr este objetivo introducimos un actor artificial: el Mediador. Para ilustrar nuestro enfoque presentaremos la especificación del conocimiento del Sistema de Mediación.
2008-01-01T00:00:00ZIntuitionistic Logic according to Dijkstra’s Calculus of Equational DeductionBohórquez, Jaimehttps://repositorio.escuelaing.edu.co/handle/001/19102022-07-01T14:32:55Z2008-01-01T00:00:00ZIntuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
Bohórquez, Jaime
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.; 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.
2008-01-01T00:00:00Z