News

September 30, 2013: FWF project “Interactive Proof: Proof Translation, Premise Selection, Rewriting” accepted

Cezary Kaliszyk’s project proposal “Interactive Proof: Proof Translation, Premise Selection, Rewriting” has been accepted by the Austrian Science Fund. The project is planned for 3 years and will commence shortly. The volume of the project is EUR 323K.

The project aims to combine interactive proof systems with automated to proving theorems. Specifically it intends to use algorithms coming from automated theorem proving, computer algebra and rewriting to make proof assistants easier to use. The long term goal is to make formal proof development an easy to use tool in mainstream mathematics and computer science.