A proof-planning framework with explicit abstractions based on indexed formulas

DOI10.1016/S1571-0661(04)00285-3MaRDI QIDQ2841241zbMATH OpenOpenAlexFDO

Authors Serge Autexier

Publication date 24 July 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)00285-3

zbMATH Keywords

abstractionmatrix characterisationsmethodologyproof planning

Mathematics Subject Classification ID

Recommendations

• Proof planning with multiple strategies
• scientific article; zbMATH DE number 1980936
• Knowledge-based proof planning
• scientific article; zbMATH DE number 1748584
• Artificial Intelligence and Symbolic Computation

Cites work

• A theory of abstraction
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• Specification of abstract data types
• T-string unification: unifying prefixes in non-classical proof methods
• Tableau methods of proof for modal logics

Cited in

(1)

• Generating plans from proofs. The interpolation-based approach to query reformulation

Describes a project that uses

Uses Software

• HOL
• Lambda-Clam

This page was built for publication: A proof-planning framework with explicit abstractions based on indexed formulas

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