[opentheory-users] Print unsatisfied assumptions

Joe Leslie-Hurd joe at gilith.com
Tue May 10 06:08:59 UTC 2016


I can't think of any way of persuading the existing opentheory tool to
give you this functionality, except in the way you describe.

I'd be happy to add the functionality to the tool, but it may take a
little while.

As a matter of curiosity, what is your use-case for this functionality?

Cheers,

Joe

On Sun, May 8, 2016 at 7:09 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> Hi,
>
> How can I get the unsatisfied assumptions of a theory in article format?
>
> I know about the info --assumptions option, but it prints _all_ assumptions,
> including the satisfied ones.
>
> The only way I have found so far to do it is to create a fake package that
> imports all the required packages and print the assumptions of that. But
> it's rather cumbersome to do so. Especially because importing the required
> packages also means figuring out all their dependencies and recreating them
> as blocks within the theory file in the right order.
>
> I know the opentheory tool knows how to calculate just the unsatisfied
> assumptions. How can I get them out of it?
>
> Cheers,
> Ramana
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



More information about the opentheory-users mailing list