[metis-users] About Metis' rules

[Joe Leslie-Hurd]

Hi Jonathan,

[cc'ing metis-users for posterity]

Your reverse engineering of the inference rules looks essentially
correct to me. Here are a few notes that occurred to me when reading
your summary:

For FOF problems the inputs are FOF formulas, which Metis converts to
CNF clauses and then looks for a refutation. The inferences on CNF
clauses are much more precise, since many systems replay those proofs
in another system. Here is a description of the CNF inferences,
including both "resolve" and "assume":

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

As far as I know no system attempts to replay the FOF to CNF
conversion in Metis, so the inferences are not so precise (as you
know, because you discovered a bug in one of them). But the basic
steps are:

1) Strip the conjecture into subgoals, so A & B is stripped into two
subgoals: A and (A => B). These subgoals are treated as completely
different problems to be proved independently.

2) Negate each subgoal, add it to the set of FOF axioms in the
problem, then convert this set of FOF formulas to CNF clauses.

3) The inference rules that are responsible for converting FOF
formulas to CNF clauses are given names according to the following
code in Tptp.sml:

  fun nameNormalize inf =
      case inf of
        Normalize.Axiom _ => "canonicalize"
      | Normalize.Definition _ => "canonicalize"
      | Normalize.Simplify _ => "simplify"
      | Normalize.Conjunct _ => "conjunct"
      | Normalize.Specialize _ => "specialize"
      | Normalize.Skolemize _ => "skolemize"
      | Normalize.Clausify _ => "clausify";

  fun nameProof inf =
      case inf of
        Proof.Axiom _ => "canonicalize"
      | Proof.Assume _ => "assume"
      | Proof.Subst _ => "subst"
      | Proof.Resolve _ => "resolve"
      | Proof.Refl _ => "refl"
      | Proof.Equality _ => "equality";

You already covered the relatively precisely-defined "conjunct" and
relatively loosely-defined "simplify" in your email, and I don't have
much to add.

As can be seen, the name "canonicalize" is rather overloaded, being
used for the identity function (Normalize.Axiom), definitional CNF
(Normalize.Definition), and the final conversion from a FOF formula in
clausal form to a CNF clause (Proof.Axiom). Actually, it's not really
the identity function, because some simplification such as eliminating
True and False from formulas happens throughout the conversion
process.

Hope that helps.

Cheers,

Joe

On Tue, Oct 10, 2017 at 9:53 PM, Jonathan Prieto-Cubides
<jprieto9 at eafit.edu.co> wrote:
> Dear Joe,
>
> I've been working for a time long this year with Metis since I'm trying to
> justify
> its proofs. I'm just working with the propositional fragment without
> equality.
>
> I would like to kindly ask you about the Metis' inference rules.
>
> Based on the scope of my problems (CPL) but also from the list of 6
> inferences
> rules described on the Metis' documentation, only 3 rules apply: axiom,
> assume
> and resolve.
>
> Comparing these rules with the TSTP derivations and after looking at the
> Metis' source code, I might say:
>
> assume inference appears when a TSTP derivation uses negate rule to
> introduce
> the negation of some subgoal. But what inference rule stands for strip rule.
>
> axiom inference justifies the rules:
>
> canonicalize performs the next (following the next order?):
>
> It translates a formula to a normalized* version. A version derived from
> a negate normal form with only True, False, And, Or, XOR connectives.
>
> It removes constants: True and False by a recursion over the structure
> of the formula. Also, It removes redundancies (e.g., p \/ ~p ==> True),
> and contradictions (e.g., p /\ ~p ==> False).
>
> But depending on the formula, Metis will try to get a CNF of the formula
> with the minimum number of clauses. Surely, I'm missing other usages.
>
> conjunct extracts a conjunct in a conjunction.
> clausify finds the basic normal form (the basic one), (form o toFormula).
> simplify: although it seems many happens inside this rule, I could say it
> works
> with many ideas similar to canonicalize, like removing redundancies, or
> contradictions.
> Always traversing the list of formulas of the derivations, trying to get a
> smaller
> a formula by applying definitions, tautologies, among others.
>
>
> resolve inference is just the binary resolution theorem that with the same
> name
> appears in TSTP derivations as the resolve rule.
>
> If you have any suggestions or corrections to make, please do not
> hesitate to let me know.
>
> Thanks in advance for your time.
>
> Best,
>
> Jonathan Prieto-Cubides
>
> La información contenida en este correo electrónico está dirigida únicamente
> a su destinatario y puede contener información confidencial, material
> privilegiado o información protegida por derecho de autor. Está prohibida
> cualquier copia, utilización, indebida retención, modificación, difusión,
> distribución o reproducción total o parcial. Si usted recibe este mensaje
> por error, por favor contacte al remitente y elimínelo. La información aquí
> contenida es responsabilidad exclusiva de su remitente por lo tanto la
> Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
> information contained in this email is addressed to its recipient only and
> may contain confidential information, privileged material or information
> protected by copyright. Its prohibited any copy, use, improper retention,
> modification, dissemination, distribution or total or partial reproduction.
> If you receive this message by error, please contact the sender and delete
> it. The information contained herein is the sole responsibility of the
> sender therefore Universidad EAFIT is not responsible for what the message
> contains.