Pages that link to "Item:Q5453489"

The following pages link to Mechanical Theorem Proving in Tarski’s Geometry (Q5453489):

Displaying 24 items.

• Towards a certified version of the encyclopedia of triangle centers (Q294378) (← links)
• The area method. A recapitulation (Q437042) (← links)
• A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975) (← links)
• Tarski geometry axioms. II (Q502683) (← links)
• Tarski geometry axioms (Q502700) (← links)
• Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method (Q616846) (← links)
• Formalization of the arithmetization of Euclidean plane geometry and applications (Q1640646) (← links)
• Towards an intelligent and dynamic geometry book (Q1701659) (← links)
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (Q1725841) (← links)
• Tarski geometry axioms. III (Q1795563) (← links)
• Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
• Formalizing complex plane geometry (Q2354913) (← links)
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
• A synthetic proof of Pappus' theorem in Tarski's geometry (Q2362204) (← links)
• Tarski geometry axioms. IV: Right angle (Q2416858) (← links)
• A graphical user interface for formal proofs in geometry (Q2462636) (← links)
• From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
• Implementing Euclid's straightedge and compass constructions in type theory (Q2631963) (← links)
• Two cryptomorphic formalizations of projective incidence geometry (Q2631964) (← links)
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs (Q3102745) (← links)
• (Q3700870) (← links)
• (Q4665735) (← links)
• Tarski geometry axioms. V: Half-planes and planes (Q6557128) (← links)