Dear Why3 Developers,
Thanks for your response to my last two questions. Now I have one more
question regarding to your response:
> For an automated theorem prover to return "Invalid", it would mean that
> this prover has checked the logical context to be free of inconsistency
> (even a goal suc
Hi Ziqing,
> If I get an "Unknown" for a goal, does it mean that the goal is invalid if
> I can separately prove the context is consistent ?
I am not sure if this may be of help, but given a goal `P`, instead of
trying to get `Invalid` from it, you could try to get `Valid` for its
negation `not
> It makes sense to me that if context is unsatisfiable any goal is valid.
> But how to let Why3 check the context ?
You could try to prove "false" with your context (i.e. replace your goal
with false).
But ATPs are necessarily incomplete (there are at best, refutationaly
complete). So they won
Hello,
Ziqing Luo writes:
> Thanks for your response to my last two questions. Now I have one more
> question regarding to your response:
>
>> For an automated theorem prover to return "Invalid", it would mean that
>> this prover has checked the logical context to be free of inconsistency
>> (ev
Hi,
Le 11/09/2017 à 16:55, Ziqing Luo a écrit :
> But how to let Why3 check the context ?
Let me add a few things about that question.
1) Indeed, Why3 does not offer any *automatic* process to check if the
context is consistent. As said by others before, there is no way for an
automatic prover
