We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a β-valued model for some non trivial truth values algebra B. A theory that has a β-valued model for all truth values algebras B is said to be super-consistent. We prove that super-consistency is a model-theoretic sufficient condition for strong normalization. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Dowek, G. (2007). Truth values algebras and proof normalization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4502 LNCS, pp. 110–124). Springer Verlag. https://doi.org/10.1007/978-3-540-74464-1_8
Mendeley helps you to discover research relevant for your work.