[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