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

Merged new parser into Leo-III #66

Closed lex-lex closed 3 years ago

lex-lex commented 3 years ago

A hand-written TPTP parser was created and integrated into Leo-III. This one outperforms the old ANTLR-based one by magnitudes.