scientific article; zbMATH DE number 1405440

MaRDI QIDQ4938413zbMATH OpenFDO

Authors Alan Bundy, Julian Richardson

Publication date 23 February 2000

zbMATH Keywords

\(\lambda\)Clam proof plannerhigher-order formulation of elliptic formulaehigher-order formulation of lists

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 3845031
• Proving Properties about Lists Using Containers
• Proving properties about functions on lists involving element tests
• scientific article; zbMATH DE number 4045132
• A short proof of Ellentuck's theorem
• scientific article; zbMATH DE number 4059363
• scientific article; zbMATH DE number 4055021
• Balancing Lists: A Proof Pearl

Cited in

(8)

• Graphical reasoning in compact closed categories for quantum computation
• Flexary connectives in Mizar
• Main problems of diagrammatic reasoning. I: The generalization problem
• Balancing Lists: A Proof Pearl
• Proving properties about functions on lists involving element tests
• Tentative experiments with ellipsis in Mizar
• What is a proof?
• Proving Properties about Lists Using Containers

Describes a project that uses

Uses Software

• Lambda-Clam

This page was built for publication:

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