[metis-users] Hypothesis and axioms in Metis

[Joe Hurd]

Hi Andres,

I've just had a look at the sources, and I don't think Metis ever
generates a new formula with a "hypothesis" role in a proof (it would
use an "axiom" for this purpose), but it should preserve the role of a
"hypothesis" input formula that occurs in a problem.

I agree with you that I don't believe there is a practical difference
between the two roles.

Cheers,

Joe

2011/4/1 Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>:
> Dear Joe,
>
> From TPTP semantics, it seems there is no difference in use "axiom" or
> "hypothesis" to annotate a TPTP formula. Is there some difference
> from Metis's point of view?
>
> Best regards,
>
> --
> Andrés
>
> _______________________________________________
> metis-users mailing list
> metis-users at gilith.com
> http://www.gilith.com/metis/mailing-list
>