issues
search
Deducteam
/
zenon_modulo
First-order automated theorem prover based on the tableau method
Other
12
stars
6
forks
source link
Add SZS option and outputs
#39
Closed
gburel
closed
1 month ago
gburel
commented
1 month 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.)
add support for dune (#24)
change lp output to use the lambdapi-zenon library (#33)
lltolp.ml: fix requires for lambdapi-zenon library (#35)
rename dummy_var into negated_conjecture (#36)
fix dk output for GDV (#37)
Add SZS status in the output
Add -szs option Add SZS dataform markers around proofs when -szs is set Only print SZS status when -szs is set