About: The Imandra Automated Reasoning System (System Description)

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: The Imandra Automated Reasoning System (System Description) Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
title	The Imandra Automated Reasoning System (System Description)
Creator	Aitken, Dave Bray, Matt Cruanes, Simon Ignatovich, Denis Kagan, Elijah Kanishev, Kostya Maclean, Ewen Mometto, Nicola Passmore, Grant
source	PMC
abstract	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 collaboration. 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, (ii) an inductive waterfall and simplifier which “lifts” many Boyer-Moore ideas to our typed higher-order setting. These mechanisms are tightly integrated and subject to many forms of user control.
has issue date	2020-06-06(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51054-1_30
has license	no-cc
sha1sum (hex)	b12321e336dc4855cd892b43aa64822df0c17ec8
schema:url	https://doi.org/10.1007/978-3-030-51054-1_30
resource representing a document's title	The Imandra Automated Reasoning System (System Description)
has PubMed Central identifier	PMC7324025
schema:publication	Automated Reasoning
resource representing a document's body	covid:b12321e336dc4855cd892b43aa64822df0c17ec8#body_text
is schema:about of	named entity 'LIVE' named entity 'SUBSET' named entity 'ORDER' named entity 'RECURSIVE' named entity 'COMPUTATIONAL' named entity 'EXPANSION' named entity 'REASONING' named entity 'MOORE' named entity 'CLOUD' named entity 'THEORIES' named entity 'INTEGRATED' named entity 'WATERFALL' named entity 'SEMI-AUTOMATIC' named entity 'DESCRIBE' named entity 'SUPPORTING' named entity 'BOUNDED' named entity 'Jupyter notebooks' named entity 'Boyer-Moore' named entity 'logical theory' named entity 'theorem prover' named entity 'Ackermann' named entity 'Primitive Recursive Arithmetic' named entity 'recursive functions' named entity 'Boolean' named entity 'Boolean' named entity 'first-order logic' named entity 'Boolean' named entity 'proof assistants' named entity 'higher-order' named entity 'ACL2' named entity 'higher-order' named entity 'axiom' named entity 'tab-completion' named entity 'well-founded' named entity 'OCaml' named entity 'SMT' named entity 'OCaml' named entity 'counterexample' named entity 'simplifier' named entity 'HOL' named entity 'computational logic' named entity 'user interfaces' named entity 'OCaml' named entity 'recursive function' named entity 'Mathematical models' named entity 'model-checking' named entity 'logic' named entity 'rewrite rules' named entity 'SMT' named entity 'Cantor normal form' named entity 'bounded and unbounded' named entity 'lexicographic' named entity 'VSCode' named entity 'function calls' named entity 'Boyer-Moore' named entity 'first-class' named entity 'Boyer-Moore' named entity 'subset' named entity 'Skolem functions' named entity 'algorithm' named entity 'recursions' named entity 'ordinals' named entity 'symbolic execution' named entity 'Boyer-Moore' named entity 'SMT solver' named entity 'lambda lifting' named entity 'IDE' named entity 'proof assistants' named entity 'logic' named entity 'function calls' named entity 'higher-order' named entity 'Isabelle' named entity 'well-foundedness' named entity 'ground instance' named entity 'subset'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2025 OpenLink Software