Events

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 proof-verification 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 first-order, but with an important second-order construct enabling one to package definitions and theorems into reusable proofware components - is a variant of the Zermelo-Fraenkel set theory, ZFC, with axioms of regularity and global choice. This is apparent from the very syntax of the language, borrowing from the set-theoretic 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 built-in mechanisms, tailored on ZFC, which constitute its inferential armory. Rather peculiar aspects of Ref, in comparison to other alike proof-assistants, 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 algorithm-correctness verification. To achieve relatively short, formally checked, proofs of properties enjoyed by claw-free 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 based-system 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 resolution-based provers.