[PVS-Help] how to write good axioms for grind?

["Brian J. Cardiff" <bcardiff@xxxxxxxxx>]

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
BEGIN
  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
END smallex

In the proof of MyTheorem, using (grind)  (or whatever somebody
suggest) I will like to get one sequent:

|---
parent(n1) = n3


Thank you
-- 
Brian J. Cardiff
bcardiff(?)gmail.com
.