call for papers,previous messageFrom:plaisted@uklirb.informatik.uni-kl.deSubject:Semantics Directed Automated DeductionDate: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