The Imandra Automated Reasoning System (system description). (arXiv:2004.10263v1 [cs.LO])

We describe Imandra, a modern computational logic theorem prover designed to
bridge the gap between decision procedures such as SMT, semi-automatic
inductive provers of the Boyer-Moore family like ACL2, and interactive proof
assistants for typed higher-order logics. Imandra’s logic is computational,
based on a pure subset of OCaml in which all functions are terminating, with
restrictions on types and higher-order functions that allow conjectures to be
translated into multi-sorted first-order logic with theories, including
arithmetic and datatypes. Imandra has novel features supporting large-scale
industrial applications, including a seamless integration of bounded and
unbounded verification, first-class computable counterexamples, efficiently
executable models and a cloud-native architecture supporting live multiuser

The core reasoning mechanisms of Imandra are (i) a semi-complete procedure
for finding models of formulas in the logic mentioned above, centered around
the lazy expansion of recursive functions, and (ii) an inductive waterfall and
simplifier which “lifts” many Boyer-Moore ideas to our typed higher-order

These mechanisms are tightly integrated and subject to many forms of user
control. Imandra’s user interfaces include an interactive toplevel, Jupyter
notebooks and asynchronous document-based verification (in the spirit of
Isabelle’s Prover IDE) with VS Code.

Source link

Related posts

Independent Reviewers release first annual report on DeepMind Health


CMS Finalizes 2019 Medicare Physician Fee Schedule and Quality Payment Program Rule


Developers Release Electronic ROI Prototype Tool


This website uses cookies to improve your experience. We'll assume you're ok with this, but you can opt-out if you wish. Accept Read More

Privacy & Cookies Policy


COVID-19 (Coronavirus) is a new illness that is having a major effect on all businesses globally LIVE COVID-19 STATISTICS FOR World

WeCreativez WhatsApp Support
Our customer support team is here to answer your questions. Ask us anything!
👋 Hi, how can I help?