The IJCAR 2008 Workshop on
Evaluation of Systems for Higher Order Logic
(ESHOL)
will be held
10-11th August 2008,
as part of
The 4th International Joint Conference on
Automated Reasoning
Sydney, Australia,
10th-15th August 2008
This workshop brings together practitioners and researchers who are involved
in the development of reasoning systems based on higher-order logic.
The workshop will stimulate and foster the build-up of an infrastructure that
supports research, development, and deployment of higher-order reasoning
systems.
A particular focus is on means to evaluate higher-order reasoning systems.
Advances in these aspects of reasoning in higher-order logic will make
higher-order reasoning system easier to use in applications, e.g., hardware
and software verification, knowledge based reasoning, and computer aided
mathematics.
The workshop's notion of higher-order includes, but is not limited to,
ramified type theory, simple type theory, intuitionistic and constructive
type theory, and logical frameworks.
The workshop's notion of reasoning systems includes automated and
semi-automated provers, model generators, as well as proof and model checkers.
The workshop will have three parts:
- Evaluation of Higher-Order Reasoning Systems
- Frameworks and tools for evaluation
- Collections of test problems
- Problem representation languages
- Evaluation of automated higher-order reasoning systems, in
particular, higher-order theorem provers
- Evaluation of interactive higher-order reasoning systems
- Evaluation of systems working for different higher-order logics and
varying semantics
- Descriptions of Successful Higher-Order Reasoning Systems
- Logical frameworks
- Higher-order automated theorem provers
- Interactive proof assistants supporting the partial automation of
higher-order logic
- Higher-order model checkers and higher-order model generators
- Systems that automate natural fragments of higher-order logic, such
as monadic second-order logic
Due to the evaluative character of the workshop, descriptions of both
existing and novel systems are welcomed.
Descriptions of existing systems should stress successful applications and
evaluations.
- System Demonstration and System Competition
The systems described in the second part will be demonstrated.
Moreover, a first competition "happening" for automated theorem provers
for simple type theory is planned.
This competition will be similar to the CASC competition for first-order
reasoning systems.
It will exploit and test the TPTP problem representation language for
simple type theory, which was recently developed by the organizers.
We envision attendees that are interested in fostering the development and
visibility of reasoning systems for higher-order logics, and the connection
between research on the various flavors of higher-order logic.
We are particularly interested in comparisons of the practical strengths of
higher-order reasoning systems and in a discusssion on the development of a
higher-order version of the TPTP.
Due to the intricate nature of higher-order logic, we are also interested
in a discussion on what practical strength means in the context of
higher-order logic and how it can be measured.
Organization
The workshop will be a one-and-a-halfday workshop, organized as follows:
- Day 1: 9:00-10:00am - Evaluation of Higher-Order Reasoning Systems
- Day 1: 10:30-12:30pm - Evaluation of Higher-Order Reasoning Systems
- Day 1: 2:00-3:00pm - Descriptions of Successful Higher-Order Reasoning Systems
- Day 1: 3:30-5:30pm - Descriptions of Successful Higher-Order Reasoning Systems
- Day 1: 5:30-End - Panel Discussion:
- Day 2: 9:00-12:00am - System Demonstration and System Competition
Program Committee
The workshop organizers are
Christoph Benzmüller,
Florian Rabe,
Carsten Schürmann,
and
Geoff Sutcliffe,
If you have any questions about the workshop, please email the organizers.
Journal Publication
A special issue of the
Journal of Applied Logic, based around around the topic of the ESHOL
workshop, is planned (the JAL has agreed), provided there are sufficiently
many strong submissions.
The special issue will target ESHOL participants, but will also also accept
submissions from the broader community.
Submission
Submission of papers for presentation at the workshop, and
proposals for system and application demonstrations at the workshop,
are now invited.
Submissions will be reviewed, and a balanced program of high-quality
contributions will be selected.
Submissions must be in PDF, and must conform to the format
produced by LaTeX with this template
(this is what the PDF should look like).
There is a 20 page limit.
Long listings of problems or computer output should be relegated to a
referenced WWW site.
Submission is via
EasyChair
(thanks to Andrei Voronkov).
The selected contributions will be printed as workshop proceedings, and
will also be published as
CEUR Workshop Proceedings.
Important dates
- Abstract submission deadline - 19th May
- Submission deadline - 26rd May
- Papers distributed to PC - 30th May
- Reviews due in from PC - 23rd June
- Notification of acceptance - 27th June
- Final versions due - 14th July
- Workshop - 10-11th August