A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas

DOI10.1016/S1571-0661(04)00285-3zbMath1268.68145OpenAlexW2087523912MaRDI QIDQ2841241

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

methodologyabstractionproof planningmatrix characterisations

Mathematics Subject Classification ID

Uses Software

• HOL
• Lambda-Clam

Cites Work

• A theory of abstraction
• Tableau methods of proof for modal logics
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• T-string unification: Unifying prefixes in non-classical proof methods
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas