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

DOI10.1007/B12001zbMATH Open1274.68407OpenAlexW2483649756MaRDI QIDQ5305641FDOQ5305641

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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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
• Title not available (Why is that?)
• 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

Uses Software

• OTTER
• IMPS

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)