exception in lltodk

[bodeveix]

Generating a proof term using -odk or -odkterm raises exceptions in lltodk. The error appears for example in the attached input:
pb.txt

zenon_modulo -itptp -odk pb.txt
Fatal error: exception File "lltodk.ml", line 289, characters 2-8: Assertion failed

zenon_modulo -itptp -odkterm pb.txt
(* PROOF-FOUND *)
Fatal error: exception File "lltodk.ml", line 1055, characters 2-8: Assertion failed

Furthermore, is it possible to add an extraction to lambdapi proof terms or proof scripts?

Thanks

[gburel]

It comes from the fact that in the file, there are only two axioms, and no goal.

The Dedukti output needs the file to contain exactly one goal, for instance by replacing the role of the second formula from axiom to negated_conjecture.

[gburel]

There is an output to lambdapi in the modulo_lp branch. It uses the same options as the Dedukti output in the modulo branch.

[fblanqui]

The syntax for the lp output (in the modulo_lp branch) is:

zenon_modulo -itptp -max-time 60s -odkterm -sig $sigmod file.p > $file.lp

where $sigmod is the lp module name where the signature is defined.
The signature must be written by hand or generated.
It may be possible to generate it by using https://github.com/Deducteam/ekstrakto.
Geoff Sutcliffe is working on having a TPTP tool doing this in the general case (ekstrakto is limited to CNF formulas currently).