Replies: 1 comment 2 replies
-
|
[This comment relates to a reply in icecream17/Stuff/issues/2. It elaborates on Your Approach
From what followed, it seems you meant proof summaries (something like w2.txt).
Is this definition of a subproof meant to be inductive, e.g. in your "output of above command" is (example: old w2.txt as a full summary)Did I now understand correctly that you tried to tell me that you are merely suggesting an alternative proof summary compression method to
Due to lack of information I am not confident in understanding what your algorithm really does, but it seems very unlikely that you meant it in a way in which it has a greater effect than So let's first have a look at Current AlgorithmIdeally,✻ the number of non-trivial subproofs❈ in a proof summary equals the number of non-axiomatic formulas which it implicitly uses, e.g. the previous w2.txt (as you have figured out by putting it into full detail) uses n := 332 different steps and formulas that are non-trivial. ✻without a certain kind of redundancy, which can now be removed from A proof summary is always loaded as a full summary via For each of the n steps (of decreasing fundamental lengths) the current procedure tries all combinations of all the steps as inputs (as long as their combination would reduce the overall fundamental length of the step), and accept inputs if they preserve the conclusion to be a schema of its predecessor (usually itself; a formula is a schema of itself). Assuming only D-rules, there are 2 inputs, thus O(n²) such combinations exist. Since it does it for each of the n steps, it is already at least O(n³), but the algorithm doesn't end there. After it did all this, only one so-called round is finished, and it repeats until no further improvements are found. From observations it would seem plausible that there are O(log₂(n)) rounds✻, so the overall complexity of ✻There are cases constructible towards O(n) which are practically irrelevant. Asymptotic worst-case complexity here seems mostly irrelevant, as elaborated next. ComparisonIn conclusion, your method cannot have greater effects than the current method, unless your intended algorithm somehow introduces new formulas into the proof summary. Which it could do, considering it could try to modify subproofs that are not direct inputs of the D-rule it currently tries to improve while allowing new intermediate steps with new conclusions, but that'd have much higher complexity (still ignoring unification). Except when you limit your "subproofs" to not all actual subproofs but e.g. to only 6 (and thereby 4 indirect inputs with up to 2 formulas that may be newly introduced) — as by the non-inductive interpretation of your subproof definition. However, it should be possible to improve the performance of my algorithm, e.g. by remembering which formulas in which order are actually unifiable with which result (and thus not unifying a single combination more than once). Possibly you had another improvement in mind? But without sufficient and well-defined statements, I cannot verify that. Recent ImprovementsI didn't yet try much to make proof compression more efficient, but I made it optionally multi-threaded✻ in order to speed it up. ✻which, on the downside, may randomly increase the number of rounds it takes towards an optimal solution I don't know what you refer to by
since even when single-threaded, it usually took far below 1 hour for entire original proof summaries (often mere seconds for our best known 1-base summaries — worst was Of course, a proof summary can contain just one non-trivial proof or a billion of them, and they may all be part of just a single greatest superproof, or none of them. Thus the term "a single proof" is meaningless as a metric. The relevant metric here is the number of distinct subproofs (which should ideally be the number of formulas, i.e. ✻Simply using I recently implemented Note that compressing all proofs of theorems (i.e. not mere inferences) from your ~w2.mm (version 0951d88) together with all those from w2.txt (version 9e703cf) and several more from a new proof extraction yielded quite significant improvements. On InferencesI do not see how your approach would utilize inferences more than ✻Meaning their conclusions are unknown, and there is no information available on which kinds of inputs or premises are conclusion-preserving or even lead to parsable results. So here I suggest an informal notion of inferences similar to D-proof format, converted from some conditional proofs of your ~w2.mm: An inference relies on outside knowledge of the form of its premises in order to determine the form of its conclusion. Consequently, premises must be addressable individually, so I chose In case an approach means to actually take derivations/inferences as inputs somehow and we need to establish further grounds for that, we should open a corresponding discussion. |
Beta Was this translation helpful? Give feedback.
-
|
Right, I thought (For my estimation of hours, I think it was an impression from #2 (reply in thread) (the 898 million step w2), but that proof is particularly long and admittedly nothing really indicates such a thing except for the timing of the posts. Now that the proofs are much shorter my assumption is incorrect) I think the only way for the same strategy to find new things would be to expand the scope of usable statements like you did in #2 (comment) Time consuming ideaConsidering inferences with multiple hypotheses, I wonder if there's a way to I would be surprised if this finds anything new, (perhaps it may eke out a few bytes somewhere), but as an example: (Ok this very specific example is actually somewhat plausible, but nearly all attempts will be garbage) |
Beta Was this translation helpful? Give feedback.
-
I missed this one, you were right. As one can see from This was indeed a particularly bad case from using what Prover9 generated.
Right, this seems like the most efficient approach that could already introduce new conclusions to the proof summary. I guess next (probably for 1.2.2) I'll try an adjustable "modify all subproofs that are not direct inputs of the D-rule up to a certain distance" approach, for which one could specify a maximum distance d of each individual search, e.g. d = 0 would be equivalent to ✻Not counting potential replacements of root formulas by proper schemas. Each search can introduce up to 2d+1-1 new formulas. I think the ability to adapt to different summaries and available resources like this would be valuable. |
Beta Was this translation helpful? Give feedback.
-
This thread is meant to generally cover the topic of proof compression algorithms (such as
--transform -z) for formal condensed detachment proofs. This includes descriptions of current methods, related questions and ideas.You may still open dedicated threads for your particular issues under appropriate categories if you prefer.
Here I simply collect information as a baseline documentation on proof compression algorithms, to which you may contribute.
Contents
1.1 Your Approach — file types for pmGenerator, clarity in communication
1.2 Current Algorithm — informal description of
--transform -z, asymptotic complexity analysis1.3 Comparison — effectiveness and potential performance improvements
1.4 Recent Improvements — performance, multi-threading, proof minimization challenges and
--transform -b1.5 On Inferences — requirements and informal notion for inference rules
Addendum
There is a software library called Skeptik that focuses on compressing formal resolution proofs, and a corresponding Wikipedia article.
Beta Was this translation helpful? Give feedback.
All reactions