Automated Reasoning Group
Lab |
ARG |
Description |
HOL |
Isabelle |
Members |
Haiku
The Automated Reasoning Group is concerned with the development and
application of theorem proving methodologies. Theorem proving
presents a challenge for logicians and computer scientists alike. Use
of theorem proving methods is finding substantial application with the
increasing use of computers in safety-critical applications, whose
workings require detailed analysis.
There is a fuller
description of the group's history and current interests and
a list of
members and their areas of expertise.
Related Groups and Meetings
eats on Mondays at 12:45pm in FW26.
The
ARG Lunch
eats on Tuesdays at 1:00pm in GS15.
Logic and Semantics Seminars:
Formal talks on Friday at 2:00pm, usually in FW11.
news:ucam.cl.isabelle
Lively discussion on the theorem prover Isabelle.
news:ucam.cl.automated-reasoning
Local automated reasoning group announcements.
Proof environments
Information on the
HOL system for interactive theorem proving in a higher-order logic
and
Isabelle generic theorem prover
is available.
You may also download
HOL
or
Isabelle
by anonymous ftp.
Publications
Both
HOL related papers
and
Isabelle related papers
are available.
Other relevant papers may be found amongst the
lab technical reports.
We also publish a selection of inspiring
Theorem Proving Haiku.
Miscellaneous
Lab |
ARG |
Description |
HOL |
Isabelle |
Members |
Haiku
Page last updated on Tue Dec 12 16:31:29 GMT 2006
by Thomas Tuerk
(tt291@cl.cam.ac.uk)