search

Deducteam / zenon_modulo

First-order automated theorem prover based on the tableau method
Other
12 stars 6 forks source link

exception in lltodk #4

Open bodeveix opened 1 year ago

bodeveix commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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).