CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2600

How does Sledgehammer translate lambda-abstractions to ATPs?

In Extending Sledgehammer with SMT solvers there is this claim:

Lambda-abstractions are rewritten to Turner combinators or transformed into explicit functions using lambda-abstractions.

The linked reference, Translating higher-order clauses to first-order clauses does not clarify how are this method synchronized. Do we use both of them always? Is one preferred to the other?

Upvotes: 2

Views: 54

Answers (1)

user1868607
user1868607

Reputation: 2600

According to mediatum.ub.tum.de/doc/1097834/1097834.pdf the choice of method is tailored for each prover.

Upvotes: 0

Related Questions