Improvements on current unification implementation

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

BSD 3-Clause "New" or "Revised" License

42 stars 10 forks source link

Closed lex-lex closed 8 years ago

lex-lex commented 8 years ago

There are multiple things that can be improved:

In order to save iterations (orderings) over the unsolved eq list, we can just divide them in separate lists for flex-flex and not-flex-flex or similar
Does the partial substitution has to be applied every time or can be postpone it?
General inspection of the code for alternative data structures that seem more appropriate than List