The higher-order-logic Formath

MaRDI QIDQ935562zbMATH OpenFDO

Authors Pieter Audenaert

Publication date 11 August 2008

Published in Bulletin of the Belgian Mathematical Society - Simon Stevin (Search for Journal in Brave)

Full work available at URL https://projecteuclid.org/euclid.bbms/1210254829

zbMATH Keywords

automated theorem provinghigher-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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.

Recommendations

• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• The HOL-Omega Logic
• scientific article; zbMATH DE number 1405633
• scientific article; zbMATH DE number 1617310
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic

Cited in

(4)

• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• The HOL-Omega Logic
• scientific article; zbMATH DE number 1405633 (Why is no real title available?)

Describes a project that uses

Uses Software

• PVS
• ACL2
• HOL
• HOL Light

This page was built for publication: The higher-order-logic Formath

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q935562)