[SCL] Issues (proof exchange)

[Tanel Tammet]

Hi,

Jim Hendler wrote:
>  I'm sure you all have argued about much of this in the past. and the 
> last thing I want is a dump of all that - but from an issues perspective 
> it would help to know how things scope.  In particular, I am very 
> interested both in the expression of rules on the web (connected to the 
> sorts of ontologies provided by OWL) and even more so in the exchange of 
> proofs on the web - which, if done right, could really prove an 
> amazingly strong case for the deployment of logics on web resources.  
> (For example, my favorite is an e-business contract in which your system 
> could send to my bank a proof that I had made a purchase at an agreed 
> upon price, and my bank would transfer the money assuming all was 
> appropriately signed and assured.  Tim BL's favorite is web site access 
> - his example is that you can access the W3C member site if you can 
> prove you work for one of the members - and that proof probably includes 
> some sort of signed statement from some database that you work for X, 
> coupled with the W3C's assertion that X is a member).
>  If that sort of proof exchange would be in scope, a number of issues 
> arise.

I'll write some notes on the proof exchange subject. I have no
gut feelings whether it would be sensible to take proof exchange into 
the SCL set of crucial issues to be solved or not. But the subject
is very interesting in itself, of course: hence the notes.

The attempts of proof exchange I have seen so far indicate that this
is relatively hard, yet sometimes achievable in practice, provided that
perfection is not looked for and naive far-from-perfect solutions
are allowed.

Let us look at proof exchange from two very different
logical viewpoints (both concentrate on proof verification as
(probably) the hard part of proof exchange):

- People doing type theory and higher order logics often use complex
   proof checkers. Proof checker takes in a detailed proof and checks
   whether the proof is OK. The proofs given to the checker are either
   constructed by hand, using a simple proof editor or using a fancy
   proof editor able to do some simple steps automatically.

   However, type theorists and other higher order people use a number of
   different logics, and the logics keep evolving. Hence it would be
   really hard for them to come to a common understanding as of
   which steps are valid and which not.

- In ordinary FOL we do not have the fundamental hardships the higher
   order people have to encounter.

   However, when you look at how provers work, then it becomes clear
   that very often they do large and complex proof steps, and it is hard
   to keep detailed data about the decomposition of these complex
   steps. For example, when you normalise a term, let us say
   +(s(s(0)),s(s(0))), to s(s(s(s(0)))), using two ordinary
   equalities defining plus, then the result of the normalisation
   is kept, but the intermediate values typically not. In fact, keeping
   all the detailed information about the exact atomic normalisation
   steps leading to the final result would waste a lot of space and time,
   and is mostly avoided. A common solution is to track all the clauses
   used during the normalisation, plus perhaps the derivation rules
   used, but not the exact order of atomic normalisation steps.

   A similar situation arises with non-equality derivations as well,
   where again several atomic steps (for example, several binary
   resolutions) may lead to a new kept clause or subgoal,
   without all the intermediate steps being explicated
   in the output proof.

   The situation is seriously aggravated if we deal with purely
   propositional formulas (prop sat checkers normally do not generate
   any unsatisfiability proofs at all, due to efficiency considerations)
   or built-in theories (for example, arithmetic)
   which do very large proof steps (for example, by solving an
   equation).

   When there is a real need to check proofs, then one solution
   I have seen used is to simply give the proof checker a proof
   where for each step a set of antecedents and a result is given,
   with no detailed or obligatory information about how to get the result
   from the antecedents.

   The proof checker then (again!) carries out real proof
   search for each step, but since these steps are much smaller than
   the whole proof, this is normally much easier than doing the
   whole proof search. During this proof-checking search it can
   be feasible to use only small atomic steps and keep all the
   data about them, so that a new proof could be output, which
   contains smaller steps than the one before.

   Both Stephan Schulz's E and my Gandalf use such a stepwise proof
   verification technique by employing a classical third-party
   prover (McCune's Otter) to verify the steps one after another.
   Sometimes (but very rarely) the steps of E or Gandalf are too
   big for Otter to manage in sensible time.

   To summarise, the issue is the granularity of a proof. How
   small should the steps be to make it meaningful to ouput
   a proof? What kinds of steps are OK and what not?


These notes probably did not get us any closer to the solution
of proof exchange. I was simply trying to point to some of the
sub-issues which make the whole proof exchange issue
relatively hard.

This said, I do not think the proof exchange
is hopelessly hard - provided we do not go deep into details and
do not try to create a nomenclature of specific admissible proof
steps. An almost trivial solution of accepting as a proof
any tree where all the parent nodes are derivable from their
children (using whatever rules, with an unbounded number
of children) might work out OK not only for E and Gandalf,
but for most systems. We actually devised one such XML-based proof 
syntax at the company called Safelogic: involved were several people 
from Safelogic, Stephan Schulz (of the E prover) and me (of the Gandalf 
prover). After some iterations we came to a draft spec which was far 
from perfect but seemed to be workable for the people and
systems involved.

BTW, I'll add a small excerpt of the Safelogic XML
standard for FOL proofs to the end of this message: it is
NOT DIRECTLY USABLE for SCL (for example, it
only treats clause syntax) but it may give some ideas.

Regards,
          Tanel Tammet


%-------------------------------------
%
% An excerpt from the copyrighted XML proof format
% spec draft from Safelogic (www.safelogic.se)
%
%---------------------------------------

%
% Note from Tanel: all clauses are assumed to contain a unique name
% (ordinarily a number) used to refer to the clause in the scope
% of one proof file
%

\subsection*{The proof}

The proof format is built around derivation rules of the form

$$ \frac{A_1 \; \ldots \; A_n}{B_1 \; \ldots \; B_m} \quad \mbox{Name} $$

\noindent where the $B_i$ are conclusions derived from the premises
$A_k$ by the rule called ``Name''.

This is represented in the \texttt{deduction} and \texttt{inference}
elements. The elements in effect represent the same thing but an
\texttt{inference} should be thought of as a ``small'' step. The elements
have the following structure

\begin{verbatim}
   <deduction type="Type" [comment="Comment"] [info="Info"]>
      {premise}*
      {clause}+
   </deduction>

   <inference type="Type" [comment="Comment"] [info="Info"]>
      {premise}*
      {clause}+
   </inference>
\end{verbatim}

\noindent where \texttt{type} is the type of the inference and
\texttt{comment} is a text field available for possible
clarification. For instance, in the case of binary resolution, it
could state that the derivation step was binary resolution with a unit
clause.  The type corresponds to the name of the derivation rule with
the addition that deductions via axioms are called \texttt{Initial}.
The \texttt{info} attribute given additional information on the deduction
or inference step, for instance that AC-unification was made within the
step.

To make things standardized, a set of deduction types are predefined

\begin{description}
\item[initial] The clause was in the initial clause set
\item[binary] Binary resolution
\item[hyper] Hyperresolution
\item[paramodulation] Paramodulation
\item[pseudo-splitting] Pseudo splitting
\item[rewrite] A rewrite step
\item[instantiation] Instantiation of variables
\end{description}

Other deduction types can be specified as well using the mechanism
described in section \ref{Axiomatization}.

....... SNIP .......

A derivation is a sequence of such \texttt{deduction} elements. A proof
is a derivation leading to the empty clause.

\begin{verbatim}
   <data>
      {deduction|inference}+
   </data>
\end{verbatim}
%-------------------------------------------