[metis-users] Proof annotations

[Alejandro Gomez]

Hi all,

I'm currently trying to parse Metis proofs and have
had some problems particularly with the <annotations> field.
as far as I know (from the TSTP site, some metis proofs,
and the metis source ) the <annotations> part of a formula in metis
proofs is more or less like:

<annotations> := ,inference(<rule>, [<info>], [<parents>])
                        | ,introduced( <??>)

<rule> := canonicalize
             | simplify
             | conjunct
             | specialize
             | skolemize
             | clausify
             | assume
             | subst
             | resolve
             | refl
             | equality
             | negate
             | strip

where

- <info> is a list of useful inference information (as described in
the TSTP site).
- <parents> is a list of references to parents formulae.
- <??> is just an unknown structure.


Is there any reference of all the possible <rule> symbols or the whole
<annotations> symbol? my long term goal is to construct a (sort of) DAG with
formulas as nodes and rules as edges, thus a complete list of all possible
rules is required.

Any help or advise is greatly appreciated.

Thanks.

-- 
Alejandro Gomez-Londoño
Computer Science, Universidad EAFIT
http://agomezl.github.io/