<img align="left" src="icon/icon-readme.png" alt="icon">

@xamidi/pmGenerator

^{A tool meant to assist research on logical systems with detachment.}

<details><summary><h4 id="contents">Contents</h4> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture></summary>

1. Introduction
   1. Who is this for, serving which purpose?
   2. Why pmGenerator excels in “exploration”
   3. Target theorem proving and refinement
   4. Details
   5. Frege's calculus simplified by Łukasiewicz (CpCqp,CCpCqrCCpqCpr,CCNpNqCqp)
2. Navigation
3. Usage
   1. Commands
   2. Examples
4. Multi-node Computing
5. Custom Proof Systems
   1. Meredith's Axiom; 1-basis (CCCCCpqCNrNsrtCCtpCsp)
   2. Walsh's 1st Axiom; 1-basis (CCpCCNpqrCsCCNtCrtCpt)
   3. Walsh's 2nd Axiom; 1-basis (CpCCqCprCCNrCCNstqCsr)
   4. Walsh's 3rd Axiom; 1-basis (CpCCNqCCNrsCptCCtqCrq)
   5. Walsh's 4th Axiom; 1-basis (CpCCNqCCNrsCtqCCrtCrq)
   6. Walsh's 5th Axiom; 1-basis (CCpqCCCrCstCqCNsNpCps)
   7. Walsh's 6th Axiom; 1-basis (CCCpqCCCNrNsrtCCtpCsp)
   8. S5 (CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp)
6. Footnotes

</details>

Introduction

<p align="justify"> This research software is designed to compute and verify the logical consequences of given sets of axioms, which makes it an automated theorem prover (ATP). Albeit an unusual one: it is best suited to explore a given proof space in full detail. It supports classical, non-classical, and modal logic but is limited to proof systems built upon propositions and <a href="https://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a>. In a way, <em>pmGenerator</em> is to conventional ATPs what a microscope is to binoculars. This tool appears to be the <em>first</em> and so far <em>only one of its kind</em> for using a <a href="https://en.wikipedia.org/wiki/Condensed_detachment#D-notation">maximally condensed proof notation</a> to process completely <a href="https://en.wikipedia.org/wiki/Formal_proof">formal</a> and <a href="https://en.wikipedia.org/wiki/Constructive_proof">effective</a> proofs in user-defined systems, delivering <a href="https://github.com/xamidi/pmGenerator/discussions/4#literature">results of outstanding quality</a> where most provers fail. </p>

Who is this for, serving which purpose?

<p align="justify"> This project is aimed towards: </p> <ol> <li><div align="justify">People developing, exploring, or teaching proof systems. This includes philosophers, computer scientists, mathematicians, and even hobbyists using formal logic.</div> <ul><li><div align="justify">This tool can generate and process exhaustive and refined proof collections. It is highly beneficial when different researchers share these files for their systems of interest with others to download and build upon.</div></li></ul> </li> <li><div align="justify">Curious learners, including undergraduates, who can use this tool to handle and/or experiment with <em>Hilbert-style proofs</em>. Some universities require students to find such proofs in order to complete exercise sheets, for example.</div></li> <li><div align="justify">Motivated, capable individuals who are able to contribute to proof minimization challenges, like Metamath's <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt">pmproofs.txt</a> or my <a href="https://github.com/xamidi/pmGenerator/discussions/10">1-basis challenges</a>.</div></li> <li><div align="justify">Proof theorists interested in the structure and/or complexity of proofs.</div> <ul><li><div align="justify">Ideally including some proof complexity theorists interested in further discussing how such technology, data, and algorithms could be used to tackle the issue of Frege system complexity, or similar.</div></li></ul> </li> </ol> <p align="justify"> The above list should help you understand whether you are part of the intended audience but is not meant to be comprehensive. If you need help with technical issues, please post your questions in <a href="https://github.com/xamidi/pmGenerator/discussions">this project's forum</a>. </p>

Why pmGenerator excels in “exploration”

<p align="justify"> Unlike regular ATPs like Prover9 or Vampire, which are “goal-oriented” (you give them a target and they try to find a path), <em>pmGenerator</em> is “source-oriented”: It treats the axioms as a seed and <a href="https://en.wikipedia.org/wiki/Breadth-first_search">breadth-first searches</a> the space of all possible <a href="https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence">syntactic consequences</a> under extensive optimizations.^✾ </p> <p align="justify"> This makes it arguably the best tool for seeing the “<a href="https://en.wikipedia.org/wiki/Tree_(abstract_data_type)">tree</a>” of what a specific, user-defined system actually produces, rather than just checking whether a specific statement is provable. </p>

Target theorem proving and refinement

<p align="justify"> The program can perform additional operations on generated proof data. Once sufficient knowledge is available, <em>pmGenerator</em> can utilize it in order to convert proofs from (user-friendly) <a href="https://plato.stanford.edu/entries/natural-deduction/">natural deduction</a> into the explored system, thus revealing paths to specified targets, meaning <em>pmGenerator</em> can also be used “goal-oriented”. </p> <p align="justify"> Furthermore, such paths (or any user-provided proofs for that matter) can then be used to find more refined variants towards the same goals, thanks to <em>pmGenerator</em>'s proof compression capabilities. Thus <em>pmGenerator</em> can also work “path-oriented”, which — paired with its ability to generate exhaustive sets of minimal proofs — makes it an excellent tool for proof minimization with respect to a certain range of systems. </p>

Details

<p align="justify"> This tool can collect exhaustive sets of <a href="https://en.wikipedia.org/wiki/Condensed_detachment">condensed detachment</a> proofs in D-N-notation and has various functions to display, analyze and utilize them. It can, for example, be used to generate improved versions of Metamath's <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">“Shortest known proofs of the propositional calculus theorems from Principia Mathematica”</a> collection.<br> The D-rule combines <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)">unification</a> with modus ponens (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus <em>pmGenerator</em> covers all syntactic consequences within <a href="https://en.wikipedia.org/wiki/Hilbert_system">Hilbert systems</a> based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.<br> There is a <a href="https://github.com/xamidi/pmGenerator/discussions">discussion forum</a> for questions, ideas, challenges, and related information. Numerous use cases of the tool are exemplified, for example <em>proof parsing</em> under the <a href="https://github.com/xamidi/pmGenerator/discussions/2#proof-notation">Proof Notation</a> section of the <a href="https://github.com/xamidi/pmGenerator/discussions/2">“Minimal 1-bases for C-N propositional calculus”</a> proof minimization challenge. </p> <p align="justify"> Eligible for high-performance computing. If you have access to a powerful computer, you may use <em>pmGenerator</em> to further contribute to our knowledge regarding the <a href="https://en.wikipedia.org/wiki/Proof_complexity">complexity of proof systems</a>.^⚜ Progress that has already been made is exemplarily shown below. </p> <p align="justify"> ^✾<sub>Presupposing finitely many axiom schemas, this works by restricting the proof space such that only the most general suitable substitutions are utilized, leading to only finitely many proofs for any given number of proof steps. These proofs derive so-called <em>most general theorems</em>, each of which represents infinitely many formulas by substitution. Furthermore, exhaustive generation quickly becomes impractical for greater numbers of axiom schemas, so it may be useful to include only <em>relevant</em> ones and merge later. However, there is support for up to thirty-five axiom schemas named <code>1</code>, <code>2</code>, …, <code>9</code>, <code>a</code>, <code>b</code>, …, <code>z</code>. At this point, they can use only up to two nullary (<code>O</code>,<code>V</code>), five unary (<code>L</code>,<code>M</code>,<code>N</code>,<code>P</code>,<code>Z</code>), and twelve binar