Automatic Learning of Proof Methods in Proof Planning

DOI10.1093/JIGPAL/11.6.647MaRDI QIDQ4465166zbMATH OpenOpenAlexWikidataFDO

Authors Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller

Publication date 27 May 2004

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/ff53597bb1a954846c600ba7aef659cf342d69bc

zbMATH Keywords

automated reasoningautomated theorem provingknowledge acquisitionautomated learningproof planningmathematical reasoning systems

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Mechanization of proofs and logical operations (03B35)

Recommendations

• Towards learning new methods in proof planning
• Proof planning: A practical approach to mechanized reasoning in mathematics
• Automating Inductive Proofs Using Theory Exploration
• Automated constructivization of proofs
• Adaptation of declaratively represented methods in proof planning
• Automated theorem proving methods
• scientific article; zbMATH DE number 2090054
• scientific article; zbMATH DE number 3880144
• Automatic inductive theorem proving using Prolog

Cited in

(18)

• Learning strategies for mechanised building of decision procedures
• scientific article; zbMATH DE number 827983 (Why is no real title available?)
• SEPIA: search for proofs using inferred automata
• Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
• scientific article; zbMATH DE number 1341622 (Why is no real title available?)
• scientific article; zbMATH DE number 2090296 (Why is no real title available?)
• Mathematical Knowledge Management
• Automatic acquisition of search control knowledge from multiple proof attempts.
• Octopus: combining learning and parallel search
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Proof-pattern recognition and lemma discovery in ACL2
• Learning domain knowledge to improve theorem proving
• Improving the time efficiency of proving theorems using a learning mechanism
• Towards learning new methods in proof planning
• The TM system for repairing non-theorems
• Learning-assisted theorem proving with millions of lemmas
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Mining state-based models from proof corpora

Describes a project that uses

Uses Software

• OMEGA

This page was built for publication: Automatic Learning of Proof Methods in Proof Planning

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