search

nomeata / incredible

The Incredible Proof Machine
MIT License
359 stars 36 forks source link

yay, I broke it :-) #61

Closed mohrm closed 8 years ago

mohrm commented 8 years ago

I just discovered that via the export function you can create a block with which you can solve any task. Just goto (or create) a task with the goal assumption "A", and make a rule from only the goal assumption. I think, this was not intended...

mohrm commented 8 years ago

Since you cannot export a rule as soon as you select a goal (from my feeling such a rule which then only has inputs and no outputs would be okay, especially to workaround issues like #60), I suspect that assumptions and goals were confused here...maybe an UI issue?

nomeata commented 8 years ago

Well, you can only proof “A” from that, not anything. But yes, I forgot to remove assumptions from the graph before passing them to the rule generation.

mohrm commented 8 years ago

true, the trick is not as universal as I initially thought. But you can apply it to any task: Make a custom task with the goal you want to prove as assumption, select that assumption, export and prove your goal with it.