La demostración automática de teoremas en Geometría elemental y su repercusión didáctica

Autor: I. Miranda Díaz

Publikováno v: Dipòsit Digital de Documents de la UAB
Universitat Autònoma de Barcelona
Enseñanza de las ciencias: revista de investigación y experiencias didácticas; 1988: Vol.: 6 Núm.: 1; p. 61-65
Enseñanza de las Ciencias: revista de investigación y experiencias didácticas; 1988: Vol.: 6 Núm.: 1; p. 61-65
Redined, Red de Información Educativa
Ministerio de Educación, Cultura y Deporte (MECD)

Resumen basado en el de la publicación Resumen en inglés El papel relevante de las tareas de validación en la enseñanza tradicional de la geometría se aborda actualmente como una mera introducción al razonamiento lógico. La existencia de algor

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be4ee31d5fe98ed7f637dbff10969083
https://doi.org/10.5565/rev/ensciencias.5063

Resolución SL*: Un paradigma basado en resolución lineal para la demostración automática

Autor: Casamayor Rodenas, Juan Carlos

Publikováno v: Riunet.

El trabajo incluido en la presente tesis se enmarca dentro del campo de la demostración automática de teoremas y consiste en la estudio, definición y desarrollo de un paradigma de resolución lineal, denominado Resolución SL*. La razón para util

Externí odkaz: http://hdl.handle.net/10251/6023

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

Autor: Ruiz Reina, José Luis

Publikováno v: idUS. Depósito de Investigación de la Universidad de Sevilla
instname

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 ecuac

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::107aacb921609b0d31f8cc2548a8039b
https://idus.us.es/handle/11441/23903

Reconstructing propositional proofs in type theory

Autor: Prieto Cubides, Jonathan Steven

Publikováno v: Repositorio EAFIT
Universidad EAFIT
instacron:Universidad EAFIT

We describe a syntactical proof-reconstruction approach to verify derivations generated by Metis prover to theorems in classical propositional logic -- To verify such derivations, we formalize in type theory each inference rule of the Metis reasoning

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::17b8bba8391e4176a5e860920efcc224
http://hdl.handle.net/10784/12484

Teoría computacional (en ACL2) sobre cálculos proposicionales

Autor: Martín Mateos, Francisco Jesús

Publikováno v: idUS. Depósito de Investigación de la Universidad de Sevilla
instname

En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2. Premio Extraordinario de Doctorado US

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::628faeeed2469638cb3864fa266d5279
https://idus.us.es/handle/11441/14970