search

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

Use as library #68

Open XBagon opened 3 years ago

XBagon commented 3 years ago

Are there experiences or tips how to go about using this as a library? Currently struggling with lots of java.lang.NoClassDefFoundError exception, but this might be a problem on my end. The plan would be to directly use Problems constructed with the types from the parser library and then let Leo prove that and output if it succeeded.

lex-lex commented 3 years ago

Unfortunately, back then when implementation work on Leo-III started, this has not been a topic at all. I see today that this is actually quite a relevant use case. Sadly, I cannot give any experience with this.

However, NoClsasDefFoundError exceptions sound (to my ear at least) as if there are classpath issues in your project. Did you include the scala library (which Leo-III depends on)?