[mizar] instance checking procedure

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

I am forwarding here Bill McCune's pointers to an interesting instance (or 
rather entailment) checking procedure that seems to be in some sense 
stronger than the current Mizar checker (more exactly, its part called 
"Unifier"). It seems to me that the treatment of existential 
variables is "done right" there. Champeaux's article is online at 
http://portal.acm.org/citation.cfm?doid=6490.6491 , the procedure is 
called INSTANCE there.

Best,
Josef

---------- Forwarded message ----------
Date: Tue, 17 Jan 2006 10:10:03 -0600
From: William McCune <mccune@mcs.anl.gov>
To: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
Cc: William McCune <mccune@mcs.anl.gov>, mccune@mcs.anl.gov
Subject: Re: MoMM (fwd)


The procedure I referred to, applying subsumption directly to
negation-normal-form formulas, is rather complicated and not
well documented.  I don't know if it has ever been written down
formally in a way that's easy to understand.  Here is the
basic reference:

@article{ miniscope,
    author = "D. Champeaux",
    title = "Sub-problem finder and instance checker,
                two cooperating modules for theorem provers",
    journal = "J. ACM",
    year = 1986,
    volume = 33,
    number = 4,
    pages = "633--657"}

I first learned about it in 1984 from Champeaux's thesis,
and I used it for a database application:

@article{ constraints-jacm,
    author = "W. McCune and L. Henschen",
    title = "Maintaining State Constraints in Relational
                    Databases: {A} Proof Theoretic Basis",
    journal = "J. ACM",
    year = 1989,
    volume = 36,
    number = 1,
    pages = "46--68"}

I've written code for it several times, with several variations
and simplifications.  First in Prolog for the database application,
then several versions in C.  Otter has a simplified version,
and Prover9 has a different simplified version.

I don't know if anyone else has used it for anything.

The procedure does transformations on first-order formaulas,
preserving equivalence.  I think the most important use of
the procedure is to simplify problems, giving sets of independent
subproblems.

One of the main operations is to reduce the scopes of quantifiers.
As this happens, subformulas get distributed, and they can blow
up in size.  Therefore the other main opertion is to detect
redundancy in subformulas (which may have quantifiers).  This
redundancy detection is by a subsumption procedure applied
to negation-normal-form formulas.

See

   http://www.mcs.anl.gov/~mccune/prover9/examples/fof/index.html

for some Prover9 examples with TPTP problems.  (Prover9's
implementation uses a shortcut that makes the NNF subsumption
procedure less complete than it could be.)