Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

What is/how powerful is the logic used by Imandra #13

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

Comments

@Bronsa
Copy link
Member

commented Sep 4, 2019

From a proof-theoretic perspective, Imandra's logic is effectively a typed version of PRA (Skolem's Primitive Recursive Arithmetic) extended with Transfinite Induction up to the ordinal epsilon_0.
It's a multisorted first-order logic, but Imandra has various niceties that allow it to handle a 'specializable' fragment of Higher-Order Logic

Since in Imandra everything is a program, all judgments are computational and because we live in a quantifier-free world of discrete combinatorial structures, we can admit classical logic and still obtain results that are constructively valid

In Imandra's logic all functions must be total and terminating, extension to the logic are accepted via defining new types or functions validated by Imandra's definitional principle, which analyses definitions to ensure they are admissible, to ensure that any extension by definitions is a conservative extension.

For exception-raising functions like List.hd, List.tl and /, Imandra has a semantics that under-specifies them, allowing them to take on any value in their 'exceptional' cases

@Bronsa Bronsa added the doc topic label Sep 4, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.