search

benbrastmckie / ModelChecker

A hyperintensional theorem prover for counterfactual conditional, modal, constitutive explanatory, relevance, and extensional operators.
https://pypi.org/project/model-checker/
5 stars 0 forks source link

Declarations #8

Closed benbrastmckie closed 6 months ago

benbrastmckie commented 6 months ago

I had thought it would be a good idea to introduce as few declarations as need be (thinking of these as the primitives). In particular, possible, verify, and falsify. The other declarations of parthood, world, and alternative were added to ease the extraction of information from Z3 models. Their interpretation was then constrained to accord with the defined notions of is_part_of, is_world, and is_alternative. However, having succeeded in eliminating these extra declarations, the models seem to fair somewhat worse (they don't seem to generate the alternative worlds that they should) though seem to run much faster. I have left the branch remove_alt for further investigation between these strategies. It may be worth creating a new branch which adds all the declarations as currently master does not include reference to the declarations world or parthood. It may also worth running these different branches against benchmarks to get a better sense of how they compare.

benbrastmckie commented 6 months ago

I merged the min_declare branch without issues and was able to remove the declaration of alternative with noticeable decrease in computation time for cf_excl_mid.py. Without doing benchmarks I think it is safe to conclude that adding extra declarations can slow down Z3.