9
$\begingroup$

Given some initial list of assumptions, I'd like to generate some true statements which follow from them without seeking a specific proof goal. I only need a small number of consequences from those assumptions, so there's no need to find every possible consequence.

Is there any proof assistant (or ATP) which has this functionality? And if not, is there some tactic or strategy within an assistant which I could modify to produce this result?

$\endgroup$
7
  • 2
    $\begingroup$ This is called forward proof search. I think you can easily write your own tactic for this functionality. $\endgroup$
    – Trebor
    Commented Mar 22, 2022 at 7:17
  • $\begingroup$ Related: proofassistants.stackexchange.com/questions/603/…. But that question isn’t necessarily asking for generation relative to a particular set of hypotheses. $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 12:23
  • $\begingroup$ This is a particularly vague question. One can always do trivial manipulations like apply symmetry to swap each side of an equality. But I assume you want to combine them in interesting ways. It depends a lot on what your theorems look like. Are they on DTT or FOL for example. Are they equalities, implications, conjunctions, or really complicated? $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 12:39
  • $\begingroup$ If you are working in FOL you may want to look at resolution theorem proving. The idea is that one starts with a bunch of assumptions as well as the negation of a conclusion. Then the algorithm repeatedly combines the formal (including axioms, assumptions, and the negated conclusion) until it gets a proof of false. $\endgroup$
    – Jason Rute
    Commented Mar 22, 2022 at 12:41
  • 1
    $\begingroup$ Am I allowed to generate 1 = 1, 2 = 2, 3 = 3, 4 = 4, ... etc? $\endgroup$ Commented Mar 22, 2022 at 16:54

1 Answer 1

4
$\begingroup$

This definitely falls under various active research projects to find interesting mathematics from a set of theorems. I can't point to a particular project per say, but let me mention why this is so hard.

The main reason it is so hard is that any naive algorithm which just starts combining statements is going to get into a combinatorial explosion of uninteresting mathematics.

For example, if my initial statements are A, B, C then I can form all sorts of things like A /\ B, A -> B, true, not not B.

Moreover if I have forall n m : Nat, n + m = m + n, then I can form 1 + 2 = 2 + 1, (1+1)*3 + 4 = 4 + (1+1)*3 and forall n m : Nat, n + 0 = 0 + n.

If I have A and A -> B, then I can form B, but often I really have A and A' -> B where A' doesn't exactly match A, so I first have to prove A' (or more likely if A' depends on a variable, I have to choose the right instance of that variable).

If I have forall a: A, f(a) = g(a), and I have some statement B about f(a), then I can rewrite any of the occurrences of f(a) in B, but it is hard to know which rewrites are interesting or useful for further downstream combinations.

I'm sure there is some work going back to the early days of AI of trying to just randomly mix axioms to get new math. And I imagine they used a lot of heuristics (probably to mixed success). I however, don't know any references.

Also, in FOL, resolution theorem provers first make all formulas into CNF so in the end you just have a list of disjunctive clauses. It is clear then what it means to combine two clauses. Indeed, an automatic theorem prover takes a bunch of clauses it wants to show are mutually inconsistent and just combines clauses using some heuristics until it reaches a proof of false. This cuts down on some redundancy, but there is still combinatorial explosion, and better heuristics can make huge gains in efficiency of ATPs.

If your goal is to create problems for say training an AI, then look at my answer to What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?.

And in general in AI for mathematics research there is always the question (with IMO no good answers so far) of can we program or train a computer to determine what "interesting" mathematics looks like?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.