Fix TPTP syntax of annotations

Deducteam / zenon_modulo

First-order automated theorem prover based on the tableau method

Other

12 stars 6 forks source link

Closed gburel closed 3 months ago

gburel commented 3 months ago

Accept integers as formula names
Fix bug where a free variable was printed in the proof term.
More close to real TPTP syntax of annotations. (Still missing: formula_data, and semantic verification.)