Automated conjecture making in number theory using HR, Otter and Maple

DOI10.1016/j.jsc.2004.12.003zbMath1126.68100OpenAlexW1969189678WikidataQ115046816 ScholiaQ115046816MaRDI QIDQ2456561

Simon Colton

Publication date: 19 October 2007

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10044/1/674

zbMATH Keywords

automated reasoningcomputer algebra systemsmachine learningautomated mathematical discoveryintegration of reasoning systems

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Learning and adaptive systems in artificial intelligence (68T05) Number-theoretic algorithms; complexity (11Y16)

Related Items

Automated conjecturing. III. Property-relations conjectures, Automated conjecturing. I: Fajtlowicz's Dalmatian heuristic revisited, Automatic conjecturing of P-recursions using lifted inference

Uses Software

• Maple
• OTTER
• Mace4
• OEIS
• GRAFFITI
• MathWeb
• HR
• tptp2X

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Clausal discovery
• Tau numbers, natural density, and Hardy and Wright's theorem 437
• On conjectures of Graffiti
• An introduction to Zariski spaces over Zariski topologies
• Single axioms for groups and abelian groups with various operations
• Solution of the Robbins problem
• On the notion of interestingness in automated mathematical discovery
• Automated Deduction – CADE-19