[metis-users] Metis

[Geoff Sutcliffe]

Hi Joe, all,

> 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.

Information about the TPTP proof format is available at ...
    http://www.cs.miami.edu/~tptp/TPTP/QuickGuide/Derivations.html
    http://www.cs.miami.edu/~tptp/TPTP/QuickGuide/FiniteInterpretations.html

... and written up in ...

@InProceedings{SS+06,
    Author       = "Sutcliffe, G. and Schulz, S. and Claessen, K. and
                    Van Gelder, A.",
    Year         = "2006",
    Title        = "{Using the TPTP Language for Writing Derivations and
                    Finite Interpretations}",
    Editor       = "Furbach, U. and Shankar, N.",
    BookTitle    = "{Proceedings of the 3rd International Joint Conference on
                    Automated Reasoning}",
    Place        = "Seattle, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "4130",
    Pages        = "67-81",
    Comment      = "TPTPCite"
}

Cheers,

Geoff

> 
> 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
> 
> _______________________________________________
> metis-users mailing list
> metis-users at gilith.com
> http://www.gilith.com/metis/mailing-list
Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Professor and Chairman                    Email : geoff at cs.miami.edu
Department of Computer Science            Phone : +1 305 2842158/2842268
University of Miami                       FAX   : +1 305 2842264
----- "My cat" is not a float. Every string should learn to swim. ------