Two questions

[TXLogic]

Howdy,

In checking this (rather baroque) formula

Code: Select all

((all x (P(x) -> (exists y (exists z (P(y) & A(x,y,z)))))) -> (all x (all y (all z ((z=x & (P(x) & x!=y)) -> (exists z (exists w (P(z) | A(y,z,w)))))))))

for theoremhood, Prover9 finds a proof but, instead of simply stopping and reporting "THEOREM PROVED" it appears to attempt to find another proof and, when it fails, it halts and outputs:

SEARCH FAILED

Exiting with 1 proof.

In this problem, I also get the following warning:

WARNING, because some of the denials share constants,
some of the denials or their descendents may be subsumed,
preventing the target number of proofs from being found.
The shared constants are: c2.

and I assume this has something to do with Prover9's unusual behavior in this case. The thing is, I'm not overtly *giving* Prover9 a "target number of proofs". I've searched the manual but have not found a way to tell Prover9 that one proof is all I want. Is there a way to do that, and also always to be guaranteed that Prover9 will output "THEOREM PROVED" in cases like the above? (I'm counting on finding that in the output for my purposes.)

My second question concerns Mace4, but I'd like to ask it here, as it is (for me) connected to the preceding question. (I'll ask it as well in the Mace4 forum if that would be better.) If you ask Mace4 to look for a countermodel for a formula that is a logical truth, if it detects the impossibility of doing so, it nonetheless tries to find one and also appears to ignore any attempt to set max_seconds, regardless of whether it is set in the input file or via the -t flag at the command line. The output *does* contain

NOTE: unsatisfiability detected on input.

But that's not much of a help if you aren't monitoring the output and can't kill the process manually. Is this a bug or a feature? And is there a way to get Mace4 to timeout in these cases?

Many thanks!

TXLogic

[mccune]

SEARCH FAILED

Exiting with 1 proof.

Short answer:

Code: Select all

clear(auto_denials).


(If you're using the GUI, it is in "Prover9 Options->Meta Options".)

Longer answer: After the formula is converted to clauses, Prover9
tries to be smart about what you want. The clauses are a Horn
set with more than one negative clause. A proof in this case must
use exactly one negative clause (this is not quite true), so it
thinks you want more than one proof.

My second question concerns Mace4, but I'd like to ask it here, as it is (for me) connected to the preceding question. (I'll ask it as well in the Mace4 forum if that would be better.) If you ask Mace4 to look for a countermodel for a formula that is a logical truth, if it detects the impossibility of doing so, it nonetheless tries to find one and also appears to ignore any attempt to set max_seconds, regardless of whether it is set in the input file or via the -t flag at the command line. The output *does* contain

NOTE: unsatisfiability detected on input.

But that's not much of a help if you aren't monitoring the output and can't kill the process manually. Is this a bug or a feature? And is there a way to get Mace4 to timeout in these cases?

The message "NOTE: unsatisfiability detected on input." applies to the particular
domain size that it's working on, so when that happens, it just goes to the next
size. If the formulas is a tautology, it will keep going. No problem here (though
the NOTE could be more informative).

The part about ignoring the time limit is a bug. It comes up on your example
above (and this is the first time I've seen it). The message "NOTE: unsatisfiability
detected on input", happens during a preprocessing step, before it starts searching
and checking the time limit. When it happens for every domain size (as in your
example), the time limit never gets checked. This will be fixed for the next
release. Until then, you can just limit the domain size (-N on the command line).

Or you can fix your own copy and recompile. Only one line needs to be changed:
Line 784 in mace4.src/msearch.c (version 2009-11A).
Change

Code: Select all

    rc = SEARCH_GO_NO_MODELS;  /* contradiction in initial state */


to

Code: Select all

    rc = check_time_memory();


This should work for earlier versions as well, but the line number might be different.

Bill

[TXLogic]

SEARCH FAILED

Exiting with 1 proof.

Short answer:

Code: Select all

clear(auto_denials).


(If you're using the GUI, it is in "Prover9 Options->Meta Options".)

Longer answer: After the formula is converted to clauses, Prover9
tries to be smart about what you want. The clauses are a Horn
set with more than one negative clause. A proof in this case must
use exactly one negative clause (this is not quite true), so it
thinks you want more than one proof.

Thanks very much for the speedy reply, explanation, and solution Bill, that does the trick. (Just FYI, I''m using the latest command line version, LADR-2009-11A).

My second question concerns Mace4, but I'd like to ask it here, as it is (for me) connected to the preceding question. (I'll ask it as well in the Mace4 forum if that would be better.) If you ask Mace4 to look for a countermodel for a formula that is a logical truth, if it detects the impossibility of doing so, it nonetheless tries to find one and also appears to ignore any attempt to set max_seconds, regardless of whether it is set in the input file or via the -t flag at the command line. The output *does* contain

NOTE: unsatisfiability detected on input.

But that's not much of a help if you aren't monitoring the output and can't kill the process manually. Is this a bug or a feature? And is there a way to get Mace4 to timeout in these cases?

The message "NOTE: unsatisfiability detected on input." applies to the particular
domain size that it's working on, so when that happens, it just goes to the next
size.

Ach, stupid of me. Obviously if it was smart enough to detect general unsatisfiability Mace4 wouldn't stupidly set off on a fruitless search for a model. I don't know what I was thinking.

If the formulas is a tautology, it will keep going. No problem here (though
the NOTE could be more informative).

The part about ignoring the time limit is a bug. It comes up on your example
above (and this is the first time I've seen it).

It seems to happen with any logical truth, even humble tautologies like (P | -P).

The message "NOTE: unsatisfiability
detected on input", happens during a preprocessing step, before it starts searching
and checking the time limit. When it happens for every domain size (as in your
example), the time limit never gets checked. This will be fixed for the next
release. Until then, you can just limit the domain size (-N on the command line).

Bill

Good to know, thanks! I'll just set a relatively high domain size for now.

TXLogic

[TXLogic]

...Or you can fix your own copy and recompile. Only one line needs to be changed:
Line 784 in mace4.src/msearch.c (version 2009-11A).
Change

Code: Select all

    rc = SEARCH_GO_NO_MODELS;  /* contradiction in initial state */


to

Code: Select all

    rc = check_time_memory();


This should work for earlier versions as well, but the line number might be different.

Bill

Whoops, I missed that part of your reply first time around. Just did this and recompiled. Bug squashed!

TXLogic