Atlas home || Conferences | Abstracts | about Atlas
Homepage: http://www.dfki.de/floc-ws13/
Organizers: Dieter Hutter, Alan Bundy, Fausto Giunchiglia, Andrew Ireland
Deadline for abstracts: April 01, 1999
Description:
Proof by Mathematical Induction presents the Automated Deduction community with some very challenging research problems.
The aim of this one day workshop is to create an informal forum in which hot-topics and emerging techniques can be presented and
discussed. The workshop continues and focuses the efforts of previous workshops held in conjunction with AAAI'93, CADE'94,
CADE'96, CADE'97, CADE'98.
TOPICS OF INTEREST Application to formal methods: Formal program development is becoming a mature and established discipline with a dynamic and increasing market share. Induction is one of the key techniques when dealing with abstract datatypes. The aim of this session is to bring together the merits of inductive theorem proving techniques and the needs of formal methods in an industrial application scenario. Higher-order inductive theorem proving: Higher-order logics provide a rich framework for expressing and reasoning about formal specifications. The importance of mechanizing formal reasoning within higher-order logics is reflected by the sustained growth in popularity of verification environments such as HOL, Isabelle and PVS. The aim of this session is to address the adequacy of current automated techniques for inductive proof within the context of higher-order logics. Meeting the challenges: To be a true challenge, a problem should lie just beyond the scope of current techniques. Here we are also interested in problems which demonstrate the unique merits of inductive theorem proving techniques. Submitted challenge problems will be displayed on the Web prior to the workshop. Researchers will then be invited to submit solutions or counter challenges. The aim of this workshop session will be to debate the relative merits of the challenges and solutions.
Date received: February 07, 1999
© 2008 Atlas Conferences Inc.