Proof planning with multiple strategies

DOI10.1016/j.artint.2007.11.004zbMath1182.68259OpenAlexW2081924722MaRDI QIDQ2389631

Andreas Meier, Erica Melis, Jörg H. Siekmann

Publication date: 17 July 2009

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2007.11.004

zbMATH Keywords

theorem provingplanningmeta-reasoningproof planningblackboard architecture

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Computer supported mathematics with \(\Omega\)MEGA

Uses Software

• GAP
• IsaPlanner
• OTTER
• SPASS
• SicoTHEO
• HR
• Waldmeister
• Lambda-Clam
• Prodigy
• TRAMP
• Bliksem
• Multi

Cites Work

• Experiments with proof plans for induction
• Computer supported mathematics with \(\Omega\)MEGA
• Challenge problems in elementary calculus
• Artificial intelligence: methodology, systems, and applications. 8th international conference, AIMSA '98. Sozopol, Bulgaria, September 21--23, 1998. Proceedings
• Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
• Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
• Constraint solving for proof planning
• Productive use of failure in inductive proof
• Knowledge-based proof planning
• Integrating planning and learning: the PRODIGY architecture
• Automated Deduction – CADE-20
• Mathematical Knowledge Management
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item