epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Substitution param inference Iff #137

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

This will be either discarded or redone in context of #144.

Following a discussion with @vkuncak, this needs to be done more carefully while identifying what we allow. Specifically, idempotence for sets of formulae can encode graph colouring and introduce NP-completeness.