8th International Workshop on the Implementation of Logics

Dvarapala, Guardian of the Temple. From the Wikimedia Commons (http://commons.wikimedia.org/wiki/File:Plaosan_Temple_Guardian.jpg)
Image courtesy of Gunkarta via the Wikimedia Commons.

The 8th International Workshop on the Implementation of Logics will be held October 10th, 2010, in Yogyakarta, Indonesia. The workshop is running in conjunction with the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-2010. 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.

Program committee

Submissions

Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full papers (up to 15 pages) via EasyChair. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions.

Submissions should be in standard-conforming PDF.

To submit a paper, go to the EasyChair IWIL page and follow the instructions there.

You can view the full call for papers.

Final versions

Final versions should be prepared in LaTeX using the easychair.cls class file. Proceedings will be published as EasyChair Proceedings.

If number and quality of the submissions warrant it, we plan to produce a special issue of a recognized journal on the topic of the workshop.

Important dates:

Dates are preliminary.

Proceedings

A preliminary version of the proceedings (~62 MB PDF) is now available. The official proceedings have also been published as Volume 2 of the EPiC Series in Computing.

Program

IWIL-2010, Sunday, 10 October 2010
10:00 - 11:00Coffee served
11:00 - 11:30Jesse Alama
Exploring Steinitz-Rademacher polyhedra: a challenge for automated reasoning tools
11:30 - 12:00Guido Fiorino
Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge
12:00 - 12:30L. Yohanes Stefanus and Ario Santoso
A PROLOG-based Prooftool for Type-Theory TAλ and Implicational Intuitionistic-Logic
12:30 - 14:00Lunch break
14:00 - 15.00Invited talk: Lawrence C. Paulson and Jasmin Christian Blanchette
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
Sledgehammer is a highly successful tool that makes automatic theorem provers available to an interactive theorem prover (Isabelle). It requires no user configuration: it can be invoked with a single mouse gesture at any point in the proof. It automatically finds any lemmas it requires from those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of resu1lts as Isabelle proof script: its output cannot be trusted, but it does not need to be trusted. Sledgehammer turns out to work particularly well with structured proofs, making it easy for beginners to construct substantial proofs. The invited talk will review the development of Sledgehammer and describe its impact on the Isabelle community.
15:00 - 15:30Harald Zankl and Martin Korp
On Implementing Modular Complexity Analysis
15:30 - 16:00Coffee break
16:00 - 16:30Pavel Klinov and Bijan Parsia
Implementing an Efficient SAT Solver for a Probabilistic Description Logic
16:30 - 17:00Carsten Fuhs and Peter Schneider-Kamp
Optimizing the AES S-Box using SAT
17:00The End

Previous Workshops:

Impressum