A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry.

Tuan-Minh Pham Yves Bertot Julien Narboux

Published in: ICCSA (4) (2011)

Keyphrases

automated theorem proving
theorem prover
theorem proving
three dimensional
euclidean geometry
inference rules
first order logic
answer set programming
virtual reality
user interaction
knowledge base
data model
user friendly
realistic rendering
data mining
computer graphics