The higher-order-logic Formath
type: Item
instance of: scholarly article
title: The higher-order-logic Formath
zbMATH Open document ID: 1168.03007
author: Pieter Audenaert
published in: Bulletin of the Belgian Mathematical Society - Simon Stevin
publication date: 2008-08-11T00:00:00Z
full work available at URL: https://projecteuclid.org/euclid.bbms/1210254829
review text: 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.
reviewed by: Albert Hoogewijs
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5309617
zbMATH Keywords: higher-order logic
zbMATH Keywords: automated theorem proving
describes a project that uses: PVS
describes a project that uses: ACL2
describes a project that uses: HOL
describes a project that uses: HOL Light
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 5309617