5th International Workshop on the Implementation of Logics

The 5th International Workshop on the Implementation of Logics will be held in conjunction with the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'2004 (not a typo), in Montevideo, Uruguay, in March 2005 (not a typo). IWIL has been unusually sucessful in bringing together many talented developers, and thus in sharing information about successful implementation techniques for automated reasoning systems and similar programs.

We are looking for contributions describing implementation techniques for and implementations 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
• System descriptions

Submissions should be in standard-conforming Postscript, PDF, or plain ASCII.

Final versions

There is no strict page limit, but we expect about 15 pages per paper. Please ask the organizers beforehand if you need more than 20 pages. The Proceedings will be published as a technical report by the University of Liverpool.

Important information:

• Submission of abstracts: January 28th, 2005
• Notification: February 18th, 2005
• Final version: March 4th, 2005
• Workshop: March 13th, 2005

Workshop Program

Sunday, March 13th, 2005
9:00-9:45	Elvira Albert, German Puebla, and John Gallagher: A Partial Deducer Assisted by Predefined Assertions and a Backwards Analyzer
9:45-10:30	Maseratu Harao, Shuping Yin, Keizo Yamada and Kouichi Hirata: Efficient Second Order Predicate Matching Based on Projection Position Indexing
Coffee Break
11:00-11:45	Flavio L.C. de Moura, Mauricio Ayala Rincon, and Faiouz Kamareddine: A Framework for Simulating and Comparing Explicit Substitutions Calculi
11:45-12:30	Keizo Yamada, Shuping Yin, Masateru Harao and Kouichi Hirata: Development of an Analogy-Based Generic Sequent Style Automatic Theorem Prover Amalgamated with Interactive Proving
Lunch Break
14:00-14:45	Erik T. Mueller and Geoff Sutcliffe: Discrete Event Calculus Deduction using First-Order Automated Theorem Proving
14:45-15:30	Martin Pollet and Volker Sorge: Towards an Efficient Representation of Computational Objects
Coffee Break
16:00-16:45	Stephan Schulz and Maria Paola Bonacina: On Handling Distinct Objects in the Superposition Calculus
16:45-17:30	Yuan Zhang and Geoff Sutcliffe: Lemma Management Techniques in Automated Theorem Proving

Program committee:

Previous Workshops:

• Reunion Workshop (held in conjunction with LPAR'2000 on Reunion Island)
• Second Workshop (together with LPAR'2001 in Havana, Cuba)
• Third Workshop (together with LPAR'2002 in Tbilisi, Georgia)
• Fourth Workshop (together with LPAR'2003 in Almati, Kazakhstan)