Diferencia entre revisiones de «Formalizing basic first order model theory»
(New page: Category: Lecturas) |
|||
| 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]] | ||
Revisión actual del 11:20 4 dic 2008
J. Harrison. 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.
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).
José A. Alonso 10:20, 4 December 2008 (CET)
