Knowledge-based proof planning

DOI10.1016/S0004-3702(99)00076-4zbMath0939.68822OpenAlexW2042236049MaRDI QIDQ1978469

Erica Melis, Jörg H. Siekmann

Publication date: 4 June 2000

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

Full work available at URL: https://doi.org/10.1016/s0004-3702(99)00076-4

zbMATH Keywords

theorem provingplanningmeta-level reasoningautomated proof planningintegrating constraint solvers

Mathematics Subject Classification ID

Related Items

Towards finding longer proofs, Proof planning with multiple strategies, \textit{Theorema}: Towards computer-aided mathematical theory exploration, Computer supported mathematics with \(\Omega\)MEGA, Comparing approaches to the exploration of the domain of residue classes., Agenda control for heterogeneous reasoners, Constraint solving for proof planning

Uses Software

• SETHEO
• Theorema
• OTTER
• SPASS
• Nuprl
• LCF
• Analytica
• EQP
• Waldmeister
• Prodigy
• PROTEIN
• Bliksem
• Omega-MKRP

Cites Work

• Experiments with proof plans for induction
• Challenge problems in elementary calculus
• SETHEO: A high-performance theorem prover
• Non-resolution theorem proving
• Integrating computer algebra into proof planning
• Inductive learning of search control rules for planning
• Analogy in inductive theorem proving
• A resolution principle for constrained logics
• Solution of the Robbins problem
• The Heine-Borel challenge problem. In honor of Woody Bledsoe
• Edinburgh LCF. A mechanized logic of computation
• Planning in a hierarchy of abstraction spaces
• Computer science today. Recent trends and developments
• Wie der Beweis der Vermutung von Baudet gefunden wurde
• STRIPS: A new approach to the application of theorem proving to problem solving
• Computer proofs of limit theorems
• Toward Mechanical Mathematics
• The undecidability of the D_A-unification problem
• Theorem Proving via General Matings
• On Matrices with Connections
• Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
• Theorem proving in cancellative abelian monoids (extended abstract)
• Integrating planning and learning: the PRODIGY architecture
• Ωmega: Towards a mathematical assistant
• A Machine-Oriented Logic Based on the Resolution Principle
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item