Utilize este identificador para referenciar este registo:
http://hdl.handle.net/10773/27104
Título: | Completeness in Equational Hybrid Propositional Type Theory |
Autor: | Manzano, Maria Martins, Manuel A. Huertas, Antonia |
Palavras-chave: | Propositional type theory Hybrid logic Equational logic Completeness |
Data: | Dez-2019 |
Editora: | Springer Verlag |
Resumo: | Equational Hybrid Propositional Type Theory (EHPTT) is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra (a nonempty set with functions) and a Kripke frame. The main result in this paper is the proof of completeness of a calculus specifically defined for this logic. The completeness proof is based on the three proofs Henkin published last century: (i) Completeness in type theory (ii) The completeness of the first-order functional calculus and (iii) Completeness in propositional type theory. More precisely, from (i) and (ii) we take the idea of building the model described by the maximal consistent set; in our case the maximal consistent set has to be named, ♦- saturated and extensionally algebraic-saturated due to the hybrid and equational nature of EHPTT. From (iii), we use the result that any element in the hierarchy has a name. The challenge was to deal with all the heterogeneous components in an integrated system. |
Peer review: | yes |
URI: | http://hdl.handle.net/10773/27104 |
DOI: | 10.1007/s11225-018-9833-5 |
ISSN: | 0039-3215 |
Aparece nas coleções: | CIDMA - Artigos AGG - Artigos DMat - Artigos |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Ria_version2019-02.pdf | 532.63 kB | Adobe PDF | Ver/Abrir |
Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.