Program

9:30 Practical Session: Introduction to Prover9/Mace4.

Some introductory instructions on Prover9/Mace4 will be provided. We suggest people interested in this first part of the workshop bring their personal computers, so they can try examples in Prover9/Mace4 during the session.

10:30 Coffee Break

11:00 Proof Simplification and Prover9. Michael Kinyon (University of Denver, USA)

The growing use of automated theorem proving (ATP) tools -- such as Prover9, Waldmeister, Vampire or E in mathematics naturally raises the question of the complexity of proofs that such tools find. It is rarely the case that the first proof of a result found by an ATP is anything close to a simple proof, based on any measure of simplicity. In this talk, after a discussion of the given clause algorithm that underlies all modern ATPs, I will talk about how advanced proof finding strategies, especially proof sketches, can be used to help Prover9 (or E) find simpler proofs. These leads to a discussion of possible measures of simplicity: the total number of inferences in a proof, the maximum size of a clause, the width of the proof tree, etc. I will conclude with a discussion of the purpose of finding simpler proofs: while originally, humanization of proofs was part of the rationale, contemporary proofs are now so large as to preclude any possibility of humanization. 

12:00 Lunch

14:00 The Problems of Automatic Proofs. João Araújo (University Aberta, Portugal)

Theorem provers are able to solve complex problems, but one thing is to know a proof exists; a different thing is to understand it and possibly extract mathematical knowledge from it. In this talk I will survey the problems of automatic proofs and what has been done to overcome them.

15:00 Research Student Session: Extending Prover9. Ivo Robert

This talk aims to show a prototype of an application that extends Prover9/Mace4 functionality by adding Python scripting. These are the first results of an ongoing PhD thesis in Computational Algebra at Universidade Aberta. The modular architecture will be introduced first, followed a small demonstration of the application and how it can be easily extended with scripts.

15:30 Coffee Break

16:00 Notions of Simplicity and Automated Reasoning. Alan Cain (New University of Lisbon, Portugal)

Simplicity in proof is a concept that may include (or at least touch upon) criteria such as length, perspicuity, methodological purity, complexity of intermediate statements, choice of lemmata, and use of possibly controversial assumptions (for example, the axiom of choice). This talk will survey some notions of simplicity, consider how they motivate and guide the search for proofs (of both established and new results), and examine to what extent these notions have been and could be used in automated reasoning.

17:00 Closing Session