Automated Deduction in Equational Logic and Cubic Curves

by W. McCune and R. Padmanabhan

Table of Contents

(For more, you'll have to get a copy of the book.)
1. Introduction
    1.1 Algebras and Equational Logic
    1.2 Outside of Equational Logic
    1.3 First-Order and Higher-Order Proofs
    1.4 Previous Applications of Automated Deduction
    1.5 Organization

2. Otter and MACE
    2.1 Definitions
    2.2 Otter
        2.2.1 The Main Loop
        2.2.2 General Strategies
        2.2.3 Equational Problems
        2.2.4 Equational Problems with the Rule (gL)
        2.2.5 Conjectures with Deduction Rules
        2.2.6 Running  Otter
        2.2.7 Example Input Files and Proofs
        2.2.8 Soundness of  Otter
    2.3 MACE
        2.3.1 Use of MACE
        2.3.2 Soundness of MACE

3. Algebras over Algebraic Curves
    3.1 What Is a Uniqueness Theorem?
        3.1.1 The Rigidity Lemma
        3.1.2 Applications to Cubic Curves
    3.2 The Median Law
    3.3 Abelian Groups
    3.4 Uniqueness of Group Laws
    3.5 Uniqueness of n-ary Steiner Laws
    3.6 Group Laws on a Quartic Curve

4. Other (gL)-Algebras
    4.1 Equations Consistent with (gL)
        4.1.1 Abelian Groups
        4.1.2 Quasigroups
        4.1.3 Boolean Groups
        4.1.4 Cancellative Semigroups
    4.2 Theories Strictly Inconsistent with (gL)
    4.3 Quasigroups and the Overlay Principle
    4.4 Closure Conditions and (gL)
    4.5 A Discovery Rule

5. Semigroups
    5.1 A Conjecture in Cancellative Semigroups
    5.2 Theorems Supporting the Conjecture
    5.3 Meta-Abelian CS and the Quotient Condition

6. Lattice-Like Algebras
    6.1 Equational Theory of Lattices
        6.1.1 Quasilattices
        6.1.2 Weakly Associative Lattices
        6.1.3 Near Lattices and Transitive Near Lattices
    6.2 Distributivity and Modularity
        6.2.1 Lattices
        6.2.2 Quasilattices
    6.3 Uniqueness of Operations
        6.3.1 Lattices
        6.3.2 Quasilattices
        6.3.3 Weakly Associative Lattices
        6.3.4 Transitive Near Lattices
    6.4 Single Axioms
        6.4.1 Presence of J\'onsson Polynomials
        6.4.2 A Short Single Axiom for Lattices
        6.4.3 Weakly Associative Lattices
    6.5 Boolean Algebras
        6.5.1 Frink's Theorem
        6.5.2 Robbins Algebra
        6.5.3 Ternary Boolean Algebra

7. Independent Self-Dual Bases
    7.1 Self-Dual Bases for Group Theory
    7.2 Self-Dual Schemas for Subvarieties of GT
    7.3 Self-Dual Bases for Boolean Algebra
        7.3.1 Padmanabhan's-Basis
        7.3.2 A-Basis from Pixley Reduction
        7.3.3 A-Basis from Majority Reduction
        7.3.4 A-Basis from Majority Reduction

8. Miscellaneous Topics
    8.1 Inverse Loops and Moufang Loops
        8.1.1 Bases for Moufang Loops
        8.1.2 Single Axioms for Inverse Loops and Moufang Loops
    8.2 Quasigroups
    8.3 Algebras of Set Difference

A. Theorems Proved
    A.3 Algebras over Algebraic Curves
    A.4 Other (gL)-Algebras
    A.5 Semigroups
    A.6 Lattice-like Algebras
    A.7 Independent Self-Dual Bases
    A.8 Miscellaneous Topics

B. Open Questions
    B.3 Algebras over Algebraic Curves
    B.4 Other (gL)-Algebras
    B.5 Semigroups
    B.6 Lattice-like Algebras
    B.7 Independent Self-Dual Bases
    B.8 Miscellaneous Topics

C. The Autonomous Mode

Index