Image courtesy of Gunkarta via the Wikimedia Commons.
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:
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 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.
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 results 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.
