activity
20212024
most citedMechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach

2 citations · 3 across the 5 of their papers we have counts for

collaborators
Showing 2021Show all

1 paper · 1 filter

cs.LO2021★ 1 cited

Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant

Nicolas Magaud

Recently, we developed an automated theorem prover for projective incidence geometry. This prover, based on a combinatorial approach using matroids, proceeds by saturation using th…