Automatic construction and verification of isotopy invariants

DOI10.1007/s10817-007-9093-yzbMath1139.68050OpenAlexW2149404447MaRDI QIDQ928664

Simon Colton, Andreas Meier, Volker Sorge, R. L. McCasland

Publication date: 11 June 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-007-9093-y

zbMATH Keywords

Computer algebraSAT solvingAutomated theorem provingAutomated mathematicsClassification theoremsInvariant generationIsotopyModel generation

Mathematics Subject Classification ID

Related Items (2)

On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts

Uses Software

• GAP
• VAMPIRE
• SPASS
• Mace4
• Chaff
• CVC Lite
• E Theorem Prover
• HR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated discovery of new axiomatizations of the left group and right group calculi
• Single axioms for groups
• Applying SAT solving in classification of finite algebras
• Single axioms for groups and abelian groups with various operations
• Automated reasoning and exhaustive search: Quasigroup existence problems
• Mathematical applications of inductive logic programming
• Small latin squares, quasigroups, and loops
• Automatic Construction and Verification of Isotopy Invariants
• Automated Reasoning
• Computer Aided Verification
• Computer Aided Verification
• Isotopy Invariants in Quasigroups

This page was built for publication: Automatic construction and verification of isotopy invariants