McCune/Padmanabhan Monograph Problems

This page leads to the input files and proofs.

Each of the members of the list below represents a lemma, theorem, corollary, counterexample, or open problem from the monograph. Each link takes you to a directory of files like these:

  [efh]*.in           - Otter input
  [efh]*.proof        - Otter proof
  [efh]*.proof-object - proof object corresponding to Otter proof
                        (the (gL) theorems don't have proof objects)
  x1.in               - MACE input
  x1.model            - MACE model
  paragraph.dvi       - the corresponding part of the monograph

Contents


Abelian Group Theory

Boolean Algebra

Cancellative Semigroup

Cancellative (gL)-Semigroup

Self-dual Algebras

Self-dual Boolean Algebra

Self-dual Group Theory

Geometry Configuration

Group Theory

Blok and Ferreirim

Inverse Loop

Lattice Theory

Majority Polynomial

Mal'cev Polynomial

Median Law

Moufang Loop

Near Lattice

Overlay Condition

Pixley Polynomial

Quasigroup Theory

Quasilattice Theory

Quartic Curve

Robbins Algebra

Reidemeister Closure

Set Difference

Steiner Law

Ternary Boolean Algebra

Ternary Boolean Group

Thomsen Closure

Transitive Near Lattice

Triangle Algebra

Unique Algebraic Law

Weakly Associative Lattice


For further information, contact William McCune (mccune@mcs.anl.gov) or R. Padmanabhan (padman@cc.umanitoba.ca).