[metis-users] Proof annotations

[Joe Leslie-Hurd]

Hi Alejandro,

I'm afraid there is no more documentation that what you have already
found, with the possible exception of some documents on

http://www.gilith.com/research/metis/

some of which I'll link to below.

I think you have correctly identified all possible inferences that
Metis makes: the general pattern of inferences in a FOF TSTP proof
goes like this:

1. Printing clauses given by the TPTP problem (e.g., axiom or conjecture).

2. Some preliminary inferences to turn the problem from tautological
goal formulas to unsatisfiable sets of formulas. In the Metis source
this inference field was just a string which wasn't helpful for
understanding its possible values, so I just released a new version
where it is the following datatype:

datatype inference =
    StripInference
  | NegateInference

3. Next come normalizing inferences to transform the problem from
first order formulas into clausal form: these are values from the
following datatype:

datatype inference =
    Axiom of Formula.formula
  | Definition of string * Formula.formula
  | Simplify of thm * thm list
  | Conjunct of thm
  | Specialize of thm
  | Skolemize of thm
  | Clausify of thm

Axiom here just refers to an input to the normalizing procedure.

4. Finally there are the CNF inferences to derive a contradiction,
which are values of the following datatype:

datatype inference =
    Axiom of LiteralSet.set
  | Assume of Atom.atom
  | Subst of Subst.subst * Thm.thm
  | Resolve of Atom.atom * Thm.thm * Thm.thm
  | Refl of Term.term
  | Equality of Literal.literal * Term.path * Term.term

Again Axiom just means an input to the refutation procedure. These
inferences are described in some detail at

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

Note that inferences that do not take an input clause (e.g., equality)
can't appear in the proof with "inference", but rather "introduced",
so it is their arguments that comprise the unknown structures that you
encountered.

I hope that helps with your project, please let me know if you have
any more questions about the Metis proof format.

Cheers,

Joe

On Sun, Mar 1, 2015 at 1:31 PM, Alejandro Gomez <agomezl at eafit.edu.co> wrote:
> 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/
>
> _______________________________________________
> metis-users mailing list
> metis-users at gilith.com
> http://www.gilith.com/metis/mailing-list