# [PVS-Help] Need suggestion with Inequality

```Hello, I'm new to PVS and currently working on my final project. This
project will be an automatic essay grader for proof of mathematical
inequality.

Here some scratch of design of the system's architecture, written down
by steps that glance in mind :

1. Convert student's answer (the proof of ineq) into nodes in
PVS-understandable expression and batch this nodes into PVS.

2. Let PVS do the verification..

3. Marking time! Suppose there's a rubric (marking scheme) from teacher,
then this rubric will be applied to the result of verification process,
yielding student's mark of his proof.

4. Aside, I will write down some strategies that commonly used in
proving inequalities like Am-Gm or Cauchy-Schwartz, such that

{-1} x>0
{-2} y>0
-------------
{1} x*x*x + y*y*y + 1 >= 3*x*y

will be easily solved by
Rules? (am-gm) <-- I hope so

afraid of "reinventing the wheel" or -moreover- "I can't invent the
wheel, but peoples have invented it".

In step (1), student's answer will take form of LaTeX, and I think I
need some NLP skills to convert it equally into PVS expression. Is there
any better solution?

In step (3), the only thing that possible to do is parsing the .prf
file. However, I don't think that's probable. Any suggestion?

In step (4), I haven't found any such strategies (yet). Am I missing
something?

Any suggestion, references of paper, book, PVS library,  even your email