Optimization of pi-base deduction engine

[prabau]

When doing a search in pi-base, the user gets either a list of known examples that match the query, or a chain of theorems providing a proof that the query cannot be satisfied. Sometimes the list of theorems justifying a proof can become quite long.

As discussed in our Community meeting of June 2, we were wondering what algorithm is used by the underlying deduction engine (breadth first, ... ?). Also, sometimes there could be multiple derivations of a proof in the implication graph. Is it possible that the chosen result is not always optimal (in terms of number of theorems used, or in terms of extraneous branches that do not need to be displayed for example) and if so, how hard would it be to optimize things?

Requesting input from @jamesdabbs.

[StevenClontz]

The other bit of context: we were wondering this partly so we can decide on the data side what policies we want to make about redundant theorems. Right now we're minimizing these but we wonder if allowing some common implications would help improve the output of pi-Base's automated dedications.

[jamesdabbs]

Yeah, for each space, we broadly

• start with a queue of all theorems about the asserted traits
• repeatedly try to apply them to deduce new traits
• if we succeed, re-enqueue theorems related to the new property

There certainly may be more clever approaches we could take. Without a more clever approach, I'd assume it's computationally infeasible to try to find the minimal-size proof for every deducible trait globally. It seems more tractable to me to have a "find alternative proofs / simplify proof" view when looking at a particular trait.