scientific article; zbMATH DE number 65530

MaRDI QIDQ4012878zbMATH OpenFDO

Authors Leen Helmink, René Ahn

Publication date 27 September 1992

zbMATH Keywords

Automath languagesgoal-directed proofproof construction in Generalized Type Systemsresolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Structure of proofs (03F07) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• scientific article; zbMATH DE number 1614692
• Goal-directed proof theory
• Automated proof construction in type theory using resolution
• scientific article; zbMATH DE number 1215502
• A Complete Proof Synthesis Method for the Cube of Type Systems

Cited in

(6)

• Automated proof construction in type theory using resolution
• TPS: A theorem-proving system for classical type theory
• scientific article; zbMATH DE number 1614692 (Why is no real title available?)
• scientific article; zbMATH DE number 683355 (Why is no real title available?)
• scientific article; zbMATH DE number 1552510 (Why is no real title available?)
• Checking algorithms for Pure Type Systems

Describes a project that uses

Uses Software

• Nuprl

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