Flussdiagramm
Dual-contexto lógica modal como adjunto izquierdo del estilo Fitch lógica modal
Inhalt des Flussdiagramms
la lógica modal intuicionista
Curry-Howard correspondencia
Estilo Hilbert
¿Que es?
Por "intuicionismo lógico" se entiende una cierta tendencia filosófica que'l si bien reivindica una forma de intuición intelectual como método de conocimiento.
Se Divide en tres partes
Estilo Kripke
Se basa en :
sistemas de deducción naturales
Son una clase de sistemas deductivos en la lógica.
Una parte de la importancia de los sistemas de deducción naturales es una relación con
los lenguajes de programación.
¿Que es?
¿Que son?
Se utilizan en:
Una estructura de Kripke es una variación del sistema de transicion, para representar el comportamiento de un sistema.
¿Que es?
la semántica de estilo Kripke y sistemas de estilo Hilbert
con axiomas son aceptadas comúnmente para las variaciones de la lógica modal
intuicionista
Se relacionan en
Los estudios sobre la logica modal
Gentzen de estilo, De doble contexto
Estilo de Fitch
corrientes principales
A pesar de una
larga historia, significado computacional de estilo Fitch deducción naturales de
sistemasción, no está bien establecida. Dado que tanto el doble contexto y de estilo
Fitch tienen múltiples contextos y juicios similares.
Cálculo de estilo AGentzen era primera propuesto por Bellin, y fue más tarde
re definido por uno de los autores
se dedicó a
la lógica lineal intuitionistic con la modalidad exponencial.
Después de varios estudios sobre S4, un cálculo de doble contexto para intuicionista K
Adjuncion
Debido a la asignación de los
niveles, se puede demostrar que la unión de los cálculos de nivel 2 se corresponde exactamente
con el cálculo adjunto.
Resultado
Nuestros resultados inducen una
descomposición de una modalidad S4 contextual.
Intuicionista lógica modal
se introducen tres tipos de sistemas deductivos para la lógica
modal intuicionista.
Fitch-estilo
Gentzen de estilo
Cálculo con Adjunción
la deducción natural de la lógica proposicional intuicionista significa
simplemente el tecleado λ- cálculo.
En esta sección, se reconstruye una variante del aditivo cálculo adjunto [ 4] a través
de sistemas al estilo de Fitch y de doble contexto.
Este estudio se basa en la formulación [17] de IK por uno
de los autores. En Fitch-estilo, un juicio tiene una forma Δ l M: UN, dónde l es un nivel que
oscila sobre los números naturales.
En este documento, usamos el símbolo Δ como una secuencia de contextos, mientras que el
símbolo Γ denota un contexto. Para evitar confusiones, se utiliza un punto y coma como
separadores entre los contextos en lugar de comas
Ejemplo:
Ejemplo
Dual-contexto
Los estudios sobre los sistemas de doble contexto fueron motivados por la lógica lineal
en los primeros días. Desde el! modalidad de lógica lineal es un tipo de modalidad S4
Fallos
Un fallo en el cálculo de doble contexto tiene dos tipos de contextos, una contexto
modal y una contexto normal
Autor # 1:
Yoshihiko Kakutani graduado de
Facultad de Ciencias, Universidad de Kyoto en 1999.
Recibió su Ph.D. del Instituto de Investigación de
Ciencias Matemáticas, Universidad de Kyoto en 2003.
Se convirtió en profesor asistente en el Departamento
de Ciencias de la Computación de la Universidad de
Tokio en 2004. Sus áreas de investigación en lenguajes
de programación, clude lógica matemática y la teoría de categorías.
Autor # 2:
Yuito Murase graduado de la Facultad de Ciencias de
la Información, Universidad de Tokio en 2016. Recibió
su M.Sc. FromDepartment grado de Ciencias de la
Computación, Facultad de Ciencias de la Información y
Tecnología de la Universidad de Tokio en 2018. Sus
líneas de investigación actuales son la lógica modal y la
teoría de tipos.
Autor # 3
Yuichi Nishiwaki graduado de la Facultad de
Ciencias de la Información, Universidad de Tokio
en 2016. Recibió su
M.Sc. grado del Departamento de Ciencias de la
Computación, Facultad de Ciencias de la Información y
Tecnología de la Universidad de Tokio en 2018, y
actualmente se encuentra en un curso de doctorado. Ha
sido un Japón
Informationen
- Beschreibung
- Mapa Conceptual Jhonatan Reynaldo Serrano Garcia
- Erstellt von
- jhonatan serrano
- Aufrufe
- 5
- Bewertung