exception in lltolp.ml

[geoffgeoffgeoff3]

it crashes on CNF problems, e.g., ... https://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ001-1.p

My command line is ...     zenon_modulo -p0 -itptp -olpterm -x arith   -max-time 30s -max-size 12G -sig LAMBDAPI_CONTEXT.Signature PUZ001-1.p ... and the barf is ...     Fatal error: exception File "lltolp.ml http://lltolp.ml", line 1060, characters 11-17: Assertion failed     Raised at file "list.ml http://list.ml", line 224, characters 10-25     Called from file "expr.ml http://expr.ml", line 249, characters 45-90

[gburel]

The problem here is that in PUZ001-1.p, the negated conjecture is not of the form "not something", but the -olpterm option expects it to be of that form because normally it is called from problems with a conjecture. Do you need the -olpterm option for this problem? I am not completely sure how to do in the case the negated conjecture is not a negation.

[geoffgeoffgeoff3]

Hi Guillaume,

The problem here is that in PUZ001-1.p, the negated conjecture is not of the form "not something", but the -olpterm option expects it to be of that form because normally it is called from problems with a conjecture.

What?!!? How do you guys ever prove anything like ... ~ sensible(donald_trump) ? That seems to be a fundamental flaw in lambdapi (or something).

Do you need the -olpterm option for this problem? I am not completely sure how to do in the case the negated conjecture is not a negation.

Vote Republican, I guess :-?

Cheers,

Geoff

-- Geoff Sutcliffe (Pronouns: words that refer to oneself/someone/something) Department of Computer Science, University of Miami, USA http://www.cs.miami.edu/~geoff

"My cat" is not a float. Every string should learn to swim. Despite the high cost of living, it's still surprisingly popular. Does superman wonder why we wear our overpants on the inside?

[gburel]

Fortunately, Zenon Modulo can prove ~ sensible(donald_trump) because it will show that the negated conjecture ~ ~ sensible(donald_trump) is inconsistent.

In fact, Zenon Modulo can prove negated conjectures even if they do not begin with ~. It can even produce a Lambdapi proof in that case, with the option -olp (although I didn't check that it works well).

The problem comes from the -olpterm option which assumes that one tries to prove a conjecture, so that it outputs a proof term for that conjecture.

One could probably output something also in the case we have a negated conjecture that is not a negation, but I am not sure where it could be useful. To my knowledge, -olpterm is only used in Ekstrakto and GDV, to prove conjectures.

In which context did you tried to use it? Is it within GDV?

[geoffgeoffgeoff3]

Hi Guillaume,

Fortunately, Zenon Modulo can prove ~ sensible(donald_trump) because it will show that the negated conjecture ~ ~ sensible(donald_trump) is inconsistent.

:-)

In fact, Zenon Modulo can prove negated conjectures even if they do not begin with ~. It can even produce a Lambdapi proof in that case, with the option -olp (although I didn't check that it works well).

The problem comes from the -olpterm option which assumes that one tries to prove a conjecture, so that it outputs a proof term for that conjecture.

Yeah. My default configuration uses -olpterm ... zenon_modulo -p0 -itptp -olpterm -x arith $NNPPArg $LeafArg -max-time $1s -max-size 12G -sig LAMBDAPI_CONTEXT.Signature $PROBLEMFILE > $SOLUTIONFILE

One could probably output something also in the case we have a negated conjecture that is not a negation, but I am not sure where it could be useful. To my knowledge, -olpterm is only used in Ekstrakto and GDV, to prove conjectures.

Even in the GDV context it can be possible that the "negated conjecture that is not a negation". The negation or lack thereof should not hamper the proof processes.

In which context did you tried to use it? Is it within GDV?

I was just trying to prove ... https://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ001-1.p

Cheers,

Geoff

-- Geoff Sutcliffe (Pronouns: words that refer to oneself/someone/something) Department of Computer Science, University of Miami, USA http://www.cs.miami.edu/~geoff

"My cat" is not a float. Every string should learn to swim. Despite the high cost of living, it's still surprisingly popular. Does superman wonder why we wear our overpants on the inside?