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

Implicitly quantified variables of a clause #28

Open lex-lex opened 8 years ago

lex-lex commented 8 years ago

...are currently calculated each time a clause is created (from the sequence of contained literals). This is, of course, in many cases too inefficient as we know the variables upon creation of the clause. Suggesstion: Add a optional parameter to the Clause constructor that accepts the argument as the implicitly quantified variables. If its not given, they are calculated as usual.