Formalizing the trading theorem for the classification of surfaces

DOI10.1007/3-540-45685-6_11MaRDI QIDQ4484338zbMATH OpenFDO

Authors Christophe Dehlinger, Jean-François Dufourd

Publication date 12 June 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100148.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to manifolds and cell complexes (57-04) Computer-aided design (modeling of curves and surfaces) (65D17)

Recommendations

• Formalizing the trading theorem in Coq
• Formalizing generalized maps in Coq
• Formal specification and proofs for the topology and classification of combinatorial surfaces
• Discrete Jordan curve theorem: a proof formalized in Coq with hypermaps
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps

Cited in

(3)

• Formalizing generalized maps in Coq
• Formalizing the trading theorem in Coq
• Formal specification and proofs for the topology and classification of combinatorial surfaces

Describes a project that uses

Uses Software

• ALF
• Isar
• Coq

This page was built for publication: Formalizing the trading theorem for the classification of surfaces

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