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
- ABGT -- Abelian Group Theory
- BA -- Boolean Algebra
- CS -- Cancellative Semigroup
- CS-GL -- Cancellative (gL)-Semigroup
- DUAL -- Self-dual Algebras
- DUAL-BA -- Self-dual Boolean Algebra
- DUAL-GT -- Self-dual Group Theory
- GEO -- Geometry Configuration
- GT -- Group Theory
- HBCK -- Blok and Ferreirim
- IL -- Inverse Loop
- LT -- Lattice Theory
- MAJ -- Majority Polynomial
- MCV -- Mal'cev Polynomial
- MED -- Median Law
- MFL -- Moufang Loop
- NL -- Near Lattice
- OC -- Overlay Condition
- PIX -- Pixley Polynomial
- QGT -- Quasigroup Theory
- QLT -- Quasilattice Theory
- QUART -- Quartic Curve
- RBA -- Robbins Algebra
- RC -- Reidemeister Closure
- SD -- Set Difference
- STN -- Steiner Law
- TBA -- Ternary Boolean Algebra
- TBG -- Ternary Boolean Group
- TC -- Thomsen Closure
- TNL -- Transitive Near Lattice
- TRI -- Triangle Algebra
- UAL -- Unique Algebraic Law
- WAL -- Weakly Associative Lattice
- Theorem CS-GL-1 Cancellative (gL)-semigroups are commutative.
- Theorem CS-GL-2 Diassociative cancellative (gL)-groupoids are commutative.
- Theorem CS-GL-3 Nearly (1) associative cancellative (gL)-groupoids are commutative.
- Theorem CS-GL-4 Nearly (2) associative cancellative (gL)-groupoids are commutative.
- Theorem CS-GL-5 Nearly (3) associative cancellative (gL)-groupoids are commutative.
- Example CS-GL-6 Nearly (4) associative cancellative (gL)-groupoids are not always commutative.
- Theorem CS-GL-7 Nearly (5) associative cancellative (gL)-groupoids are commutative.
- Problem CS-GL-8 A (gL)-basis for identities common to x+y and x-y (1).
- Problem CS-GL-9 A (gL)-basis for identities common to x+y and x-y (2).
- Problem CS-GL-10 Nearly (6) associative cancellative (gL)-groupoids.
For further information, contact
William McCune
(mccune@mcs.anl.gov) or
R. Padmanabhan
(padman@cc.umanitoba.ca).