Knowledge-based proof planning
From MaRDI portal
Publication:1978469
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
- \(\Omega\)\textsc{mega}: towards a mathematical assistant
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- A Machine-Oriented Logic Based on the Resolution Principle
- A resolution principle for constrained logics
- Analogy in inductive theorem proving
- Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
- Challenge problems in elementary calculus
- Computer proofs of limit theorems
- Computer science today. Recent trends and developments
- Edinburgh LCF. A mechanized logic of computation
- Experiments with proof plans for induction
- Extensions to the rippling-out tactic for guiding inductive proofs
- scientific article; zbMATH DE number 1696826 (Why is no real title available?)
- scientific article; zbMATH DE number 4203762 (Why is no real title available?)
- scientific article; zbMATH DE number 4164178 (Why is no real title available?)
- scientific article; zbMATH DE number 3954298 (Why is no real title available?)
- scientific article; zbMATH DE number 4068801 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 3684929 (Why is no real title available?)
- scientific article; zbMATH DE number 3727583 (Why is no real title available?)
- scientific article; zbMATH DE number 3756774 (Why is no real title available?)
- scientific article; zbMATH DE number 3777779 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 1222425 (Why is no real title available?)
- scientific article; zbMATH DE number 1254246 (Why is no real title available?)
- scientific article; zbMATH DE number 1302386 (Why is no real title available?)
- scientific article; zbMATH DE number 517013 (Why is no real title available?)
- scientific article; zbMATH DE number 1140678 (Why is no real title available?)
- scientific article; zbMATH DE number 1140683 (Why is no real title available?)
- scientific article; zbMATH DE number 1497743 (Why is no real title available?)
- scientific article; zbMATH DE number 1497744 (Why is no real title available?)
- scientific article; zbMATH DE number 1748585 (Why is no real title available?)
- scientific article; zbMATH DE number 194754 (Why is no real title available?)
- scientific article; zbMATH DE number 3237808 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
- scientific article; zbMATH DE number 3099224 (Why is no real title available?)
- scientific article; zbMATH DE number 3104649 (Why is no real title available?)
- Inductive learning of search control rules for planning
- Integrating computer algebra into proof planning
- Integrating planning and learning: the PRODIGY architecture
- Non-resolution theorem proving
- On Matrices with Connections
- Planning in a hierarchy of abstraction spaces
- SETHEO: A high-performance theorem prover
- Solution of the Robbins problem
- STRIPS: A new approach to the application of theorem proving to problem solving
- The Heine-Borel challenge problem. In honor of Woody Bledsoe
- The undecidability of the DA-unification problem
- Theorem proving in cancellative abelian monoids (extended abstract)
- Theorem Proving via General Matings
- Toward Mechanical Mathematics
- Wie der Beweis der Vermutung von Baudet gefunden wurde
Cited in
(18)- An integral theorem prover and the role of proof planning
- Decision planning knowledge representation framework: A case-study
- Comparing approaches to the exploration of the domain of residue classes.
- Agenda control for heterogeneous reasoners
- Constraint solving for proof planning
- Towards finding longer proofs
- Proof planning with multiple strategies
- Proof planning: A practical approach to mechanized reasoning in mathematics
- A proof-planning framework with explicit abstractions based on indexed formulas
- scientific article; zbMATH DE number 4072438 (Why is no real title available?)
- scientific article; zbMATH DE number 1748584 (Why is no real title available?)
- A framework for using knowledge in tableau proofs
- Mechanizing Mathematical Reasoning
- Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
- Mathematical Knowledge Management
- Automation of Boolos' Curious Inference in Isabelle/HOL
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Computer supported mathematics with MEGA
Describes a project that uses
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)
