TariqSep 21, 2025

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

Samiro DischerJun 11, 2025

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

Release pmGenerator 1.2 (patch 2) · xamidi/pmGenerator

pmGenerator-1.2.2-win.7z contains Windows binaries only. Compiled by GCC 11.3.0, binaries from winlibs-x86_64-posix-seh-gcc-11.3.0-llvm-14.0.3-mingw-w64msvcrt-10.0.0-r3 Used oneTBB 2021.9.0-1, lib...

GitHub
Show threadJon AwbreyFeb 5, 2023

@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.