Invited Speakers

Eugenio Omodeo (Dipartimento di Matematica e Geoscienze / DMI, Università
degli Studi di Trieste, Italy)
Proof Verification within Set Theory: Exploiting a New Way of Modeling Graphs
Abstract. This talk illustrates proofverification technology based on set theory, also reporting on experiments carried out with AEtnaNova, aka Ref. The said verifier processes script files consisting of definitions, theorem statements and proofs of the theorems. Its underlying deductive system  mainly firstorder, but with an important secondorder construct enabling one to package definitions and theorems into reusable proofware components  is a variant of the ZermeloFraenkel set theory, ZFC, with axioms of regularity and global choice. This is apparent from the very syntax of the language, borrowing from the settheoretic tradition many constructs, e.g. abstraction terms. Much of Ref's naturalness, comprehensiveness, and readability, stems from this foundation; much of its effectiveness, from the fifteen or so builtin mechanisms, tailored on ZFC, which constitute its inferential armory. Rather peculiar aspects of Ref, in comparison to other alike proofassistants, are that Ref relies only marginally on predicate calculus and that types play no prominent role, in it, as a foundation. The selection of examples, mainly referred to graphs, to be discusses in this talk, reflects today's tendency to bring Ref's use closer to algorithmcorrectness verification. To achieve relatively short, formally checked, proofs of properties enjoyed by clawfree graphs, we took advantage of novel results about representing their (undirected) edges via membership.
Acknowledgements. Partial funding was granted by the INdAM/GNCS 2013 project "Specifica e verifica di algoritmi tramite strumenti basati sulla teoria degli insiemi".  Dominique Pastre (Université Paris Descartes,
France)
Mathematical Theorem Proving, from Muscadet0 to Muscadet4, Why and How
Abstract. We will present the ideas and the choices which have been made throughout the development of the Muscadet theorem prover. We will first see the principles and main ideas which lead to a first prover in the context of the time, influenced by a famous paper by Woody Bledsoe. This program used "natural" methods and was applied to set theory. It was then rewritten as a knowledge basedsystem where an inference engine applied rules, given or automatically built by metarules which expressed general or specific mathematical knowledge. It has been applied to some difficult problems. In order to allow more flexibility for expressing knowledge, it has been rewritten in Prolog, allowing the knowledge to be more or less declarative or procedural. To work with the TPTP Library the system had to work without knowing anything about mathematics except predicate calculus. All mathematical concepts had to be defined with mathematical statements, and the belonging relation handled as any other binary relation. To avoid translating knowledge to TPTP syntax, TPTP syntax has been used (this unfortunately forbade the use of some abbreviations mathematicians are comfortable with). Last but not least, the relevant trace has been extracted to give a proof easily read by anyone, except in the case of failure, when all steps may be displayed to understand (manually) the reasons for the failure. Muscadet has participated to CASC competitions. The results show its complementarity with regard to resolutionbased provers.