Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry
From MaRDI portal
Publication:3102739
DOI10.1007/978-3-642-25070-5_7zbMath1350.68240OpenAlexW1449190760MaRDI QIDQ3102739
Publication date: 25 November 2011
Published in: Automated Deduction in Geometry (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25070-5_7
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Cites Work
- Unnamed Item
- Unnamed Item
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Interrogating witnesses for geometric constraint solving
- A deductive database approach to automated geometry theorem proving and discovering
- Perspectives on Projective Geometry
- Cancellation Patterns in Automatic Geometric Theorem Proving
- INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
- Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
This page was built for publication: Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry
