The higher-order-logic Formath (Q935562)
From MaRDI portal
![]() | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: The higher-order-logic Formath |
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The higher-order-logic Formath |
scientific article |
Statements
The higher-order-logic Formath (English)
0 references
11 August 2008
0 references
This paper describes in detail the logic Formath, inspired by two HOL derivatives: HOL-4 and HOL-Light. Formath is designed from the point of view of a mathematician. This results in the introduction of a syntactical distinction between bound and free variables, the use of ``de Bruijn'' indices and extending the consequences to more than one consequence. The author proves the soundness of his system and ends with an interesting comparison of Formath and the classical HOL-4 and HOL-Light variants. The logical strength of Formath seems to be the same as the more established versions, but the axiomatization is rather elegant and has several novel features (for this context), e.g., multiple-conclusion sequents and a syntactic distinction between free and bound variables using an approach similar to ``de Bruijn'' indices.
0 references
higher-order logic
0 references
automated theorem proving
0 references