Documentation Gap

[RSchulz]

Hi,

I am writing an LADR format parser and have been using the input files in the downloadable documentation bundle http://www.cs.unm.edu/~mccune/prover9/manual/prover9-manual-2009-02A.tar.gz as test cases.

In doing so, I came across this construct:

Input: Select all

list(distinct)
% ...

The only mention of this I could find anywhere is at http://forums.prover9.org/viewtopic.php?f=9&t=9&p=19 (look for the October 21, 2008 entry).

This construct is not documented anywhere that I can find by searching the PDF file "finalbook.pdf" contained in the documentation bundle.


Randall Schulz

[mkinyon]

Yes, some updating is certainly need. For now, see the zebra2 example here:

http://www.cs.unm.edu/~mccune/prover9/manual/2009-02A/m4-arithmetic.html

[RSchulz]

Yes, some updating is certainly need. For now, see the zebra2 example here:

http://www.cs.unm.edu/~mccune/prover9/manual/2009-02A/m4-arithmetic.html

Uh, that's what sent me looking for a description of what said list is for.


Randall Schulz

[mkinyon]

Oh, well, it's basically just a shortcut. For instance,

Code: Select all

list(distinct).
   [England,Spain,Ukraine,Japan,Norway].
end_of_list.


is just a shorthand for

Code: Select all

formulas(assumptions).
England != Spain. England != Ukraine. England != Japan. England != Norway.
Spain != Ukraine. Spain != Japan. Spain != Norway.
Ukraine != Japan. Ukraine != Norway.
Japan != Norway.
end_of_list.

[RSchulz]

I do understand what it's for / what it means. I just wanted to point out that it should be documented.


RRS