UA-61751701-2

Order-Sorted Equality Enrichments Modulo Axioms
    • español
    • English
EscuelaIng
  • English 
    • español
    • English
  • Login
  • Inicio
  • Guías de Uso
    • Directrices
    • Procedimientos de Trabajo de Grado
    • Guía de Autoarchivo
    • Formato de Autorización para Publicación
  • Navegar
    • Comunidades
    • Autores
    • Títulos
    • Fechas
    • Materias
    • Tipo de Material
  • Investigadores
  • Organizaciones
  • Proyectos

Repositorio Digital

  • Comunities Comunities
  • Authors Authors
  • Titles Titles
  • Dates Dates
  • Subjects Subjects
  • Resource Type Resource Type
View Item 
  •   DSpace Home
  • 2 - Investigación
  • A - Grupos de Investigación
  • AD - CTG – Informática
  • View Item
  •   DSpace Home
  • 2 - Investigación
  • A - Grupos de Investigación
  • AD - CTG – Informática
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Cambiar vista

Browse

All of DSpaceCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsResource TypeThis CollectionBy Issue DateAuthorsTitlesSubjectsResource Type

My Account

LoginRegister

Statistics

View Usage Statistics

Order-Sorted Equality Enrichments Modulo Axioms


Gutiérrez, Raúl
Meseguer, José
Rocha, Camilo

Capítulo - Parte de Libro

2012

Springer

Teoría EcuacionalBuscar en Repositorio UMECIT
Obligación de pruebaBuscar en Repositorio UMECIT
Transformación de la teoríaBuscar en Repositorio UMECIT
Especificación algebraicaBuscar en Repositorio UMECIT
Álgebra InicialBuscar en Repositorio UMECIT
Equational TheoryBuscar en Repositorio UMECIT
Proof ObligationBuscar en Repositorio UMECIT
Theory TransformationBuscar en Repositorio UMECIT
Algebraic SpecificationBuscar en Repositorio UMECIT
Initial AlgebraBuscar en Repositorio UMECIT

Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation E↦E≃ that extends an algebraic specification E to a specification E≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation E↦E≃ preserves all the just-mentioned properties of E . The transformation has been automated in Maude using reflection and is used in several Maude formal tools.
 
Los predicados de igualdad y desigualdad incorporados basados ​​en la comparación de formas canónicas en especificaciones algebraicas se usan con frecuencia porque son prácticos y eficientes. Sin embargo, su uso sitúa las especificaciones algebraicas con semántica inicial del álgebra más allá de las herramientas de prueba de teoremas basadas, por ejemplo, en técnicas de inducción explícitas o sin inducción, y de otras herramientas formales para verificar propiedades clave como la confluencia, la terminación y la completitud suficiente. En cambio, tales especificaciones serían susceptibles de análisis formal si se les agregara un predicado de igualdad definido ecuacionalmente que enriqueciera los tipos de datos algebraicos. Además, tener un predicado de igualdad definido ecuacionalmente es muy útil por derecho propio, particularmente en la demostración inductiva de teoremas. ¿Es posible definir efectivamente una transformación teórica E↦E≃ que extienda una especificación algebraica E a una especificación E≃ que tenga un predicado de igualdad definido ecuacionalmente? Este artículo responde afirmativamente a esta pregunta para una amplia clase de especificaciones E condicionales clasificadas por orden que son de orden decreciente, confluentes en el suelo y que terminan operacionalmente los axiomas del módulo B y tienen una subfirma de constructores. Los axiomas B pueden consistir en axiomas de asociatividad, de conmutatividad o de asociatividad-conmutatividad, de modo que los constructores sean módulo B libre. Probamos que la transformación E↦E≃ conserva todas las propiedades de E recién mencionadas. La transformación se ha automatizado en Maude mediante reflexión y se utiliza en varias herramientas formales de Maude.
 

https://repositorio.escuelaing.edu.co/handle/001/1859

Rewriting Logic and Its Applications

  • AD - CTG – Informática [76]

Descripción: Order-Sorted Equality Enrichments Modulo Axioms.png
Título: Order-Sorted Equality Enrichments Modulo Axioms.png
Tamaño: 28.45Kb

Order-Sorted Equality Enrichments Modulo Axioms.pngOpen Access


Show full item record

Cita

Cómo citar

Cómo citar

Miniatura

Thumbnail

Gestores Bibliográficos

Exportar a Bibtex

Exportar a RIS

Exportar a Excel

Buscar en google Schoolar

Buscar en microsoft academic

untranslated

Código QR

Envíos recientes

    No hay artículos recientes

Oferta académica

Carreras profesionales

Especializaciones

Maestrías

Doctorado

Nustros Campus

Introducción al campus

Tecnología

Fortalezas

Premios y reconocimientos

Flora y fauna

Visita el campus

Internacionalización

Programas y alianzas

Movilidad

Sobre la Escuela y Bogotá

Convenios internacionales, nacionales y con colegios

Ayuda

PQRSFC

Centro de Ayuda

Contáctenos

Habeas Data

Centro de Servicios Tecnológicos

Directorio Escuela

acriditación institucional
icoMaps

AK. 45 No. 205 - 59, Autopista Norte.

PBX: +57(1) 668 3600 - Bogotá.

Línea nacional gratuita:

018000112668.

Sistema DSPACE - Metabiblioteca | logo