{"id":{"repo_id":"sevilla","oai_identifier":"oai:idus.us.es:11441/23903"},"canonical_url":"https://search.dev.ndltd.org/etd/sevilla/oai:idus.us.es:11441/23903","repository":{"repo_id":"sevilla","name":"Universidad de Sevilla","base_url":"https://idus.us.es/server/oai/request"},"display":{"title":"Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades","abstract":"El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.|","abstract_html":"El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.|","abstract_has_math":false,"creators":["Ruiz Reina, José Luis"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Alonso Jiménez, José Antonio"],"committee_chairs":[],"committee_members":[],"year":2001,"date_issued":"2001","date_published":"2001","updated_at":"2026-07-24T04:29:54Z","subjects":[],"languages":["spa"],"rights":["Atribución-NoComercial-SinDerivadas 4.0 España"],"rights_urls":["http://creativecommons.org/licenses/by-nc-nd/4.0/"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/11441/23903","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Alonso Jiménez, José Antonio"]},{"key":"dc:creator","label":"Author","values":["Ruiz Reina, José Luis"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2015-04-16T09:19:05Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2015-04-16T09:19:05Z"]},{"key":"dc:date.issued","label":"Date","values":["2001"]},{"key":"dc:type","label":"Dc Type","values":["doctoral thesis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["spa"]},{"key":"dc:rights","label":"Dc Rights","values":["Atribución-NoComercial-SinDerivadas 4.0 España"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://creativecommons.org/licenses/by-nc-nd/4.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/11441/23903"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.|"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades"]}]}],"canonical_facts":{"dc:contributor.advisor":["Alonso Jiménez, José Antonio"],"dc:creator":["Ruiz Reina, José Luis"],"dc:date.accessioned":["2015-04-16T09:19:05Z"],"dc:date.available":["2015-04-16T09:19:05Z"],"dc:date.issued":["2001"],"dc:description.abstract":["El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.|"],"dc:format":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/11441/23903"],"dc:language.iso":["spa"],"dc:rights":["Atribución-NoComercial-SinDerivadas 4.0 España"],"dc:rights.uri":["http://creativecommons.org/licenses/by-nc-nd/4.0/"],"dc:title":["Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades"],"dc:type":["doctoral thesis"]},"updated_at":"2026-07-24T04:29:54Z"}