Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs.
Albert Q. JiangSean WelleckJin Peng ZhouWenda LiJiacheng LiuMateja JamnikTimothée LacroixYuhuai WuGuillaume LamplePublished in: CoRR (2022)
Keyphrases
- theorem prover
- theorem proving
- automated theorem proving
- automated reasoning
- first order logic
- formal proof
- inference rules
- term rewriting
- automated deduction
- computer algebra
- proof search
- formal semantics
- higher order logic
- natural deduction
- proof planning
- formal model
- formal and informal learning
- predicate calculus
- training data
- reasoning tasks
- expert systems