I don't understand the ∀-intro and ∃-elim rules.

I asked here - if you can help, please do!

https://cs.stackexchange.com/questions/173607/help-understanding-quantifier-rules-for-natural-deduction

#logic #maths #naturaldeduction

New: pmGenerator, since version 1.2.2, can
- compress Hilbert-style proofs via exhaustive search on user-provided proof data
- convert Fitch-style natural deduction proofs into any sufficiently explored Hilbert system

#Logic #HilbertSystems #NaturalDeduction #FormalMethods #ProofTheory #Mathematics

https://github.com/xamidi/pmGenerator/releases/tag/1.2.2

@emondb @hochstenbach @bblfish @josd

Hi Bruno,

I took a course & independent study on #AutomaticTheoremProving with David #Plaisted when he was still at #UIUC in 84–85. It was mostly about #ResolutionUnification & #NaturalDeduction provers but I was already on a different path by then as I had been working on #Peirce's & #SpencerBrown's versions of #LogicalGraphs in a computational vein since the late 60s. I'll discuss the differences that make a difference between those paradigms as we go.