call for papers, previous message

From:     plaisted@uklirb.informatik.uni-kl.de
Subject:  Semantics Directed Automated Deduction
Date:     Wed, 18 May 1994 11:11:49 GMT


			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