The HR program for theorem generation

DOI10.1007/3-540-45620-1_24MaRDI QIDQ4809066zbMATH OpenFDO

Authors Simon Colton

Publication date 12 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2392/23920285.htm

Mathematics Subject Classification ID

Recommendations

• Automated conjecture making in number theory using HR, Otter and Maple
• Managing Automatically Formed Mathematical Theories
• Automated Deduction – CADE-19
• ILP for mathematical discovery.
• scientific article; zbMATH DE number 5909822

Cited in

(11)

• HR
• Mathematical applications of inductive logic programming
• Dealing with algebraic expressions over a field in Coq using Maple
• Automated conjecture making in number theory using HR, Otter and Maple
• Making conjectures about Maple functions
• Category-based co-generation of seminal concepts and results in algebra and number theory: containment-division and Goldbach rings
• Managing Automatically Formed Mathematical Theories
• ILP for mathematical discovery.
• Conjectures, tests and proofs: an overview of theory exploration
• Considerations on approaches and metrics in automated theorem generation/finding in geometry
• Applying SAT solving in classification of finite algebras

Describes a project that uses

Uses Software

• OTTER
• Mace4
• TPTP

This page was built for publication: The HR program for theorem generation

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