[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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

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

I need suggestion about this system's design. Since I'm new to PVS, I'm
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

Any suggestion, references of paper, book, PVS library,  even your email
addresses will help. Thx b4.

Dimas Danurwenda
Institut Teknologi Bandung
Bandung, Indonesia