HR
The HR program for theorem generation. Automated theory formation involves the production of objects of interest, concepts about those objects, conjectures relating the concepts and proofs of the conjectures. In group theory, for example, the objects of interest are the groups themselves, the concepts include element types, subgroup types, etc., the conjectures include implication and if-and-only-if conjectures and these become theorems if they are proved, non-theorems if disproved. Similar to Zhang’s MCS program, the HR system -- named after mathematicians Hardy and Ramanujan -- performs theory formation in mathematical domains. It works by (i) using the MACE model generator to generate objects of interest from axiom sets (ii) performing the concept formation and conjecture making itself and (iii) using the Otter theorem prover to prove conjectures. In domains where Otter and MACE are effective, HR can produce large numbers of theorems for testing automated theorem provers (ATPs), or smaller numbers of prime implicates, which represent some of the fundamental facts in a domain. We explain how HR operates in S2 and give details of a representative session in S3. As discussed in S4, the applications of HR to automated reasoning include the generation of constraints for constraint satisfaction problems, the generation of lemmas for automated theorem proving, and the production of benchmark theorems for the TPTP library of test problems for ATP systems. HR is a Java program available for download here: http://www.dai.ed.ac.uk/ simonco/research/hr.
Keywords for this software
References in zbMATH (referenced in 23 articles , 2 standard articles )
Showing results 1 to 20 of 23.
Sorted by year (- Larson, C.E.; Van Cleemput, N.: Automated conjecturing. I: Fajtlowicz’s Dalmatian heuristic revisited (2016)
- Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel: Algorithmic introduction of quantified cuts (2014)
- Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014) ioport
- Heras, Jónathan; Komendantskaya, Ekaterina; Johansson, Moa; Maclean, Ewen: Proof-pattern recognition and lemma discovery in ACL2 (2013)
- Johansson, Moa; Dixon, Lucas; Bundy, Alan: Conjecture synthesis for inductive theories (2011)
- Aouchiche, M.; Hansen, P.: A survey of automated conjectures in spectral graph theory (2010)
- Pease, Alison; Smaill, Alan; Colton, Simon; Lee, John: Bridging the gap between argumentation theory and the philosophy of mathematics (2009)
- Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
- Sorge, Volker; Meier, Andreas; McCasland, Roy; Colton, Simon: Automatic construction and verification of isotopy invariants (2008)
- Aouchiche, Mustapha; Caporossi, Gilles; Hansen, Pierre: Variable neighborhood search for extremal graphs. 20. Automated comparison of graph invariants (2007)
- Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: User interaction with the Matita proof assistant (2007)
- Ritchie, Graeme: Some empirical criteria for attributing creativity to a computer program (2007) ioport
- Brankov, V.; Hansen, P.; Stevanović, D.: Automated conjectures on upper bounds for the largest Laplacian eigenvalue of graphs (2006)
- Colton, Simon; Muggleton, Stephen: Mathematical applications of inductive logic programming (2006)
- Colton, Simon; Muggleton, Stephen: Mathematical applications of inductive logic programming (2006) ioport
- Ritchie, Graeme: The transformational creativity hypothesis (2006)
- Colton, Simon: Automated conjecture making in number theory using HR, Otter and Maple (2005)
- Delahaye, David; Mayero, Micaela: Dealing with algebraic expressions over a field in Coq using Maple (2005)
- Meier, Andreas; Sorge, Volker: Applying SAT solving in classification of finite algebras (2005)
- Colton, Simon; Meier, Andreas; Sorge, Volker; McCasland, Roy: Automatic generation of classification theorems for finite algebras (2004)