A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems

DOI10.2168/LMCS-7(1:6)2011zbMath1218.03010arXiv1012.3372MaRDI QIDQ3003307

Stéphane Lengrand, James McKinna, Roy Dyckhoff

Publication date: 26 May 2011

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1012.3372

zbMATH Keywords

sequent calculustype theoryPTSstrong normalisationmetavariablesproof-searchinteractive proof construction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Related Items (1)

Practical Proof Search for Coq by Type Inhabitation

Uses Software

• Coq
• HOL
• Automath
• LEGO

This page was built for publication: A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems