[metis-users] Metis

[Joe Leslie-Hurd]

Hi Jonathan,

[cc'ing the metis-users mailing list]

Unfortunately there isn't really a comprehensive document describing
the output of Metis. The website lists two example outputs, one for a
CNF problem and one for a FOF problem:

http://www.gilith.com/software/metis/example-cnf-proof.txt
http://www.gilith.com/software/metis/example-fof-proof.txt

The inference rules used by the cnf clauses in the output are
described in this document:

http://www.gilith.com/software/metis/logical-kernel.txt

I'd be happy to answer any further questions you have about the output
on the mailing list.

Cheers,

Joe


On Thu, Jun 9, 2016 at 3:28 PM, Jonathan Prieto <prieto.jona at gmail.com> wrote:
> Hi Joe,
>
> I've started using Metis, and I was wondering if metis has some document explain his usage and information about the output it generates.
> I read some notes, and pages following the links in the metal's website, but it seems the doc is missing. I will be grateful if you have some hints,
> or some documentation to dig into the outputs,  I am working in proof reconstruction.
> I am aware that metis outputs in TSTP format, whatever you can help me, thank you.
>
>
> Regards,
>
> Jonathan Prieto
> EAFIT University