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
Samiro DischerApr 9, 2024

An explanation of what axioms and mathematical proofs really are. With a reference to my tool that helps exploring some of them.

https://math.codidact.com/posts/290943/291261#answer-291261

#Logic #Axioms #Mathematics #ProofTheory #HilbertSystems #ModalLogic #Research #Software

What is the significance of the K-axiom in modal logic S5?

In normal modal logic S5, the K axiom says $\square (p \rightarrow q) \rightarrow (\square p \rightarrow \square q)$. First of all, is this an abuse...

Samiro DischerApr 7, 2024

Damn, another social network not containing anything about my research interests..

Looking for challengers: https://github.com/xamidi/pmGenerator/discussions/2

#ProofTheory #HilbertSystems #ProofMinimization #Research #Logic #Puzzle #Challenge

[Proof Minimization Challenge] Minimal 1-bases for C-N propositional calculus · xamidi pmGenerator · Discussion #2

There are seven minimal single axioms for propositional logic in terms of {→,¬}, namely Meredith's axiom and Walsh's six axioms. This thread is meant to allow anyone to participate in the challenge...

GitHub