scientific article; zbMATH DE number 1301855

MaRDI QIDQ4247078zbMATH OpenFDO

Authors Karsten Konrad

Publication date 16 June 1999

zbMATH Keywords

automated higher-order theorem proverextensional higher-order tableaux calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1552534
• Satallax: An Automatic Higher-Order Prover
• HyperS tableaux -- heuristic hyper tableaux
• Partheo: A high-performance parallel theorem prover

Cited in

(9)

• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• HOT
• Analytic tableaux for higher-order logic with choice
• scientific article; zbMATH DE number 1552534 (Why is no real title available?)
• Analytic tableaux for higher-order logic with choice
• Superposition with lambdas
• Superposition with lambdas
• The Watson theorem prover
• TPS: A hybrid automatic-interactive system for developing proofs

Describes a project that uses

Uses Software

• TPS
• Oz
• leanTAP

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 Q4247078)