Delivery-Date: 
From: plaisted@mpi-sb.mpg.de (David Plaisted)
Organization: Max-Planck-Institut fuer Informatik D-66123 Saarbruecken, Germany
Date: Wed, 18 May 94 11:26:59 +0200
Message-Id: <9405180926.AA12345@mpii02022.ag2.mpi-sb.mpg.de>
To: aal@anu.edu.au, deduktion@intellektik.informatik.th-darmstadt.de, 
    fg121@inferenzsysteme.informatik.th-darmstadt.de, info-hol@cs.uidaho.edu, 
    kgs@csdec1.tuwien.ac.at, nqthm-users@cli.com, qed@mcs.anl.gov, 
    rewriting-list@lorraine.loria.fr, theorem-provers@mc.lcs.mit.edu
Subject: CADE tutorial on model-directed theorem proving
Cc: plaisted@mpi-sb.mpg.de


		     Call for Participation

			CADE 12 Tutorial

      The Use of Semantics in a Herbrand-Based Proof Procedure

             Heng Chu, Shie-Jue Lee, and David Plaisted

             University of North Carolina at Chapel Hill
               National Sun Yat-Sen University, Taiwan
                         MPI fuer Informatik
                   Universitaet Kaiserslautern 

		       Monday, June 27, 1994
			   Nancy, France


        The clause linking method (CLIN), implemented by Shie-Jue Lee,
and its extension to semantics (CLIN-S), implemented by Heng Chu, are
refutational clause-form theorem provers for first-order logic.  These
methods work by enumerating instances of the input clauses and then
applying a propositional decision procedure similar to the Davis and
Putnam method.  Thus they go back in spirit to the early methods of
Davis, Gilmore and Prawitz.  These methods are an attempt to eliminate
some of the propositional inefficiencies in resolution and other
common theorem proving strategies.  CLIN-S has the additional interest
that it makes use of nontrivial structures, or semantics, to guide the
search.  It demonstrates unsatisfiability by the failure of a
persistent attempt to construct a model of the input clauses.

        These provers have obtained proofs in a number of areas with
little guidance, including propositional calculus, logic puzzles,
simple set theory, temporal logic, and modal logic.  In addition,
CLIN-S has obtained automatic proofs of the intermediate value
theorem, am8, exq1, exq2, exq3, three of Bledsoe's limit theorems,
Andrew's challenge problem, Eder's problems, pelletier 38, and a
version of the unsolvability of the halting problem.  For these, no
switches were set, and the user only chooses a model, which is often a
trivial one.  Many of these problems are difficult for most other
provers without substantial guidance.

        CLIN-S is also interesting because of its combination of two
additional (incomplete) methods with semantic hyper-linking, which is
in itself complete.  One of them is a version of resolution designed
to eliminate large literals from proofs, and another is unit-resulting
(UR) resolution, which eliminates the Horn part of proofs.  What
remains is a proof with small literals and non-Horn clauses; clause
linking with semantics is particularly effective on such problems.  In
addition, this prover uses decision procedures, not to test for
validity, but to test if a clause is satisfied by the user-specified
structure.


        David Plaisted will give an introductory lecture, Shie-Jue Lee
will discuss CLIN, and Heng Chu will discuss CLIN-S.  We will make
CLIN and CLIN-S available by anonymous ftp; user manuals will be
provided to participants in the tutorial and instruction on how to use
the provers will be given.


	Information about registration and accommodations is available
by anonymous ftp on the machine

			     ftp.loria.fr

in the directory

		    pub/loria/conferences/CADE-12

and e-mail queries may be directed to

			   cade-12@loria.fr