Activities in interactive theorem proving in the Mechanized Reasoning Group
Fausto Giunchiglia, Mechanized Reasoning Group, IRST, Trento, Italy
Abstract:
The goal of this talk is to briefly present the research activities
in interactive theorem proving of the Mechanized Reasoning Group
(MRG). After a brief survey of all the main activities of MRG,
our talk will concentrate on two specific research topics. The first
is the development of an interactive theorem prover, called ABSFOL,
implementing reasoning with abstraction. The second is the development
of a theory for the interconnection and interactions of distinct
reasoning systems, possibly developed separately. To this extent we
will introduce the notion of OMRS (Open Mechanized Reasoning Systems).