[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] how to write good axioms for grind?
I'm trying to use pvs in batch mode for automatic proving some theorems.
At this moment I'm focusing in how grind is able (or not) to use the
information in axioms
For example, I realised that
AXIOM n1 /= n2
should be written as
AXIOM (n1 = n2) = FALSE
so grind is able to use this information during its execution.
But I couldn't find how to write good axioms that starts with
universal quantifiers. Is there any way?
Here is a very small example of what i am expecting to get.
smallex : THEORY
Node : TYPE+
n1, n2, n3 : Node
parent : [Node -> Node]
ax1 : AXIOM (n1 = n2) = FALSE
ax2 : AXIOM (n3 = n2) = FALSE
ax3 : AXIOM FORALL (o: Node): parent(o) /= n2
MyTheorem : THEOREM parent(n1) = n3 AND parent(n1) /= n2
In the proof of MyTheorem, using (grind) (or whatever somebody
suggest) I will like to get one sequent:
parent(n1) = n3
Brian J. Cardiff