search

nick8325 / equinox

Paradox model finder and equinox theorem prover for first-order logic.
MIT License
19 stars 4 forks source link

paradox feature request: specify minimum and maximum domain cardinality #6

Open jessealama opened 11 years ago

jessealama commented 11 years ago

When searching for models with paradox, I find that I often want to compare different models of a theory, specifically, models of different cardinalities. As it stands, though, this appears not to be possible with paradox without either (1) modifying the paradox sources, or (2) adding a premise to the theory saying that the domain size is at least N. Both of these are rather awkward; it seems better to me to support a minimum (and perhaps also maximum) domain size as a commandline parameter for paradox, similar to -n and -N for mace4.

nick8325 commented 11 years ago

This would be nice, I agree! I will talk to Koen to see how to go about implementing it.