DOI10.1016/0168-0072(95)00005-2zbMath0836.03034OpenAlexW2067558609WikidataQ114684038 ScholiaQ114684038MaRDI QIDQ1902978
Jan von Plato
Publication date: 2 May 1996
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0168-0072(95)00005-2
A constructive real projective plane,
Formalizing generalized maps in Coq,
Current Status of the I2GATP Common Format,
Implementing Euclid's straightedge and compass constructions in type theory,
Two cryptomorphic formalizations of projective incidence geometry,
Constructive geometrical reasoning and diagrams,
The ILTP problem library for intuitionistic logic,
CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE,
Formal specification and proofs for the topology and classification of combinatorial surfaces,
Syntactic categories in the language of mathematics,
Brouwer and Euclid,
Using the prover ANDP to simplify orthogonality.,
The area method. A recapitulation,
Simplifying von Plato's axiomatization of constructive apartness geometry,
Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof,
A resolution theorem prover for intuitionistic logic,
Organization and development of a constructive axiomatization,
Constructivity in Geometry,
Axiomatizing geometric constructions,
In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs,
Real numbers and projective spaces: intuitionistic reasoning with undecidable basic relations,
Formalization of the Poincaré disc model of hyperbolic geometry,
Mechanical Theorem Proving in Tarski’s Geometry,
Constructibility and Geometry,
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge,
A ModalWalk Through Space,
A constructive theory of ordered affine geometry,
A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs,
Automating Theories in Intuitionistic Logic,
A common axiom set for classical and intuitionistic plane geometry,
A FORMAL SYSTEM FOR EUCLID’SELEMENTS,
Formalizing constructive projective geometry in Agda,
Formalizing complex plane geometry
