Technische Universität München, Fakultät für Informatik Lehrstuhl Informatik IV, Research Group Automated Reasoning
The E Equational Theorem Prover, Stephan Schulz

5th International Workshop on the Implementation of Logics

Schema of Montevideo

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:

We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems in practice. Researchers interested in participating are invited to send a short abstract (4-8 pages) to 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, PDF, or plain ASCII.

Final versions

The final versions should be prepared in LaTeX using the Springer Verlag llncs class. Please send the final Postscript file together with the source code and all the necessary input files by email to Please do not number the pages. The deadline for the final versions is March 4th, 2005.

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:

Please notice that the deadline for submission and other dates have been moved back after multiple requests.

Workshop Program

Note: All talks are scheduled for 30 minutes of presentation and 15 minutes of discussion.

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:

Elvira Albert Universidad Complutense de Madrid
Alessandro Cimatti ITC/irst, Trento
Bart Demoen Katholieke Universiteit Leuven
Ullrich Hustadt University of Liverpool
Boris Konev (Co-Chair) University of Liverpool
Bernd Löchner Universität Kaiserslautern
William McCune Argonne National Laboratory
Gopalan Nadathur University of Minnesota
Alexandre Riazanov University of Manchester
Renate Schmidt University of Manchester
Kostis Sagonas Uppsala University
Stephan Schulz (Co-Chair) Technische Universität München and Università degli Studi di Verona
Gernot Stenz Technische Universität München
Mark E. Stickel SRI International
Geoff Sutcliffe University of Miami

Previous Workshops: