Algorithms for ordinal arithmetic.

DOI10.1007/B11829MaRDI QIDQ5900722zbMATH OpenOpenAlexFDO

Authors Panagiotis Manolios, Daron Vroon

Publication date 20 April 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b11829

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ordinal and cardinal numbers (03E10)

Recommendations

• Ordinal arithmetic: Algorithms and mechanization
• Formal Methods in Computer-Aided Design
• An ordinal calculus for proving termination in term rewriting
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• An ordinal measure based procedure for termination of functions

Cited in

(12)

• Integrating external deduction tools with ACL2
• A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
• A mechanizable first-order theory of ordinals
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Specification and verification of concurrent programs through refinements
• Trees, ordinals and termination
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• Formal Methods in Computer-Aided Design
• An ordinal measure based procedure for termination of functions
• Test sets for equality of terms in the additive structure of ordinals augmented with right multiplication by
• Ordinal arithmetic: Algorithms and mechanization
• A mechanical analysis of program verification strategies

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Algorithms for ordinal arithmetic.

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