This repository contains two Rumm tactics for finding Metamath proofs in classical propositional logic. For now, it supports statements containing only material implication -> and negation -., but this might be expanded in the future.
It can find proofs of theorems with no hypotheses, or rules of inferences that have at most one hypothesis.
Content of this repository:
-
file1.mm: Auxiliary theorems and variables necessary to run solver1.rmm.
-
file2.mm: Auxiliary theorems and variables necessary to run solver2.rmm.
-
solver1.rmm: The first tactics. It has faster execution time, but it often produces longer proofs than the second version.
-
solver2.rmm: The second tactics. It produces shorter proofs in general, but the execution time is slower. Furthermore, all proofs generated by this tactics use only the
->and-.symbols. -
output1.txt: Output produced by solver1.rmm. This file contains the Metamath proofs of the goal statements generated by solver1.rmm.
-
output2.txt: Output produced by solver2.rmm. This file contains the Metamath proofs of the goal statements generated by solver2.rmm. Notice that this file is much larger than the first one.
-
set.mm: Untouched version of set.mm dating back to 4 January 2025. For compatibility reasons, it is recommended to keep using this version of set.mm, rather than an updated one.
To save running time, it is highly recommended to print the output to a file rather than the console. Both tactics should take a few seconds to produce all test proofs.