Notes from the logbook of a proof-checker's project

DOI10.1007/B12001MaRDI QIDQ5305641zbMATH OpenOpenAlexFDO

Authors Domenico Cantone, Pietro Ursino, Eugenio Omodeo, Jacob T. Schwartz

Publication date 23 March 2010

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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4009856
• Computational logic and set theory. Applying formalized logic to analysis. Foreword by Martin Davis
• scientific article; zbMATH DE number 1259143
• Implementing constructive real analysis (preliminary report)
• Constructing the real numbers in HOL

Cited in

(5)

• Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate
• Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates
• scientific article; zbMATH DE number 4009856 (Why is no real title available?)
• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions

Describes a project that uses

Uses Software

• IMPS
• OTTER

This page was built for publication: Notes from the logbook of a proof-checker's project

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