0

Wondering how a proof assistant such as Coq proves forall or exists. For example:

enter image description here

Three aspects:

  1. If you were to give it a huge set of items like a million, wondering if it would actually iterate through it 3x and compare all the values to prove the transitive relation holds.
  2. If not, then wondering if it doesn't even need such an "example" group, and instead it can just work on the definition itself, and how that would work.
  3. Or is this proof definition defining a set in advance, so it provably has the transitive relation from the start. If so, how that works.

Say you want to prove some set has the transitive property, wondering how the proof assistant goes about proving that, how it works under the hood.

  • I think you're in the wrong place. Did you mean to post this on math.stackexchange.com? – Robert Harvey May 3 '18 at 20:51
  • I posted it there but they voted to close it as off topic lol. It is sort of about programming since it's the implementation of the assistant. – Lance Pollard May 3 '18 at 20:52
  • Well, it doesn't seem to have much to do with Software Engineering. We're not really in the business of dissecting or reverse-engineering corporate software. – Robert Harvey May 3 '18 at 20:52
  • 1
    @RobertHarvey: it is a question about an algorithm, which makes it IMHO on topic here - at least, formally. However, not sure if our community has many experts for this very specific kind of algorithmic domain. – Doc Brown May 3 '18 at 20:55
  • 2
    I agree it is an algorithm question, and probably one of the more common ones about this type of tool. – Frank Hileman May 3 '18 at 22:42
7

In general, #2. The language takes the declared initial states and uses Boolean logic transitions to make sure that there are no contradictions in the interactions between all of the rules defined. Pretty much like any philosophy or math major would do when proving logical assertions, but in an automated (and less error prone) manner.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.