Knowledge-based proof planning
type: Item
instance of: scholarly article
title: Knowledge-based proof planning
zbMATH Open document ID: 0939.68822
DOI: 10.1016/S0004-3702(99)00076-4
author: Erica Melis
author: Jörg H. Siekmann
published in: Artificial Intelligence
publication date: 2000-06-04T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1454255
zbMATH Keywords: theorem proving
zbMATH Keywords: planning
zbMATH Keywords: automated proof planning
zbMATH Keywords: meta-level reasoning
zbMATH Keywords: integrating constraint solvers
describes a project that uses: OTTER
describes a project that uses: EQP
describes a project that uses: Waldmeister
describes a project that uses: Prodigy
describes a project that uses: Bliksem
describes a project that uses: SETHEO
describes a project that uses: Nuprl
describes a project that uses: Analytica
describes a project that uses: Theorema
describes a project that uses: SPASS
describes a project that uses: LCF
describes a project that uses: PROTEIN
describes a project that uses: Omega-MKRP
MaRDI profile type: Publication
cites work: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
cites work: Q3880316
cites work: Theorem Proving via General Matings
cites work: Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
cites work: Q4227289
cites work: Q3957169
cites work: Q4217949
cites work: Ωmega: Towards a mathematical assistant
cites work: On Matrices with Connections
cites work: Non-resolution theorem proving
cites work: Q3352532
cites work: Challenge problems in elementary calculus
cites work: Computer proofs of limit theorems
cites work: Q3804239
cites work: Experiments with proof plans for induction
cites work: A resolution principle for constrained logics
cites work: Q3723721
cites work: Q4247688
cites work: Q4385443
cites work: STRIPS: A new approach to the application of theorem proving to problem solving
cites work: Q4499153
cites work: Theorem proving in cancellative abelian monoids (extended abstract)
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q5843404
cites work: Q4282537
cites work: Q3490996
cites work: Integrating computer algebra into proof planning
cites work: Q5525322
cites work: Inductive learning of search control rules for planning
cites work: SETHEO: A high-performance theorem prover
cites work: Q3915990
cites work: Q4139711
cites work: Q3940021
cites work: Q4692751
cites work: Solution of the Robbins problem
cites work: The Heine-Borel challenge problem. In honor of Woody Bledsoe
cites work: Q2767093
cites work: Q4499154
cites work: Analogy in inductive theorem proving
cites work: Q5839903
cites work: Q5559220
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q4530470
cites work: Planning in a hierarchy of abstraction spaces
cites work: Q3801492
cites work: The undecidability of the DA-unification problem
cites work: Computer science today. Recent trends and developments
cites work: Q5560258
cites work: Q4385449
cites work: Wie der Beweis der Vermutung von Baudet gefunden wurde

Knowledge-based proof planning (cites work)
cites work: Integrating planning and learning: the PRODIGY architecture

Knowledge-based proof planning (cites work)
cites work: Toward Mechanical Mathematics

Knowledge-based proof planning (cites work)
cites work: Extensions to the rippling-out tactic for guiding inductive proofs

Knowledge-based proof planning (full work available at URL)
full work available at URL: s0004-3702(99)00076-4

Knowledge-based proof planning (OpenAlex ID)
OpenAlex ID: W2042236049

Knowledge-based proof planning (Recommended article)
Recommended article: Q4530469
Similarity Score: 0.89061236
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Proof planning: A practical approach to mechanized reasoning in mathematics
Similarity Score: 0.889189
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Towards learning new methods in proof planning
Similarity Score: 0.8863456
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Constraint solving for proof planning
Similarity Score: 0.8856485
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Q3455569
Similarity Score: 0.8840034
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Q4518862
Similarity Score: 0.8828293
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Mathematical Knowledge Management
Similarity Score: 0.87679
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Q4808725
Similarity Score: 0.8762282
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: Q4499154
Similarity Score: 0.8753489
Recommender Run: Recommender Run 3

Knowledge-based proof planning (Recommended article)
Recommended article: A propositional theorem prover to solve planning and other problems
Similarity Score: 0.872382
Recommender Run: Recommender Run 3