Knowledge-based proof planning
From MaRDI portal
Publication:1978469
DOI10.1016/S0004-3702(99)00076-4zbMATH Open0939.68822OpenAlexW2042236049MaRDI QIDQ1978469FDOQ1978469
Authors: 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
Recommendations
- scientific article; zbMATH DE number 1748584
- Proof planning: A practical approach to mechanized reasoning in mathematics
- Towards learning new methods in proof planning
- Constraint solving for proof planning
- Knowledge-based programs as plans. The complexity of plan verification
- scientific article; zbMATH DE number 1538007
- Mathematical Knowledge Management
- scientific article; zbMATH DE number 2090054
- scientific article; zbMATH DE number 1497744
- A propositional theorem prover to solve planning and other problems
Cites Work
- Edinburgh LCF. A mechanized logic of computation
- \(\Omega\)\textsc{mega}: towards a mathematical assistant
- STRIPS: A new approach to the application of theorem proving to problem solving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- SETHEO: A high-performance theorem prover
- Solution of the Robbins problem
- Computer science today. Recent trends and developments
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorem proving in cancellative abelian monoids (extended abstract)
- Title not available (Why is that?)
- Analogy in inductive theorem proving
- The undecidability of the DA-unification problem
- Title not available (Why is that?)
- Toward Mechanical Mathematics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Experiments with proof plans for induction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorem Proving via General Matings
- Non-resolution theorem proving
- On Matrices with Connections
- Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
- Integrating computer algebra into proof planning
- Planning in a hierarchy of abstraction spaces
- Title not available (Why is that?)
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- Extensions to the rippling-out tactic for guiding inductive proofs
- Computer proofs of limit theorems
- Integrating planning and learning: the PRODIGY architecture
- Title not available (Why is that?)
- Title not available (Why is that?)
- Challenge problems in elementary calculus
- Wie der Beweis der Vermutung von Baudet gefunden wurde
- A resolution principle for constrained logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Inductive learning of search control rules for planning
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Heine-Borel challenge problem. In honor of Woody Bledsoe
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (17)
- Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
- A framework for using knowledge in tableau proofs
- Decision planning knowledge representation framework: A case-study
- Title not available (Why is that?)
- Mechanizing Mathematical Reasoning
- Towards finding longer proofs
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Computer supported mathematics with \(\Omega\)MEGA
- Agenda control for heterogeneous reasoners
- Comparing approaches to the exploration of the domain of residue classes.
- A proof-planning framework with explicit abstractions based on indexed formulas
- Constraint solving for proof planning
- Title not available (Why is that?)
- Proof planning: A practical approach to mechanized reasoning in mathematics
- Mathematical Knowledge Management
- Proof planning with multiple strategies
- An integral theorem prover and the role of proof planning
Uses Software
This page was built for publication: Knowledge-based proof planning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1978469)
