Automatic theorem proving and OTTER

MaRDI QIDQ2721238zbMATH OpenFDO

Authors José Alfredo Amor Montaño, Favio E. Miranda Perea

Publication date 1 July 2001

zbMATH Keywords

classical logicfinitely described theorypredicate language with equality

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited in

(13)

• OTTER
• OTTER experiments in a system of combinatory logic
• KARNAK an automated theorem prover for PPC
• scientific article; zbMATH DE number 1566502 (Why is no real title available?)
• Hyperincursive proof theory
• scientific article; zbMATH DE number 4033134 (Why is no real title available?)
• scientific article; zbMATH DE number 4043814 (Why is no real title available?)
• A mechanical proof of the Church-Rosser theorem
• scientific article; zbMATH DE number 158462 (Why is no real title available?)
• scientific article; zbMATH DE number 1140676 (Why is no real title available?)
• scientific article; zbMATH DE number 1761418 (Why is no real title available?)
• The t‐variable method in gentzen‐style automatic theorem proving
• Mathematical induction in Otter-lambda

This page was built for publication: Automatic theorem proving and OTTER

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