Automated deduction in equational logic and cubic curves

DOI10.1007/3-540-61398-6zbMath0921.03011OpenAlexW4211016048MaRDI QIDQ1919221

R. Padmanabhan, William W. McCune

Publication date: 4 August 1996

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61398-6

zbMATH Keywords

semigroupsequational logicMoufang loopsalgebraic geometryuniversal algebraMACEcubic curvesalgebras over algebraic curvesfinite models as counterexamplesgeometric logic algebraslattice-like algebrasself-dual basestheorem prover Otter

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Special algebraic curves and curves of low genus (14H45) Mechanization of proofs and logical operations (03B35) Computational aspects of algebraic curves (14Q05) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Software, source code, etc. for problems pertaining to algebraic geometry (14-04) Equational classes, universal algebra in model theory (03C05) Software, source code, etc. for problems pertaining to general algebraic systems (08-04)

Related Items

On weakly associative lattices and near lattices ⋮ Automatic proofs and counterexamples for some ortholattice identities ⋮ On the configurations of nine points on a cubic curve ⋮ Automatization of ternary Boolean algebras ⋮ Algebraic generalization of Diffie-Hellman key exchange ⋮ Dihedral semigroups, their defining relations and an application to describing knot semigroups of rational links ⋮ Paraconsistent constructive logic with strong negation as a contraction-free relevant logic ⋮ Constructive logic with strong negation is a substructural logic. I ⋮ The Legacy of a Great Researcher ⋮ Group Embedding of the Projective Plane PG(2, 3) ⋮ Every diassociative A-loop is Moufang ⋮ Constructive logic with strong negation is a substructural logic. II ⋮ Automated Deduction in Ring Theory ⋮ THE MOUFANG LAWS, GLOBAL AND LOCAL ⋮ On two alternative axiomatizations of lattices by McKenzie and Sholander ⋮ Moufang and commutant elements in magmas ⋮ The varieties of quasigroups of Bol-Moufang type: an equational reasoning approach. ⋮ Commutativity Theorems in Groups with Power-like Maps ⋮ Formalization of quasilattices ⋮ Rectangular quasigroups and rectangular loops.

Uses Software

• OTTER