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

Re: [PVS-Help] Need suggestion with Inequality



Hi Dimas,

I'm not sure to understand your project. However, you may want to look
at ProofLite (http://research.nianet.org/~munoz/ProofLite), a tool for
non-interactive proof checking in PVS (the site is currently down due to
a disk failure, but someone is working on that).

Hope that it helps,

Cesar



dimas wrote:
> 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
> 
> 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
> something?
> 
> Any suggestion, references of paper, book, PVS library,  even your email
> addresses will help. Thx b4.
> 
> --
> Dimas Danurwenda
> Informatics
> Institut Teknologi Bandung
> Bandung, Indonesia
> 
> 

-- 
Cesar A. Munoz, Research Fellow               mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4