The last part about preconditions/assumptions isn't specific to constructive logic; it's about backwards-chaining proof tactics; for example, applying the `ring` tactic in Coq will tell us to prove that the given structure is a ring (see the Errors section of https://coq.inria.fr/refman/addendum/ring.html#concrete-usag... )
The reason constructive logic is nice for this is the first part: we'll be given a counterexample, or a total algorithm for generating counterexamples, etc. (depending on the nature of the statement and its quantifiers). This is preferable to classical logics, where an automated prover might tell us "false", but we have no idea why.
The reason constructive logic is nice for this is the first part: we'll be given a counterexample, or a total algorithm for generating counterexamples, etc. (depending on the nature of the statement and its quantifiers). This is preferable to classical logics, where an automated prover might tell us "false", but we have no idea why.