The Higher-Order-Logic Formath
Audenaert, Pieter
Bull. Belg. Math. Soc. Simon Stevin, Tome 15 (2008) no. 1, p. 335-367 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
We introduce a new formalization of Higher-Order-Logic (abbreviated Hol), which we baptized Formath, an acronym for FORMAl MATHematics. We discuss the syntax, semantics, deduction-rules, axioms and principles of extension, after which we prove soundness and consistency. The semantics are comparable to other systems for Hol, such as Hol-4 and Hol-Light, but other parts differ from the traditional way of working, for example the deduction-rules and axioms. We discuss these differences in large extent. We also talk about porting theorems to the Formath library, provide examples and discuss the applications.
Publié le : 2008-05-15
Classification:  
@article{1210254829,
     author = {Audenaert, Pieter},
     title = {The Higher-Order-Logic Formath},
     journal = {Bull. Belg. Math. Soc. Simon Stevin},
     volume = {15},
     number = {1},
     year = {2008},
     pages = { 335-367},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1210254829}
}

Audenaert, Pieter. The Higher-Order-Logic Formath. Bull. Belg. Math. Soc. Simon Stevin, Tome 15 (2008) no. 1, pp.  335-367. http://gdmltest.u-ga.fr/item/1210254829/