A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry.

David Braun Nicolas Magaud Pascal Schreck

Published in: J. Autom. Reason. (2024)

Keyphrases

theorem prover
theorem proving
geometry theorem proving
automated theorem proving
proof search
first order logic
three dimensional
inference rules
projective geometry
greedy algorithm
data driven
knowledge representation
semi automatic
natural deduction
fully automatic
knowledge based systems
case study