Create deductive proofs

The prover in OK Geometry provides, when successful, human-readable deductive proofs.

With OK Geometry you can create deductive proofs of geometric properties of dynamic constructions. The proving process employs a variant of the Geometric Deductive Database method developed by Chou, Gao and Zhang. While not every statement can be proved using this method, a successful outcome yields a human-readable, top-down deductive proof. Although the resulting proof may sometimes lack elegance, it can, with a little effort, be refined into a standard format suitable for educational purposes.

You can find more about advanced query here.