Proof Assistant Questions

Stream: computer science

[Ender]

The BNF derived parse tree of a proof is like a deep structure in generative grammar, I think. Can I use generative grammars for proof search? Feel free to correct my misunderstanding. This would entail exploring the possibility space of proofs instead of proving one theorem in particular. 

• The closest I can find to a proof search algorithm that uses rewriting or replacement rules would seem to be proof search algorithms using sequent calculus. 

• Is Lambek calculus at all related to this concept? Lambek calculus and the Lambek grammar keep coming up in my searches because I am interested in generative grammars.

What are the building blocks of a proof assistant?  (Proof calculus, logic calculus?)

What is the difference between a proof calculus and logic calculus? 

What does it mean for a calculus to be uninterpreted?