Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

How to express forall_exists in Imandra #11

Open
Bronsa opened this issue Sep 4, 2019 · 0 comments
Open

How to express forall_exists in Imandra #11

Bronsa opened this issue Sep 4, 2019 · 0 comments
Labels
doc topic

Comments

@Bronsa
Copy link
Member

Bronsa commented Sep 4, 2019 •
edited by mattjbray
Loading

Imandra's logic is purely computational, without existential quantifiers.
In order to prove forall x exists y s.t. phi(x,y), you define a computable witnessing Skolem function f(x) and use Imandra to prove forall x (phi(x, f(x)))
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
doc topic
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Bronsa