Vol. 3 No. 1 (2010)

Articles

• Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure

  Geoff Sutcliffe, Christoph Benzmueller

  1-27

  • PDF

• Sets in Coq, Coq in Sets

  Bruno Barras

  29-48

  • PDF

• Basic first-order model theory in Mizar

  Marco Bright Caminati

  49-77

  • PDF

• Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets

  José Grimm

  79-126

  • PDF