> 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't be able to check your context for an inconsistency. > What did you mean by "Since this is very quickly undecidable to check > the context for consistency" ? Did you mean that Why3 cannot check the > consistency of the context ? Yes, as I just explained. First-order logic is not decidable. > 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 ? No, it simply means that the prover was not able to prove it. For instance, the prover may give up at some point, having exhausted all its heuristics. SMT provers do that. Some other provers (such as E-prover, or SPASS) may be refutationaly complete: if there is a proof, they'll find it (possibly after a very, very long time, though); but they may loop forever if there is not. Again, FOL is not decidable, so there isn't much more you can do. Hope this helps, -- Jean-Christophe _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
