Theory Development in an Automated Theorem Prover

  • Stéphane Ricour

Student thesis: Master typesMaster en sciences informatiques


Oyster/Clam is an automated theorem prover based on Martin-Löf's constructive theory of types. Recent work has centred round the notion of proof plan to guide the search for proofs. Experiments with proof plans for finding proofs by induction, using heuristics adapted from the work of Boyer and Moore, have shown encouraging results. This work apply this approach to the data structure of finite sets. A systematic approach is taken to building up the machinery needed to use such a theory, in the form of suitable tactics and a library of theorem.
la date de réponse1991
langue originaleAnglais
L'institution diplômante
  • Universite de Namur
SuperviseurBaudouin LE CHARLIER (Promoteur)

Contient cette citation