Delivery-Date: 
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: schneide@ira.uka.de, John.Harrison@cl.cam.ac.uk
In-reply-to: schneide's message of Mon, 17 May 1993 19:29:52 +0200 <9305171819.AA25772@ted.cs.uidaho.edu>
Subject: First-Order Reasoning
Message-Id: <93Jun23.194052met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 23 Jun 1993 19:40:51 +0200


Hi Klaus,

  This is a very delayed reaction to your posting of May 17. 

You wrote

> 		============================
>		First-Order Reasoning in HOL
>		============================
>
> Reasoning in first-order logic can be roughly described as follows:
> First the formula which is to be proven is negated and skolemized. 
> Then it is to be proven that the resulting formula is unsatisfiable.
> Therefore, a finite number of instantiations of the quantified formulae
> has to be performed and afterwards a simple tautology checker is sufficient
> for the remaining proof.
>  The instantiations can be computed by an external first-order prover.

This is a good idea. The responses you got were all of the sort "well my
theorem prover can do this faster", but that's not the point. The
important point is that some external tool can find the instantiations,
and all one has to do in HOL is to apply the instantiations and check
for propositional validity. This "in-the-logic" work is presumably less
expensive in time and space than the search for the instantiations. Do
you have any references or information on the relative breakdown in
speed of the operations? As far as I know, both skolemization and
checking for propositional validity are NP-hard (correct me if I'm
wrong), but the search for instantiations is basically unbounded, being
a semi-decision procedure.

Of course, another good point behind this linkage is modularity - any
implementation of a first order reasoner would do just as well, since
there is a well-defined interface.

You concluded with

> Has anybody similar tactics or conversions?

Yes, I find the same situation with AC-rewriting. Finding the set of
unifiers is basically done by an external agent, while inside the logic
I have to do associative and commutative operations to make the
instantiated pattern identical to the term being rewritten. Only then
can replacement take place, by the rules of the logic. Finding the
unifiers is said to be worse-case doubly exponential, while establishing
formal identity modulo A and C axioms is polynomial (these complexity
results are work by P. Narendran).


Also, I am interested in the utility of first order provers in
verification - is automatic first order proof used much in Mephisto? I
am puzzled about automatic first order methods; to me they don't seem to
map very well to informal proof. I don't recall ever reading an informal
proof that says "... and now the result follows from a first order
validity". I must be confused about something!

Cheers,
Konrad.