Línea 1:

+

J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/model.html ''Formalizing basic first order model theory'']. Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170. 

+

----

+

En este trabajo se presenta una formalización de la teoría de modelo de la lógica de primer orden, El libro de partida es el de Kreisel y Krivine ''Elements of mathematical logic: model theory''. El sistema en donde se realiza la formalización es en HOL-Light. La motivación del trabajo fue la de escribir un libro de texto de lógica matemática.

−

Category: Lecturas

+

En el trabajo se describe la formalización realizada:

+

* Definición de los conceptos sintácticos. 

+

* Definición de los conceptos semánticos.

+

* Demostración de metateoremas:

+

** Teorema de compacidad para la sublógica proposicional.

+

** Formas prenexas y de Skolem.

+

** Modelos canónicos.

+

A lo largo del trabajo se explica las razones para elegir la representación utilizada. Generalmente es par mantener la fidelidad al texto y ser la más intuitiva.

+

Este trabajo pude usarse para la formalización de la metalógica en Isar. Habría que considerar la evaluabilidad de los procedimientos y la conveniencia de usar Isabelle/ZF (para evitar los problemas con los tipos que se comenta en el trabajo).

+

[[User:Jalonso|José A. Alonso]] 10:20, 4 December 2008 (CET)

+

[[Category: Lecturas]]

Formalizing basic first order model theory - Historial de revisiones

Jalonso en 09:20 4 dic 2008

Jalonso: New page: Category: Lecturas

← Revisión anterior		Revisión del 09:20 4 dic 2008
Línea 1:		Línea 1:
		+	J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/model.html ''Formalizing basic first order model theory'']. Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170.
		+	----
		+	En este trabajo se presenta una formalización de la teoría de modelo de la lógica de primer orden, El libro de partida es el de Kreisel y Krivine ''Elements of mathematical logic: model theory''. El sistema en donde se realiza la formalización es en HOL-Light. La motivación del trabajo fue la de escribir un libro de texto de lógica matemática.

−	Category: Lecturas	+	En el trabajo se describe la formalización realizada:
		+	* Definición de los conceptos sintácticos.
		+	* Definición de los conceptos semánticos.
		+	* Demostración de metateoremas:
		+	** Teorema de compacidad para la sublógica proposicional.
		+	** Formas prenexas y de Skolem.
		+	** Modelos canónicos.
		+
		+	A lo largo del trabajo se explica las razones para elegir la representación utilizada. Generalmente es par mantener la fidelidad al texto y ser la más intuitiva.
		+
		+	Este trabajo pude usarse para la formalización de la metalógica en Isar. Habría que considerar la evaluabilidad de los procedimientos y la conveniencia de usar Isabelle/ZF (para evitar los problemas con los tipos que se comenta en el trabajo).
		+
		+	[[User:Jalonso\|José A. Alonso]] 10:20, 4 December 2008 (CET)
		+
		+
		+
		+
		+	[[Category: Lecturas]]