About certain rules used in Spacer

[panda2134]

Hi! I'm trying to use the print-certification function in spacer. The certificate emitted looks like this:

(let ((a!1 (forall ((A E))
             (! (=> (and (E.Sem A 1 1 1) (E.Sem A 4 2 4) (E.Sem A 2 5 5))
                    realizable)
                :weight 0)))
      (a!2 (asserted (forall ((A E) (B Int) (C Int))
                       (! (E.Sem A B C B) :weight 0))))
      (a!3 ((_ hyper-res 0 0)
             (asserted (forall ((A E) (B Int) (C Int))
                         (! (E.Sem A B C C) :weight 0)))
             (E.Sem $1 2 5 5))))
(let ((a!4 ((_ hyper-res 0 0 0 1)
             (asserted (=> realizable query!0))
             ((_ hyper-res 0 0 0 1 0 2 0 3)
               (asserted a!1)
               ((_ hyper-res 0 0) a!2 (E.Sem $1 1 1 1))
               ((_ hyper-res 0 0) a!2 (E.Sem $1 4 2 4))
               a!3
               realizable)
             query!0)))
  (mp a!4 (asserted (=> query!0 false)) false)))

However, I cannot understand what does the arguments of hyper-res, mp and asserted mean. To be exact, I know about their meaning, but I have no idea what does each argument correspond to. The documentation here seems hard to understand. Can anyone provide some examples of these rules?

[agurfinkel]

This is a resolution proof that explains how query is derived from input clauses.

asserted is used to mark formulas in the original problem input.
hyper_res is hyper resolution, one input to it is a clause, other are unit literals that are resolved.
Extra parameters to hyper_res supposed to indicate how to instantiate universal quantifiers, but right now they are not properly set and should be ignored.

An example of how to process such a proof is given here: https://github.com/agurfinkel/spacer-on-jupyter/blob/master/Dagstuhl2019.ipynb . See SpacerProof and how it is used.

An example of a proof in a more mathematical notation is here: https://arieg.bitbucket.io/pdf/synasc2019.pdf , slide 10.