4 papers
CoLF Logic Programming as Infinitary Proof Exploration
Zhibo Chen, Frank Pfenning
Logical Frameworks such as Automath [de Bruijn, 1968] or LF [Harper et al., 1993] were originally conceived as metalanguages for the specification of foundationally uncommitted ded…
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
Chenyang An, Zhibo Chen, Qihao Ye +6
Recent advances in Automated Theorem Proving have shown the effectiveness of leveraging a (large) language model that generates tactics (i.e. proof steps) to search through proof s…
A Logical Framework with Infinitary Terms
Zhibo Chen
Logical frameworks are successful in modeling proof systems. Recently, CoLF extended the logical framework LF to support higher-order rational terms that enable adequate encoding o…
A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
Zhibo Chen, Frank Pfenning
Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has…