23 April 2018: Jasmin Blanchette Title: Formal Proof for the Working Automated Reasoning Researcher Abstract: Starting with Automath and Mizar, a long-term dream of the interactive theorem proving community has been to develop proof assistants that can help working mathematicians. But what about researchers in automated deduction? Much like the shoemaker's children, we profess to love theorem provers but carry out most of our metatheoretical proofs with pen and paper (or LaTeX). Together with colleagues, I started an effort, called IsaFoL (Isabelle Formalization of Logic), that aims at developing libraries and a methodology for formalizing modern research in the field, using the Isabelle/HOL proof assistant. I will talk about what we have accomplished so far in terms of formalized metatheory, of the resolution and superposition proof calculi and of the CDCL calculus underlying modern SAT solvers, emphasizing the Isabelle features that make this work possible and enjoyable. Bio: Jasmin Blanchette is a lecturer at the Vrije Universiteit Amsterdam. He's the (co)developer of several tools in Isabelle, including the Nitpick counterexample generator and the Sledgehammer subsystem that integrates automatic theorem provers. He was recently awarded an ERC grant to work on efficient automatic higher-order proving, aiming at improving automation in proof assistants. Apr 23 2018 14.00 - 15.00 23 April 2018: Jasmin Blanchette Formal Proof for the Working Automated Reasoning Researcher IF 4.31/4.33
23 April 2018: Jasmin Blanchette Title: Formal Proof for the Working Automated Reasoning Researcher Abstract: Starting with Automath and Mizar, a long-term dream of the interactive theorem proving community has been to develop proof assistants that can help working mathematicians. But what about researchers in automated deduction? Much like the shoemaker's children, we profess to love theorem provers but carry out most of our metatheoretical proofs with pen and paper (or LaTeX). Together with colleagues, I started an effort, called IsaFoL (Isabelle Formalization of Logic), that aims at developing libraries and a methodology for formalizing modern research in the field, using the Isabelle/HOL proof assistant. I will talk about what we have accomplished so far in terms of formalized metatheory, of the resolution and superposition proof calculi and of the CDCL calculus underlying modern SAT solvers, emphasizing the Isabelle features that make this work possible and enjoyable. Bio: Jasmin Blanchette is a lecturer at the Vrije Universiteit Amsterdam. He's the (co)developer of several tools in Isabelle, including the Nitpick counterexample generator and the Sledgehammer subsystem that integrates automatic theorem provers. He was recently awarded an ERC grant to work on efficient automatic higher-order proving, aiming at improving automation in proof assistants. Apr 23 2018 14.00 - 15.00 23 April 2018: Jasmin Blanchette Formal Proof for the Working Automated Reasoning Researcher IF 4.31/4.33
Apr 23 2018 14.00 - 15.00 23 April 2018: Jasmin Blanchette Formal Proof for the Working Automated Reasoning Researcher
