Automatic construction and verification of isotopy invariants

DOI10.1007/S10817-007-9093-YMaRDI QIDQ928664zbMATH OpenOpenAlexFDO

Authors Volker Sorge, Andreas Meier, Simon Colton, Roy 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

Automated mathematicsAutomated theorem provingClassification theoremsComputer algebraInvariant generationIsotopyModel generationSAT solving

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• Automatic Construction and Verification of Isotopy Invariants
• Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
• Automated Reasoning
• Automated theorem proving in quasigroup and loop theory
• Applying SAT solving in classification of finite algebras

Cites work

• Applying SAT solving in classification of finite algebras
• Automated discovery of new axiomatizations of the left group and right group calculi
• Automated Reasoning
• Automated reasoning and exhaustive search: Quasigroup existence problems
• Automatic Construction and Verification of Isotopy Invariants
• Computer Aided Verification
• Computer Aided Verification
• scientific article; zbMATH DE number 5909822 (Why is no real title available?)
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 47663 (Why is no real title available?)
• scientific article; zbMATH DE number 1765682 (Why is no real title available?)
• scientific article; zbMATH DE number 2090305 (Why is no real title available?)
• scientific article; zbMATH DE number 2115087 (Why is no real title available?)
• scientific article; zbMATH DE number 784652 (Why is no real title available?)
• Isotopy Invariants in Quasigroups
• Mathematical applications of inductive logic programming
• Single axioms for groups
• Single axioms for groups and abelian groups with various operations
• Small latin squares, quasigroups, and loops

Cited in

(6)

• Boosting isomorphic model filtering with invariants
• On the generation of quantified lemmas
• Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
• Automatic Construction and Verification of Isotopy Invariants
• Algorithmic introduction of quantified cuts
• Automated Reasoning

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q928664)