Formal Proof: Theory and Practice - Historial de revisiones

Jalonso en 10:05 16 dic 2008

2008-12-16T10:05:13Z

Jalonso en 10:04 16 dic 2008

2008-12-16T10:04:17Z

Jalonso en 10:01 16 dic 2008

2008-12-16T10:01:01Z

Jalonso en 09:58 16 dic 2008

2008-12-16T09:58:39Z

Jalonso en 09:56 16 dic 2008

2008-12-16T09:56:44Z

Jalonso en 09:55 16 dic 2008

2008-12-16T09:55:30Z

Jalonso en 09:54 16 dic 2008

2008-12-16T09:54:08Z

Jalonso en 09:21 16 dic 2008

2008-12-16T09:21:58Z

Jalonso en 09:12 16 dic 2008

2008-12-16T09:12:11Z

Jalonso en 09:10 16 dic 2008

2008-12-16T09:10:57Z

@@ Línea 13: / Línea 13: @@
 # '''Conclusiones y prospectivas'''
 #* El uso de las demostraciones formales en matemáticas es una continuación natural del aumento del rigor.
-#* La formalización es un tranbajo pesado.
+#* La formalización es un trabajo pesado.
 #* El uso de asistentes de demostración puede aligerarlo y hacerlo divertido.
 #* Se progresará mediante la acumulación de bibliotecas de matemáticas formalizadas, la integración en los asistentes de procedimientos de decisión y la mejora de los lenguajes usados para expresar las demostraciones.

@@ Línea 4: / Línea 4: @@
 El resumen del artículo es el siguiente:
-# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de
+# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos: (''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396)).
-la certidumbre) y aplicaciones (revisión de artículos matemáticos y
+# '''Lógica formal'''. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad).
-verificación de sistemas informáticos); los avances en asistentes de prueba
+# '''Los fundamentos de la matemáticas'''. Presenta una historia de los fundamentos de la matemáticas: su inicio en los ''Elementos'' de Euclides, los problemas de los axiomas, la corriente logicista de Frege, la teorái de conjunto de Cantor, la paradoja de Russell y las soluciones mediante tipos o axiomas (de Zermelo-Fraenkel).  Termina comentando la relaciones entre tipos y teoría de conjunto, donde se decanta por los tipos (''Type-based approaches look immediately appealing, because mathematicians generally do make type distinctions: between points and lines, or between numbers and sets of numbers, etc.'' (p. 1398)).
-(más fácilidad de uso, más potencia y más retos superados) y, la relación entre
+# '''¿Formalización o proceso social?'''. Comenta que en la historia anterior hay distintas motivaciones: fundamentar la matemática (Russell, Frege, Hilbert, Brouwer) y mejorar su enseñanza (Peano). Respecto a la acualidad comenta la extensión del uso del lenguaje conjuntista en matemática, pero no el de la lógica (''as far as the mathematical community is concerned George Boole has lived in vain'' (Dijkstra)). La certificación de la matemática se hace mediante revisión entre pares y no formalmente. Este proceso de revisión presenta fallos: teoremas grandes (p.e. teorema de los cuatro colores y la conjetura de Kepler). La certificación formal se ve demasiado laboriosa, pero opina que ya se puede facilitar usando ordenadores y sustituirá a la tradicional (''the traditional social process is an anachronism to be swept away by formalization, just as empiricism replaced a similar “social process” used by the Greeks to decide scientific questions.'').
-la formalización en matemáticas y la verificación de sistemas informáticos:
+# '''Verificación formal'''. El uso de la matemática en los sistemas informáticos, la importacia crítica de dichos sistemas y sus fallos potencian el uso de métodos formales para verificarlos.
-(''formalization of pure mathematics and verification applications are not
+# '''Aspectos teóricos del razonamiento automático'''. Comenta la historia de la automatización del razonamiento (Leibniz, Frege). Presenta la lógica de primer orden (sintaxis, semántica, deducción, completitud, teorema de incompletitud, semidecisibilidad).
-separate activities, one undertaken for fun and the other for profit, but are
+# '''Aspectos prácticos del razonamiento automático'''. Comenta el cálculo simbólico de la lógica mediante lenguajes funcionales que da lugar a demostradores automáticos e interactivos. Comenta algunos de los éxitos de los demostradores: sistemas de decisión (SAT, aritmética de Presburger, SMT (satisfacibilidad módulo teorías), resolución y paramodulación, solución de la conjetura de Robbins, asistentes de prueba (SAM, Automath, LCF, Mizar, Nqthm) y estilos procedural (HOL) y declarativo (Mizar, Isar).
 # '''Conclusiones y prospectivas'''
-#* El uso de las demostraciones formales en matemáticas es una continuación
+#* El uso de las demostraciones formales en matemáticas es una continuación natural del aumento del rigor.
 #* La formalización es un tranbajo pesado.
 #* El uso de asistentes de demostración puede aligerarlo y hacerlo divertido.
-#* Se progresará mediante la acumulación de bibliotecas de matemáticas
+#* Se progresará mediante la acumulación de bibliotecas de matemáticas formalizadas, la integración en los asistentes de procedimientos de decisión y la mejora de los lenguajes usados para expresar las demostraciones.
-Este artículo sirve como referencia para los cursos
+Este artículo sirve como lectura para los cursos [http://www.cs.us.es/~jalonso/cursos/li Lógica informática] y [http://www.cs.us.es/~jalonso/cursos/d-ra Razonamiento automático]-
 [[User:Jalonso|José A. Alonso]] 10:54, 16 December 2008 (CET)
 [[Category:Lecturas]]

@@ Línea 1: / Línea 1: @@
-J. Harrison (2008) [http://www.ams.org/notices/200811/tx081101395p.pdf ''Formal
+J. Harrison (2008) [http://www.ams.org/notices/200811/tx081101395p.pdf ''Formal Proof: Theory and Practice'']. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
 ----
-Este trabajo es el tercer artículo del [http://www.ams.org/notices/200811/
+Este trabajo es el tercer artículo del [http://www.ams.org/notices/200811/ número de Diciembre de 2008 de las ''Notices of the AMS''] dedicado a las demostraciones formales.
 El resumen del artículo es el siguiente:
-# '''Introducción'''. En esta sección comenta los conceptos de demostración
+# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de
 la certidumbre) y aplicaciones (revisión de artículos matemáticos y
 verificación de sistemas informáticos); los avances en asistentes de prueba

@@ Línea 1: / Línea 1: @@
-J. Harrison (2008) [http://www.ams.org/notices/200811/tx081101395p.pdf ''Formal Proof: Theory and Practice'']. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
+J. Harrison (2008) [http://www.ams.org/notices/200811/tx081101395p.pdf ''Formal
 ----
-Este trabajo es el tercer artículo del [http://www.ams.org/notices/200811/ número de Diciembre de 2008 de las ''Notices of the AMS''] dedicado a las demostraciones formales.
+Este trabajo es el tercer artículo del [http://www.ams.org/notices/200811/
 El resumen del artículo es el siguiente:
-# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos: (''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396)).
+# '''Introducción'''. En esta sección comenta los conceptos de demostración
-# '''Lógica formal'''. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad).
+formal y asistentes de demostración; las razones de crear demostraciones
-# '''Los fundamentos de la matemáticas'''. Presenta una historia de los fundamentos de la matemáticas: su inicio en los ''Elementos'' de Euclides, los problemas de los axiomas, la corriente logicista de Frege, la teorái de conjunto de Cantor, la paradoja de Russell y las soluciones mediante tipos o axiomas (de Zermelo-Fraenkel).  Termina comentando la relaciones entre tipos y teoría de conjunto, donde se decanta por los tipos (''Type-based approaches look immediately appealing, because mathematicians generally do make type distinctions: between points and lines, or between numbers and sets of numbers, etc.'' (p. 1398)).
+formales (satisfación intelectual, fundamentación de la matemática y mejora de
-# '''¿Formalización o proceso social?'''. Comenta que en la historia anterior hay distintas motivaciones: fundamentar la matemática (Russell, Frege, Hilbert, Brouwer) y mejorar su enseñanza (Peano). Respecto a la acualidad comenta la extensión del uso del lenguaje conjuntista en matemática, pero no el de la lógica (''as far as the mathematical community is concerned George Boole has lived in vain'' (Dijkstra)). La certificación de la matemática se hace mediante revisión entre pares y no formalmente. Este proceso de revisión presenta fallos: teoremas grandes (p.e. teorema de los cuatro colores y la conjetura de Kepler). La certificación formal se ve demasiado laboriosa, pero opina que ya se puede facilitar usando ordenadores y sustituirá a la tradicional (''the traditional social process is an anachronism to be swept away by formalization, just as empiricism replaced a similar “social process” used by the Greeks to decide scientific questions.'').
+la certidumbre) y aplicaciones (revisión de artículos matemáticos y
-# '''Verificación formal'''. El uso de la matemática en los sistemas informáticos, la importacia crítica de dichos sistemas y sus fallos potencian el uso de métodos formales para verificarlos.
+verificación de sistemas informáticos); los avances en asistentes de prueba
-# '''Aspectos teóricos del razonamiento automático'''. Comenta la historia de la automatización del razonamiento (Leibniz, Frege). Presenta la lógica de primer orden (sintaxis, semántica, deducción, completitud, teorema de incompletitud, semidecisibilidad).
+(más fácilidad de uso, más potencia y más retos superados) y, la relación entre
-# '''Aspectos prácticos del razonamiento automático'''. Comenta el cálculo simbólico de la lógica mediante lenguajes funcionales que da lugar a demostradores automáticos e interactivos. Comenta algunos de los éxitos de los demostradores: sistemas de decisión (SAT, aritmética de Presburger, SMT (satisfacibilidad módulo teorías), resolución y paramodulación, solución de la conjetura de Robbins, asistentes de prueba (SAM, Automath, LCF, Mizar, Nqthm) y estilos procedural (HOL) y declarativo (Mizar, Isar).
+la formalización en matemáticas y la verificación de sistemas informáticos:
 # '''Conclusiones y prospectivas'''
-#* El uso de las demostraciones formales en matemáticas es una continuación natural del aumento del rigor.
+#* El uso de las demostraciones formales en matemáticas es una continuación
 #* La formalización es un tranbajo pesado.
 #* El uso de asistentes de demostración puede aligerarlo y hacerlo divertido.
-#* Se progresará mediante la acumulación de bibliotecas de matemáticas formalizadas, la integración en los asistentes de procedimientos de decisión y la mejora de los lenguajes usados para expresar las demostraciones.
+#* Se progresará mediante la acumulación de bibliotecas de matemáticas
 [[User:Jalonso|José A. Alonso]] 10:54, 16 December 2008 (CET)
 [[Category:Lecturas]]

@@ Línea 4: / Línea 4: @@
 El resumen del artículo es el siguiente:
-# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos:
+# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos: (''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396)).
 # '''Lógica formal'''. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad).
-# '''Los fundamentos de la matemáticas'''. Presenta una historia de los fundamentos de la matemáticas: su inicio en los ''Elementos'' de Euclides, los problemas de los axiomas, la corriente logicista de Frege, la teorái de conjunto de Cantor, la paradoja de Russell y las soluciones mediante tipos o axiomas (de Zermelo-Fraenkel).  Termina comentando la relaciones entre tipos y teoría de conjunto, donde se decanta por los tipos:
+# '''Los fundamentos de la matemáticas'''. Presenta una historia de los fundamentos de la matemáticas: su inicio en los ''Elementos'' de Euclides, los problemas de los axiomas, la corriente logicista de Frege, la teorái de conjunto de Cantor, la paradoja de Russell y las soluciones mediante tipos o axiomas (de Zermelo-Fraenkel).  Termina comentando la relaciones entre tipos y teoría de conjunto, donde se decanta por los tipos (''Type-based approaches look immediately appealing, because mathematicians generally do make type distinctions: between points and lines, or between numbers and sets of numbers, etc.'' (p. 1398)).
 # '''¿Formalización o proceso social?'''. Comenta que en la historia anterior hay distintas motivaciones: fundamentar la matemática (Russell, Frege, Hilbert, Brouwer) y mejorar su enseñanza (Peano). Respecto a la acualidad comenta la extensión del uso del lenguaje conjuntista en matemática, pero no el de la lógica (''as far as the mathematical community is concerned George Boole has lived in vain'' (Dijkstra)). La certificación de la matemática se hace mediante revisión entre pares y no formalmente. Este proceso de revisión presenta fallos: teoremas grandes (p.e. teorema de los cuatro colores y la conjetura de Kepler). La certificación formal se ve demasiado laboriosa, pero opina que ya se puede facilitar usando ordenadores y sustituirá a la tradicional (''the traditional social process is an anachronism to be swept away by formalization, just as empiricism replaced a similar “social process” used by the Greeks to decide scientific questions.'').
 # '''Verificación formal'''. El uso de la matemática en los sistemas informáticos, la importacia crítica de dichos sistemas y sus fallos potencian el uso de métodos formales para verificarlos.

← Revisión anterior		Revisión del 09:21 16 dic 2008
Línea 6:		Línea 6:
	# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos:		# '''Introducción'''. En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos:
	#: ''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396).		#: ''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396).
		+	# '''Lógica formal'''. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad).
		+	# '''Los fundamentos de la matemáticas'''. Presenta una historia de los fundamentos de la matemáticas: su inicio en los ''Elementos'' de Euclides, los problemas de los axiomas, la corriente logicista de Frege, la teorái de conjunto de Cantor, la paradoja de Russell y las soluciones mediante tipos o axiomas (de Zermelo-Fraenkel). Termina comentando la relaciones entre tipos y teoría de conjunto, donde se decanta por los tipos:
		+	#: ''Type-based approaches look immediately appealing, because mathematicians generally do make type distinctions: between points and lines, or between numbers and sets of numbers, etc.'' (p. 1398).

← Revisión anterior		Revisión del 09:10 16 dic 2008
Línea 1:		Línea 1:
−	J. Harrison (2008) ''[[Formal Proof: Theory and Practice]]''	+	J. Harrison (2008) [http://www.ams.org/notices/200811/tx081101395p.pdf ''Formal Proof: Theory and Practice'']. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
		+	----
		+	Este trabajo es el tercer artículo del [http://www.ams.org/notices/200811/ número de Diciembre de 2008 de las ''Notices of the AMS''] dedicado a las demostraciones formales.
		+
		+	El resumen del artículo es el siguiente:
		+	# Introducción.
		+	#: En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos:
		+	#:: ''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396).