Contents A "Theory" mechanism (Published paper) Three newsletters from a proof-checker's project logbook [BW] (Paper in preparation) An equational re-engineering of set theories (Published paper, currently under extensive revision) Inductive sets (First draft) A quick introduction to formative processes (One-page technical report) "Defining real numbers using Bishop's 'regular' Cauchy sequences" (draft scenario-script) Presentation on the "Theory" mechanism in Atlanta (Slides) "Three-variable statements of set-pairing" in Clermont-Ferrand (Slides) "Three language extension mechanisms for map calculus" in Madrid (Slides) Otter experiments concerning ordered groups [.pdf] [Proofs] Otter files concerning set theory "Proofware ipertestuale" (Slides of Rossini's thesis on hypertextual proofware) "Insolubilità del X problema di Hilbert" (Slides and code of Notarantonio's thesis on the unsolvability of Hilbert's 10th problem) A catalog of Boolean laws Catalog of definitions and theorems in the main scenario (Black-and-white version here) (Variant of a very important theory here) Address Eugenio Omodeo - Dipartimento di Informatica Università di L'Aquila Via Vetoio Loc. Coppito I-67010 L'Aquila phone: +39 0862 433126 fax: +39 0862 433180 email:omodeo@di.univaq.it
phone: +39 0862 433126 fax: +39 0862 433180
email:omodeo@di.univaq.it