A semantics for proof plans with applications to interactive proof planning

DOI10.1007/3-540-36078-6_23MaRDI QIDQ4428310zbMATH OpenFDO

Authors Julian Richardson

Publication date 15 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2514/25140337.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 827983
• Towards learning new methods in proof planning
• Proof planning with multiple strategies
• scientific article; zbMATH DE number 1748584
• Artificial Intelligence and Symbolic Computation

Cited in

(16)

• Proof planning for strategy development
• Constraint solving for proof planning
• Co-localization, co-support and local homology
• Crystal: Integrating structured queries into a tactic language
• Towards learning new methods in proof planning
• Generating plans from proofs. The interpolation-based approach to query reformulation
• A proof-planning framework with explicit abstractions based on indexed formulas
• Towards proof planning for \(\mathcal{M}_{\omega}^+\)
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• Integrating constraint solving into proof planning
• scientific article; zbMATH DE number 827983 (Why is no real title available?)
• Plans and planning in mathematical proofs
• Automated Deduction – CADE-20
• Artificial Intelligence and Symbolic Computation
• Experiments with proof plans for induction
• Proof systems for planning under 0-approximation semantics

Describes a project that uses

Uses Software

• Stratego

This page was built for publication: A semantics for proof plans with applications to interactive proof planning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4428310)