Towards proof planning for M_^+

MaRDI QIDQ2844813zbMATH OpenFDO

Authors Serge Autexier, Carsten Schürmann

Publication date 19 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066104805103

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proof planning with multiple strategies
• On the comparison of proof planning systems: \(\lambda\)\textsc{clam}, \(\Omega\)\textsc{mega} and \textsc{IsaPlanner}
• scientific article; zbMATH DE number 1980936
• scientific article; zbMATH DE number 1303348
• scientific article; zbMATH DE number 1926636

Cited in

(3)

• Towards a formal proof system for \(\omega\)-rational expressions
• On the comparison of proof planning systems: \(\lambda\)\textsc{clam}, \(\Omega\)\textsc{mega} and \textsc{IsaPlanner}
• A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus

Describes a project that uses

Uses Software

• Twelf

This page was built for publication: Towards proof planning for \(\mathcal{M}_{\omega}^+\)

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