Automation for Geometry in Isabelle/HOL.

Laura I. Meikle Jacques D. Fleuriot

Published in: PAAR@IJCAR (2010)

Keyphrases

theorem prover
natural deduction
inference rules
theorem proving
three dimensional
higher order logic
first order logic
cut elimination
human operators
sequent calculus
projective geometry
geometric information
geometric structure
image processing
formal methods
linear logic
data mining
machine learning