2nd International Workshop on Implementation of Logics

*** The workshop is over. Get the proceedings. ***

Following the successful Reunion Workshop on Implementations of Logic (held in conjunction with LPAR'2000 on Reunion Island), we are now organizing a second workshop on this topic, to be held on December 8th, 2001. The workwhop will be held in conjunction with the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'2001, in Havana (La Habana), Cuba, December 3-7, 2001.

We have been looking for contributions describing the implementation of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to:

• Datastructures and algorithms for the efficient representation of logical concepts
• Practical constraint handling
• Implementation of provers for different logics
• Efficient model generation
• Issues of reliability, witness generation, and witness verification
• Propositional logic and decision procedures
• Implementation of higher order logics and lambda-calculus
• Proof search organization and efficient heuristics for classical and inductive provers
• Experiences with new or unusual calculi
• Evaluation and benchmarking of provers and other logic-based systems

The deadline has passed, please check below for the list of accepted papers!

Researchers interested in participating are invited to send a short abstract (4 pages) to schulz@informatik.tu-muenchen.de. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions.

Submissions should be in standard-conforming Postscript or plain ASCII. Final versions should be in Postscript and will be included in the proceedings. The proceedings of the workshop will be published as an MPI preprint by the Max-Plank-Institut für Informatik, and will be distributed at the workshop. If possible, please use LaTeX and the standard article class.

Important information:

• Submission of abstracts: September 15th
• Notification: October 8th
• Final version: November 15th. Please submit to Hans De Nivelle, nivelle@mpi-sb.mpg.de
• Workshop: December 8th, 2001, after LPAR

The main LPAR page has travel information. Note in particular that despite the embargo, US citizens are generally allowed to participate in scientific venues like LPAR or the workshop on Cuba by a general license.

Here is a PostScript version of the original call for papers.

Accepted papers

• Graham Fyffe, Joseph D. Horton, Yangping He: Experiments with Marmoset, a Deduction System based on Clausetrees
• Thomas Hillenbrand, Bernd Löchner: The Next Waldmeister Loop
• Bernd Löchner, Stephan Schulz: An Evaluation of Shared Rewriting
• Dominique Pastre: Implementation of Knowledge Bases for Natural Deduction
• Carsten Schuermann: Towards an Efficient Implementation of Explicit Substitutions
• Sylvain Soliman: Phase Model Checking for some Linear Logic Calculi
• Gernot Stenz, Reinhold Letz: Integration of Equality Reasoning into the Disconnection Calculus
• Geoff Sutcliffe: The Design and Implementation of a Compositional Competition-Cooperation Parallel ATP System

Program committee: